《基於符號執行的並發程式分析與驗證研究》是依託中國人民解放軍國防科技大學，由黃春擔任項目負責人的面上項目。
基本介紹
- 中文名：基於符號執行的並發程式分析與驗證研究
- 項目類別：面上項目
- 項目負責人：黃春
- 依託單位：中國人民解放軍國防科技大學
中文摘要,結題摘要,
中文摘要
隨著並行計算和異構多核平台的套用越來越廣泛，並發軟體的質量引起了廣泛關注。由於並發系統自身的非確定性，使得並發程式呈現出不可預測性、狀態空間巨大、複雜性等特徵,為並發系統的可信保障帶來了巨大挑戰。因此，研究並發程式的形式驗證技術，對提高並發系統的可靠性與安全性具有重要意義。本項目將首先從並發程式的特點和可信需求出發，研究並發程式的錯誤特徵和關鍵性質規約方法，得到能夠支持並發程式交疊執行規約的多維形式規約方法；然後在規約方法的基礎上，結合符號執行技術的最新進展，研究基於符號執行的分析驗證技術及其最佳化，支持高效的並發程式驗證；進一步研究符號執行的環境支持和數據結構抽象技術，提高驗證方法可行性和完全性；最終建立自動化程度高、直接面向原始碼的並發程式符號執行和驗證工具。本項目的研究能顯著提高並發程式的驗證能力，能豐富和發展基於符號執行的程式分析與驗證方法，為提高並發系統的可靠性提供有力支持。
結題摘要
隨著並行計算和異構多核平台的套用越來越廣泛，並發軟體的質量引起了廣泛關注。由於並發系統自身的非確定性，使得並發程式呈現出不可預測性、狀態空間巨大、複雜性等特徵，為並發系統的可信保障帶來了巨大挑戰。從目前看，對於並發軟體，符合其特點的形式規約方法、驗證方法以及有效的驗證工具都有待於進一步研究。對此，本項目針對具有典型特徵的並行程式，對其可信保證理論基礎和關鍵技術進行了深入研究。本項目的主要研究成果包括： （1）在現有程式分析理論和方法的基礎上，研究了基礎了的符號執行方法，提出了猜測符號執行方法、正規性質引導的符號執行方法以及浮點及複雜數據類型程式的符號執行方法，以提高符號執行的可行性和可擴展性。 （2）研究提出了MPI程式的符號執行方法，能系統探索含阻塞和非阻塞通訊MPI程式的行為空間；基於符號執行方法，提出了MPI程式符號化驗證方法，有機結合目前的模型檢驗技術，可驗證MPI程式的關鍵性質；同時，提出了基於符號執行的MPI程式同步錯缺陷檢測方法，以發現非阻塞通訊MPI程式中的同步錯缺陷； （3）研究了基於請求路徑的並發系統性能問題診斷方法，提出了基於路徑分割的性能異常診斷方法，以降低數據維度、增大樣本容量，從而提高診斷方法的效率和結果的準確度。 根據上述理論和方法，項目設計實現了MPI C程式的符號化分析驗證工具，並在多個實際的MPI程式上開展了實驗套用；同時，也設計開發了基於請求路徑的並發系統性能問題檢測及診斷工具。
