并发程序执行的一种粒度分析方法

A Granularity Analysis Approach to Concurrent Programs Execution

文章讨论基于交替计算模式的并发程序执行行为的可信性问题。通过比较共享变量程序的交替计算与实际重叠执行，对并发程序的执行过程进行粒度分析──首先提出一种粒度细化、求精方法，限制单个原子转换包含的临界事件数目；继而引入一种限制临界引用（ＬＣＲ）条件，进一步限制每一与语句相关的转换至多执行一次临界引用；对任一程序，通过转换算法将其转化为与之等价的ＬＣＲ程序，且ＬＲ程序的交替计算结果与实际的重叠执行结果是一致的。

The paper discusses the faithfulness of the behavior of concurrent programs based on interleaved compulation modes. First, it compares the results between interleaved computations by shared-variables programs and overlapped executions by actual concurrent program. Second, it presents an approach of finer granularity, by proper restrictions on the number of critical event contained in a single atomic transition. At last, it presents limited -critical -reference constraint(LCR) condition,each of the transition associated with a statement performs at most on critical reference. for every program P, there exists an LCR program that is equivalent to P, and interleaved computations and overlapped executions of LCR program yield the same set of behaviors.