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

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

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

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

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