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

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

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

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

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