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

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

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

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