并行程序驗證的若干關鍵技術研究.pdf

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

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

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

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