基于分組壓縮算法的并行程序模型檢測(cè).pdf

1、在并行時(shí)代，系統(tǒng)正確性驗(yàn)證越來(lái)越受到關(guān)注。在并行系統(tǒng)中，由于線程之間執(zhí)行次序的不確定性，錯(cuò)誤往往很難通過(guò)測(cè)試的方法重現(xiàn)，從而研究人員提出模型檢測(cè)技術(shù)驗(yàn)證并行程序。模型檢測(cè)一般利用狀態(tài)空間搜索的方法驗(yàn)證系統(tǒng)的正確性，隨著被驗(yàn)證系統(tǒng)規(guī)模的增大，各線程之間交互次序的改變導(dǎo)致被搜索的狀態(tài)集越來(lái)越大，因此，這種狀態(tài)爆炸現(xiàn)象是亟需解決的難題。本文致力于緩解驗(yàn)證過(guò)程中出現(xiàn)的狀態(tài)爆炸現(xiàn)象，在現(xiàn)有的模型檢測(cè)框架Spin基礎(chǔ)上，重新生成新的模型檢測(cè)器GSp

2、in。結(jié)合新的狀態(tài)空間搜索算法，減少搜索的狀態(tài)集，提高并行驗(yàn)證效率。
　　本文的研究工作及創(chuàng)新之處主要包括以下兩個(gè)方面:
　　1.編譯制導(dǎo)分組，結(jié)合分組壓縮算法搜索狀態(tài)空間
　　本文在Bell實(shí)驗(yàn)室開(kāi)發(fā)的模型檢測(cè)器Spin的基礎(chǔ)上，在驗(yàn)證程序中添加制導(dǎo)分組語(yǔ)句，重新改寫(xiě)新的詞法語(yǔ)法規(guī)則文件，添加對(duì)制導(dǎo)語(yǔ)句的分析處理，生成新的模型檢測(cè)器GSpin。利用GSpin生成的分組信息，結(jié)合分組壓縮算法搜索系統(tǒng)狀態(tài)。新的驗(yàn)證框架能

3、有效減少驗(yàn)證系統(tǒng)的狀態(tài)空間大小，提高驗(yàn)證效率。本文選取了8組測(cè)試程序，平均減少56.7％的狀態(tài)空間大小，有效提高了驗(yàn)證效率。
　　2.優(yōu)化的分組壓縮算法
　　為了進(jìn)一步提高程序的驗(yàn)證效率，考慮到各個(gè)分組之間的不相關(guān)性，本文提出兩種優(yōu)化的分組壓縮算法，分別為局部并行化的Native算法及完全并行化的Entirely算法。Native算法將分組與多線程一一對(duì)應(yīng)，使得每個(gè)線程順序搜索相應(yīng)的組，同步各組第一次到達(dá)自己的最終狀態(tài)后，利

4、用主線程將各線程的搜索路徑合并，在串行模式下繼續(xù)搜索系統(tǒng)狀態(tài)。Entirely算法認(rèn)為每個(gè)組都是一個(gè)獨(dú)立的整體，并不僅僅在第一條完整路徑上，還包括回溯等過(guò)程。該算法更能縮短驗(yàn)證時(shí)間，進(jìn)一步提高驗(yàn)證效率。利用局部并行化算法Native算法搜索程序狀態(tài)空間，隨著被驗(yàn)證程序規(guī)模的增加，并行化效果也隨之加強(qiáng)，驗(yàn)證時(shí)間平均減少了41.7％,但以消耗內(nèi)存為代價(jià)，內(nèi)存是順序模式下的分組壓縮算法的1.47倍。完全并行搜索的Entirely算法平均搜索時(shí)