嵌入式多核環(huán)境下的并行程序建模與正確性驗證.pdf

1、以并行計算為基礎(chǔ)的高性能計算科學當前已經(jīng)成為科學研究的第三大支柱。使用并行計算的首要因為是高性能高效率,而并行程序的首要條件是正確性。以往的設(shè)計和分析工具都只關(guān)注于正確性和高性能的其中一個方面。
　　 針對以上情況,作者提出了一種能同時進行正確性驗證和性能分析的工具原型,該工具原型可使正確性驗證和性能分析一直貫穿于設(shè)計、運行、直到結(jié)果分析的全過程中。通過比較,給出用Petri網(wǎng)系統(tǒng)對并行程序建立模型的優(yōu)越性。
　　 現(xiàn)在

2、最廣泛應(yīng)用的編程模式是基于消息傳遞的,而MPI已經(jīng)成為事實上的標準。本文研究了并行程序函數(shù)的特點,給出了其所嵌套的C語言結(jié)構(gòu)的Petri網(wǎng)系統(tǒng)模型,提出針對并行程序建模初步的步驟與方法,給出了靜態(tài)可執(zhí)行的和并行正確的兩種并行程序概念,驗證了并行正確的并行程序模型的強連通性、可達性、安全性、活性與可逆性,給出了違背這些性質(zhì)的可能的因為,并提出使用圖的遍歷和Petri網(wǎng)模型的T-不變量、可達圖/樹等算法,對以上性質(zhì)和錯誤因為進行檢驗。

3、>　　 并行程序的基礎(chǔ)是正確性,由于其的復(fù)雜性,對其驗證要困難得多,因此要進行建模并驗證其性質(zhì)。將并行程序轉(zhuǎn)換為Petri網(wǎng)系統(tǒng)模型后,證明出相對于并行正確并行程序的Petri網(wǎng)系統(tǒng)模型應(yīng)當滿足的結(jié)構(gòu)性質(zhì),包括S不變量、T不變量、強連通性、守恒性以及受控死鎖性質(zhì),最后舉例說明了這些性質(zhì)在程序驗證中的應(yīng)用。由于這些性質(zhì)可以事前驗證,從而避免了通過動態(tài)性質(zhì)驗證會出現(xiàn)狀態(tài)死鎖的問題,因此提高了程序設(shè)計效率,同時以上方法具有廣泛的可推廣性。<

4、br>　　 若用網(wǎng)系統(tǒng)的結(jié)構(gòu)性質(zhì)進行分析,無需形成可達樹/圖,這樣就避免了可達狀態(tài)爆炸的問題,從而提高了驗證的準確度。由于是從編程角度來證明Petri網(wǎng)模型的性質(zhì),因此此方法符合并行程序驗證的原理,同時并行程序消息傳遞的模式有良好的可移植性,因此得到的模型和性質(zhì)具有普遍的可適用性。
　　 本文針對基于Petri網(wǎng)系統(tǒng)模型的并行程序做了一些正確性驗證,可以總結(jié)為幾個方面:
　　 1、對當前基于消息傳遞的并行程序模式,和該