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

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

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

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