發(fā)布時間：2021-09-22 15:41

　　許多實(shí)用計(jì)算機(jī)程序是并發(fā)程序,且常由多個程序模塊組成。分離編譯對這樣的程序十分重要,它將每個程序模塊獨(dú)立地編譯之后鏈接成完整的可執(zhí)行程序。將編譯得到的目標(biāo)模塊鏈接成完整的目標(biāo)程序之后,正確的編譯過程應(yīng)能確保目標(biāo)程序與源程序的行為一致。這要求編譯過程不僅正確地編譯每個模塊本身,還要確保目標(biāo)模塊間的交互與源程序模塊一致。本文針對并發(fā)程序的分離編譯場景,研究了編譯正確性的形式化描述和驗(yàn)證技術(shù),并作出了如下貢獻(xiàn)。首先,本文提出了一個驗(yàn)證并發(fā)程序分離編譯器的驗(yàn)證框架,它通過復(fù)用經(jīng)過驗(yàn)證的串行程序編譯來構(gòu)建無數(shù)據(jù)競爭的并發(fā)程序的分離編譯及其正確性證明。在該框架中,本文提出了一種保持內(nèi)存印跡（執(zhí)行中訪問的內(nèi)存地址集合）的模擬關(guān)系,并將這種源模塊與目標(biāo)模塊間的模擬關(guān)系作為編譯正確性的形式化描述。在外部函數(shù)調(diào)用點(diǎn)和線程間同步點(diǎn)處,該模擬關(guān)系刻畫了模塊與環(huán)境的相互影響,令這種模擬關(guān)系具有模塊鏈接和非搶占式并發(fā)層面上的可組合性;通過在模擬關(guān)系中引入內(nèi)存印跡的保持關(guān)系,本文將完整程序間無數(shù)據(jù)競爭性質(zhì)的保持性分解成模塊間的局部性質(zhì),實(shí)現(xiàn)了無數(shù)據(jù)競爭性的保持性的模塊化驗(yàn)證。此外,通過對程序語言模型進(jìn)行抽象,該驗(yàn)證... 

【文章來源】：中國科學(xué)技術(shù)大學(xué)安徽省 211工程院校 985工程院校

【文章頁數(shù)】：181 頁

【學(xué)位級別】：博士

【部分圖文】：

圖２．３驗(yàn)證框架的擴(kuò)展??

?第５章驗(yàn)證框架的應(yīng)用——ＣＡＳＣｏｍｐＣｅｒｔ編譯器???引理?５．２（ｘ８６－ＳＣ是良定義的）ｗｄ（ｘ８６－ＳＣ）。??Ｘ８６－ＳＣ被編譯器用作目標(biāo)語言。在證明框架中的模擬關(guān)系反轉(zhuǎn)引理（引??理４．８）中，需要以目標(biāo)語言是確定性的為前提。為了能夠應(yīng)用該引理，我們證??明了?Ｘ８６－ＳＣ是確定性的。??引理?５．３?（ｘ８６＿ＳＣ是確定性的）ｄｅｔ（ｘ８６－ＳＣ）。??５．２?ＣｏｍｐＣｅｒｔ?的驗(yàn)證??Ｉ?１??

盡管ＣｏｍｐＣｅｒｔ不包含內(nèi)存印跡概念及相關(guān)的定義，在其編譯器證明中許多??中間定義、引理和證明腳本可以通過少量修改來支持內(nèi)存印跡的保持性。例如，??圖５．５給出了?Ｓｅｌｅｃｔｉｏｎ編譯趟的證明中的一個關(guān)鍵引理ｓｅｌ＿ｅｘｐｒ＿ｃｏｒｒｅｃｔ，其??高亮部分是我們對該引理做的修改。該引理的含義是經(jīng)指令選擇得到的新表達(dá)??式的求值結(jié)果是原表達(dá)式求值結(jié)果的精化。我們對該引理作的修改只是增加對??內(nèi)存印跡的約束，即在擴(kuò)展（Ｍｅｍ．ｅｘｔｅｎｄｓ）的內(nèi)存上，指令選擇得到的新表達(dá)??式比原表達(dá)式有更小（ｆＰ．ｓｕ／ｊｓｅｔ）的內(nèi)存印跡。??在復(fù)用ＣｏｍｐＣｅｒｔ模擬關(guān)系不變式（ｍａｔｃｈ＿ｓｔａｔｅ關(guān)系）時，添加對內(nèi)存印??跡保持性的支持相對直接．例如圖５．６中給出的Ｓｅｌｅｃｔｉｏｎ編譯趟證明中的模擬??關(guān)系不變式，我們只需要在原ＣｏｍｐＣｅｒｔ的ｍａｔｃｈ＿ｓｔａｔｅ關(guān)系中加入內(nèi)存印跡相??關(guān)的約束（高亮部分）即可。??５．３?Ｃｏｑ中的驗(yàn)證工作量??本節(jié)我們介紹本文Ｃｏｑ實(shí)現(xiàn)的驗(yàn)證工作量。??


本文編號：3404001