基于上下文限界的并發(fā)程序可達性研究.pdf

1、隨著多核處理器的發(fā)展,對并發(fā)程序的研究已成為程序設計的熱點。然而并發(fā)程序執(zhí)行的不確定性,導致傳統測試方法很難發(fā)現程序中隱匿的錯誤。模型檢測作為一種自動驗證技術,已成為保證并發(fā)程序安全性與可靠性的重要手段?？蛇_性分析通過分析某一狀態(tài)是否可達來判定程序的正確性,是模型檢測的重要核心技術。
　　基于共享內存的通信方式是并發(fā)程序中最常用的通信方式之一,然而該程序可達性是不可判定的,而采用上下文限界技術對其進行約束,則能使其可達分析為可判定

2、。本文主要考慮基于共享內存通信的并發(fā)程序,結合上下文限界技術對其進行可達性分析。主要工作如下:
　　研究了不帶線程動態(tài)創(chuàng)建的并發(fā)程序的可達性問題,針對此類程序用異步下推網絡進行建模,采用現有的限界可達算法對其進行可達性分析。然而該算法需要精確的窮盡搜索每一條可能路徑,隨著變量的增多將產生狀態(tài)爆炸問題。為了緩解該算法面臨的狀態(tài)空間爆炸問題,本文對算法進行符號化分析。在符號化分析過程中為了符號表示一組可達格局集合而不引發(fā)“沖突”,在可

3、達計算的初始階段就把互斥的格局分開,使之得以很好的符號表示,有效的緩解了狀態(tài)爆炸問題。
　　研究了帶有線程動態(tài)創(chuàng)建的并發(fā)程序的可達性問題,針對此類并發(fā)程序的抽象模型——異步動態(tài)下推網絡進行可達分析,并結合上下文限界技術給出了兩種可達性分析算法。一是將該模型在k-上下文限界執(zhí)行下轉化為異步下推網絡,將帶動態(tài)線程創(chuàng)建的模型簡化為不帶動態(tài)線程創(chuàng)建的模型,然后對后者用上述提到的符號可達算法進行可達分析。二是在單個上下文中,將該模型的可達性