并行程序驗(yàn)證的若干關(guān)鍵技術(shù)研究.pdf

1、本文旨在對(duì)并行程序設(shè)計(jì)、通信正確性驗(yàn)證、性能分析給出相應(yīng)的建模與實(shí)現(xiàn)方法，以利于并行程序的推廣應(yīng)用。本文工作的主要貢獻(xiàn)表現(xiàn)在如下幾個(gè)方面：(1)在對(duì)現(xiàn)有主要的程序建模方法如UML、CSP(通信順序過程)與CCS(通信演算系統(tǒng))和Petri網(wǎng)做了詳細(xì)的分析，Petri網(wǎng)能較好地描述并發(fā)系統(tǒng)的結(jié)構(gòu)，表示系統(tǒng)中的并行、同步、沖突及順序等關(guān)系，并以圖形表示的組合模型，具有直觀、易懂和易用的優(yōu)點(diǎn)。根據(jù)并行程序的具體特點(diǎn)，應(yīng)用Petri

2、網(wǎng)作為建模工具，可以較好的描述并行程序中各種通信狀態(tài)。(2)研究了Petri網(wǎng)精煉操作動(dòng)態(tài)性質(zhì)保持關(guān)系，包括行為不變性、一致相關(guān)性、狀態(tài)不減性、公平性、不變量等等。它們?yōu)檠芯縈PI并行程序逐步求精方法奠定了理論基礎(chǔ)。(3)研究了基于Petri網(wǎng)的并行程序建模方法，包括：一般語句的Petri網(wǎng)模型，MPI通信語句的Petri網(wǎng)模型，并給出MPI逐步求精的設(shè)計(jì)方法。(4)研制了并行程序驗(yàn)證系統(tǒng)。本系統(tǒng)在windows環(huán)境下，使

3、用Visual C++6.0開發(fā)，采用VC的MFC編程。文件的讀寫使用了VC的順序化機(jī)制，實(shí)現(xiàn)了網(wǎng)文件的永久性保存。充分利用了windows下GUI編程的優(yōu)點(diǎn)，人機(jī)交互方便，可以對(duì)并行程序Petri網(wǎng)模型的性質(zhì)做分析，以檢查并行程序中是否含有與通信有關(guān)的錯(cuò)誤。如：孤兒消息、缺發(fā)消息、死鎖、活鎖等。利用該系統(tǒng)，給出矩陣乘法和快速傅立葉變換兩個(gè)程序的建模和驗(yàn)證過程。(5)參與開發(fā)移植了程序行為監(jiān)測(cè)和性能分析工具ParaVT系統(tǒng)，

4、該系統(tǒng)對(duì)并行程序的結(jié)構(gòu)進(jìn)行分析，在程序運(yùn)行過程中輸出必要的調(diào)試信息，并且動(dòng)態(tài)的監(jiān)視程序的運(yùn)行情況，當(dāng)前正在被調(diào)用的函數(shù)和函數(shù)的調(diào)用路徑可以通過樹形調(diào)用圖反映出來。根據(jù)接收到的調(diào)試信息對(duì)程序性能分析，給出對(duì)并行程序性能的分析結(jié)果，并且可視化地直觀呈現(xiàn)給最終的用戶?？梢圆榭吹姆治鲆晥D包括動(dòng)態(tài)運(yùn)行圖、通訊行為圖、負(fù)載平衡圖、通訊矩陣等。最后，關(guān)于進(jìn)一步工作的方向進(jìn)行了簡要的討論。關(guān)鍵詞：Petri網(wǎng)、并行程序、精煉操作、設(shè)計(jì)、驗(yàn)