良序下推系统理论及其在并发程序分析中的应用

As hardware techniques reach maturity, we enjoy the benefits of concurrent computations every day. However, concurrent programs/software are notably error-prone and difficult to analyze since their state-reachability problem is generally undecidable. We propose Well-Structured Pushdown Systems (WSPDS), a general model for concurrent programs. We found most current models for concurrent program analysis can be reduced to submodels of WSPDS. We will: 1) study what kind of restrictions will lead to the decidability of WSPDS reachability, and relate the restrictions on WSPDS with those on concurrent programs; 2) find the "upper bound" of decidability for concurrent programs; 3) design algorithms to solve the reachability problem, and integrate them into program analyzing tools; and 4) demonstrate the expressiveness power of WSPDS. We expect the researches on WSPDS in this project will exhibit the current state of concurrent program analysis, reveal the essence of its undecidability and extend the methodology to more concurrent recursive programs.

硬件技术的高速发展带来了并发计算的春天，同时也使得对并发程序分析的研究更具紧迫性。程序分析中最关键的问题是可达性问题，它在并发递归程序上是不可判定的。良序下推系统是我们为并发程序分析提出的一般性模型，当前很多并发程序分析模型都可以证明能归约到它的子模型。在本项目中我们将从理论和应用两方面进一步深入研究良序下推系统：1）研究什么样的条件限制使得它的可达性可以判定,并发现这些限制在具体程序和程序语言上的呈现方式；2) 探索并发程序可判定的"上界"；3）为良序下推系统的可达性问题设计高效的判定算法，并嵌入到已有的并发程序分析工具中；4）研究良序下推系统的表达能力，厘清它与其他计算模型之间的关系。本项目希望能通过对良序下推系统的研究梳理并发程序分析的现状、揭示其不可判定的根本原因，发现高效实用的算法，从而能把更多的并发程序纳入可分析的范围，辅助人们设计正确的、能最大化利用硬件技术的并发程序。

为了进行并发递归程序的程序分析与验证，我们提出了良序下推系统这个通用模型，当前很多并发程序分析模型都可以证明能归约到它的子模型。本研究从理论和应用两方面进一步深入研究了良序下推系统。 首先，我们给出了良序下推系统几个可达性可判定的子集，同时证明了目前已有的一些可判定的并发程序模型都可以被良序下推系统覆盖。其次，我们得出了良序下推系统的可终止性和有界性可判定的结论。第三，我们同时实现了良序下推系统的一个子系统的高效算法，另外，我们实现了良序下推系统可终止性和有界性两个高效的判定算法。最后，在良序下推系统的表达能力上，我们得出了良序下推系统并非图灵等价的结论。