通信下推系统的一种有界可达算法

Qadeer首次针对并发下推系统提出一种有界可达算法,通过限定上下文切换的次数使得算法可终止,可有效地分析过程间并发程序。但是并发下推系统以全局变量模拟同步,不适应于当前广泛使用的基于事件驱动的并发程序。针对通信下推系统,提出一种基于双重调度的有界可达算法,通过限定同步调度的次数,结合线程间的同步调度和线程内的路径调度解决通信下推系统的可达性问题,从而为事件驱动的过程间并发程序分析提供了算法基础。