使用事務(wù)內(nèi)存同步機(jī)制的并行程序驗(yàn)證的研究.pdf

1、近年來，隨著超線程、多核體系結(jié)構(gòu)等多線程技術(shù)的發(fā)展和廣泛應(yīng)用，計(jì)算機(jī)硬件已經(jīng)提供了越來越高效的軟件運(yùn)行平臺(tái)。但是要更好地利用這些平臺(tái)的并行優(yōu)勢(shì)，計(jì)算機(jī)軟件就需要具備更好地并行性，以充分利用多個(gè)處理器的性能。并行程序已經(jīng)成為了軟件開發(fā)的主流。然而要確保順序程序的正確性已經(jīng)是非常困難的了，要保證并行程序的正確性難度更甚。這是因?yàn)樵诓⑿谐绦蛑?，程序員還需要處理共享數(shù)據(jù)的并發(fā)存取問題，確保數(shù)據(jù)在不同線程中的有效性。傳統(tǒng)上，程序員使用鎖的方式來管

2、理并行程序中共享數(shù)據(jù)的并發(fā)存取。但是鎖方式不僅難于推理，而且還容易出現(xiàn)死鎖等導(dǎo)致程序進(jìn)入異常執(zhí)行狀態(tài)的隱患。為減輕程序員開發(fā)并行程序的負(fù)擔(dān)，提高軟件開發(fā)的效率，近年的研究提出了使用事務(wù)內(nèi)存同步機(jī)制來管理共享數(shù)據(jù)的并發(fā)存取。提供了事務(wù)內(nèi)存同步機(jī)制的系統(tǒng)通過自動(dòng)地管理數(shù)據(jù)的并發(fā)訪問，免除了程序員在這方面的負(fù)擔(dān)，也避免了死鎖等鎖機(jī)制的致命隱患。但是近年來圍繞著事務(wù)內(nèi)存同步機(jī)制的研究主要集中于提供事務(wù)內(nèi)存同步機(jī)制的系統(tǒng)的各種實(shí)現(xiàn)策略及其性能的提

3、高上，而對(duì)該同步機(jī)制在程序推理、形式驗(yàn)證及易于推理方面的研究甚少。 針對(duì)事務(wù)內(nèi)存同步機(jī)制相關(guān)研究的現(xiàn)狀，基于程序推理驗(yàn)證的研究成果，本文提出了一種推理方法以推理使用了事務(wù)內(nèi)存同步機(jī)制的實(shí)現(xiàn)系統(tǒng)所提供的編程結(jié)構(gòu)的程序。該推理方法基于眾所周知的不變式證明(InvarianceProof)方法并對(duì)Hoare邏輯進(jìn)行了擴(kuò)展，通過指明共享數(shù)據(jù)上的不變式來約束多個(gè)線程間的并發(fā)訪問，可靠、可行，并具備模塊化驗(yàn)證的特點(diǎn)。同時(shí)，本文還專注于事務(wù)內(nèi)

4、存同步機(jī)制的語義研究，在攜帶證明的代碼的研究的基礎(chǔ)上，將所提出的推理方法形式化到遵循事務(wù)內(nèi)存同步機(jī)制語義的Hoare風(fēng)格的驗(yàn)證框架中，并證明了推理方法遵循事務(wù)內(nèi)存同步機(jī)制的語義的可靠性。此外，本文還給出了推理驗(yàn)證的應(yīng)用實(shí)例，展示了本文所提出的推理方法和驗(yàn)證框架的有效性。最后，本文通過詳盡的比較，闡明了事務(wù)內(nèi)存同步機(jī)制相對(duì)于傳統(tǒng)的鎖同步機(jī)制易推理的優(yōu)點(diǎn)，展示了事務(wù)內(nèi)存同步機(jī)制對(duì)程序推理的簡化。 本文的主要特色和貢獻(xiàn)為： ·

5、本文提出了一種Hoare風(fēng)格的推理方法，用于在事務(wù)內(nèi)存同步機(jī)制的語義的高層抽象上推理源語言級(jí)的并行程序。 ·本文也提出了一個(gè)攜帶證明的代碼(Proof-CarryingCode)風(fēng)格的驗(yàn)證框架，用于在事務(wù)內(nèi)存同步機(jī)制的語義的底層實(shí)現(xiàn)上驗(yàn)證匯編級(jí)的并行程序，并證明了驗(yàn)證框架遵循事務(wù)內(nèi)存同步機(jī)制的語義的可靠性。該驗(yàn)證框架的提出，填補(bǔ)了攜帶證明的代碼的研究在事務(wù)內(nèi)存同步機(jī)制方面的空白。 ·本文在Coq定理證明輔助工具中完成了所