CAJ | 학술논문

基于无界FIFO消息队列的通信框架作为一种通用的并发系统模型,常用于事件驱动的并发程序或分布式程序建模.然而当模型包含递归过程调用时,即使仅考虑执行有限次上下文切换,其可达性问题仍是不可判定的.假定进程的消息队列约束为良序,即仅当进程的局部栈为空时才能从队列中读取消息,则其在上下文切换定界上的可达性为可判定.文中以基于队列通信的递归并发程序为对象,研究其可达性问题.首先构造能模拟递归队列并发程序执行的多栈下推系统,并提出转换方法;然后给出一种基于多栈下推系统的上下文切换定界可达算法,算法使用标准Post*操作描述下推系统的迭代,基于良序排队控制进程对队列的出队操作,穷尽地计算k次上下文切换之内的正向可达格局,并证明了构造多栈下推系统方法和上下文切换定界可达算法的正确性;最后对目标状态集合与可达格局状态集合的交集进行判空,确定目标状态是否可达,从而较好地解决此类并发程序的可达性问题.
기우무계FIFO소식대렬적통신광가작위일충통용적병발계통모형,상용우사건구동적병발정서혹분포식정서건모.연이당모형포함체귀과정조용시,즉사부고필집행유한차상하문절환,기가체성문제잉시불가판정적.가정진정적소식대렬약속위량서,즉부당진정적국부잔위공시재능종대렬중독취소식,칙기재상하문절환정계상적가체성위가판정.문중이기우대렬통신적체귀병발정서위대상,연구기가체성문제.수선구조능모의체귀대렬병발정서집행적다잔하추계통,병제출전환방법;연후급출일충기우다잔하추계통적상하문절환정계가체산법,산법사용표준Post*조작묘술하추계통적질대,기우량서배대공제진정대대렬적출대조작,궁진지계산k차상하문절환지내적정향가체격국,병증명료구조다잔하추계통방법화상하문절환정계가체산법적정학성;최후대목표상태집합여가체격국상태집합적교집진행판공,학정목표상태시부가체,종이교호지해결차류병발정서적가체성문제.