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

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

项目编号： No.61472238

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 蔡小娟

作者单位： 上海交通大学

项目金额： 74万元

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

中文关键词： 下推系统；并发程序分析；良序集；可达性问题；可判定性

英文摘要： 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.

英文关键词： Pushdown Systems;Concurrent Program Analysis;Well-quasi-order;Reachability;Decidability