《良序下推系統理論及其在並發程式分析中的套用》是依託上海交通大學，由蔡小娟擔任項目負責人的面上項目。
基本介紹
- 中文名：良序下推系統理論及其在並發程式分析中的套用
- 項目類別：面上項目
- 項目負責人：蔡小娟
- 依託單位：上海交通大學
項目摘要,結題摘要,
項目摘要
硬體技術的高速發展帶來了並發計算的春天，同時也使得對並發程式分析的研究更具緊迫性。程式分析中最關鍵的問題是可達性問題，它在並發遞歸程式上是不可判定的。良序下推系統是我們為並發程式分析提出的一般性模型，當前很多並發程式分析模型都可以證明能歸約到它的子模型。在本項目中我們將從理論和套用兩方面進一步深入研究良序下推系統：1、研究什麼樣的條件限制使得它的可達性可以判定,並發現這些限制在具體程式和程式語言上的呈現方式；2、探索並發程式可判定的上界；3、為良序下推系統的可達性問題設計高效的判定算法，並嵌入到已有的並發程式分析工具中；4、研究良序下推系統的表達能力，釐清它與其他計算模型之間的關係。本項目希望能通過對良序下推系統的研究梳理並發程式分析的現狀、揭示其不可判定的根本原因，發現高效實用的算法，從而能把更多的並發程式納入可分析的範圍，輔助人們設計正確的、能最大化利用硬體技術的並發程式。
結題摘要
為了進行並發遞歸程式的程式分析與驗證，我們提出了良序下推系統這個通用模型，當前很多並發程式分析模型都可以證明能歸約到它的子模型。本研究從理論和套用兩方面進一步深入研究了良序下推系統。 首先，我們給出了良序下推系統幾個可達性可判定的子集，同時證明了目前已有的一些可判定的並發程式模型都可以被良序下推系統覆蓋。其次，我們得出了良序下推系統的可終止性和有界性可判定的結論。第三，我們同時實現了良序下推系統的一個子系統的高效算法，另外，我們實現了良序下推系統可終止性和有界性兩個高效的判定算法。最後，在良序下推系統的表達能力上，我們得出了良序下推系統並非圖靈等價的結論。
