论文部分内容阅读
基于无界FIFO消息队列的通信框架作为一种通用的并发系统模型，常用于事件驱动的并发程序或分布式程序建模．然而当模型包含递归过程调用时，即使仅考虑执行有限次上下文切换，其可达性问题仍是不可判定的．假定进程的消息队列约束为良序，即仅当进程的局部栈为空时才能从队列中读取消息，则其在上下文切换定界上的可达性为可判定．文中以基于队列通信的递归并发程序为对象，研究其可达性问题．首先构造能模拟递归队列并发程序执行的多栈下推系统，并提出转换方法；然后给出一种基于多栈下推系统的上下文切换定界可达算法，算法使用标准Post’