异步通讯程序的程序分析理论与方法

Due to the expressiveness as Turing-complete, it is impossible to propose a general programming model for concurrent programs. This proposal focuses on a special concurrent program, asynchronously communicating program, on which there are no systematically theoretical results, neither efficient analysis tools. The researches includes, I. Apply a non-trivial restriction on the depth of the stack for asynchronously communicating programs based on unordered buffers, and investigate the decidability and complexity results on the coverability and liveness of the programming model with value-passing feature. II. Assume an asynchronously communicating program can be linearized, and investigate the decidability and complexity results on the verification problems. The research above can be used to analyze the programs. At the same time, the theoretical meaning is magnificent. III. Construct a theoretical model and an analysis model of asynchronously communicating programs with communications based on mailboxes. The research can make the asynchronously communicating program analysis more thorough and concrete. IV. Investigate verification algorithms and implementations of a model strictly more expressive than Petri net, and encode the programming models mentioned above to the implemented tool. Through a series of researches, we can systematically and entirely achieve the decidability and complexity results of the verification problems of asynchronously communicating program under different restrictions, and develop an efficient program analyzer on asynchronously communicating programs.

并发程序所固有的图灵完备特性，无法为其建立通用的程序模型。目前，开展的并发程序的特例——异步通讯程序研究，尚未有系统性的理论结论及高效的分析工具。为此，对其展开系统性研究。包括：1). 对基于无序缓存的异步通讯程序的各栈深度进行非平凡限制，研究允许各线程传值模型的可覆盖性、活性的判定性和复杂性问题；2). 假设异步通讯程序可以线性化，研究程序的输入通讯在不同限制条件下的可覆盖性、活性的判定性和复杂性问题，其结论除了应用于程序分析，还具有重要的理论意义；3). 研究并建立基于信箱的异步通讯程序的理论模型和分析模型，其结论可对异步通讯程序的分析更加深入具体；4). 研究表达能力严格大于Petri网的验证算法及实现问题，再将前述研究的程序模型编码到该工具上。通过上述研究，可系统全面地得到异步通讯程序在不同约束条件下的验证问题的判定性和复杂性结论，并开发出高效的异步通讯程序程序分析器。

在一年的研究中，针对异步通讯程序的验证模型进行了如下的研究：1)建立了异步程序的高效验证模型，将该程序的安全性规约为BPP模型上的可覆盖性问题，活性归约为BPP上的可达性问题。这两个性质都是NP完全的，大大地降低了原问题的复杂性。同时，开发了基于BPP模型的高效验证工具，用于将来程序分析器的开发。2) 在异步通讯程序的验证模型中，将 通讯和多栈两个问题分别予以限制和抽象，提出了通讯Petri网这一模型，在其中，对通讯，给予程序输入个数一个界；对栈进行了Pattern的抽象。并证明了该模型的可覆盖性是可判定的，可以用之来表示程序的安全性。活性是不可判定的，代表了这一问题在异步通讯程序需要以更高的限制来检查。3) 实时异步程序的验证问题，研究了具有时间性质的异步程序的可调度性、安全性和活性问题，给出了一个在不知道最差执行时间WCET的情况下，仍然可以判定可调度性的算法。给出了该模型安全性的可判定的结论，并且给出了一个可以实现的算法。