并行編程模型的確定性的證明方法及其應(yīng)用.pdf

1、如何開發(fā)并行程序并保證其正確性是一個(gè)研究熱點(diǎn)。由于線程交錯(cuò)執(zhí)行次序的不確定性，測(cè)試、調(diào)試工作不易覆蓋所有執(zhí)行情況、不易再現(xiàn)出錯(cuò)的執(zhí)行，于是即使進(jìn)行大量的測(cè)試、調(diào)試工作也不能完全保證程序是正確的。確定性并行技術(shù)保證程序在相同輸入下的的所有執(zhí)行是一致的并且能再現(xiàn)執(zhí)行，因而能簡(jiǎn)化測(cè)試、調(diào)試工作。
　　由于對(duì)并行確定性現(xiàn)存的認(rèn)識(shí)并不統(tǒng)一，而且在指導(dǎo)測(cè)試、調(diào)試工作時(shí)存在缺陷，因此本文以一個(gè)基于共享消息通道的確定性并行編程模型為例，深入研究確

2、定性的內(nèi)涵、證明方法與以及如何更完善地指導(dǎo)測(cè)試、調(diào)試工作。
　　為此，本文探討并完成以下工作;
　　1、提出一種能較好的統(tǒng)一認(rèn)識(shí)不同確定性的角度
　　本文指出各種確定性異同的核心因素在于:選擇哪些程序點(diǎn)進(jìn)行觀察以及如何觀察程序的狀態(tài)。如何選擇兩者進(jìn)行組合是主觀的，對(duì)應(yīng)了不同的確定性。而一個(gè)程序是否滿足某確定性是客觀的，取決于程序的語(yǔ)義和存儲(chǔ)模型。
　　當(dāng)選定兩個(gè)因素后，一個(gè)程序是確定的，當(dāng)且僅當(dāng)其任意兩次執(zhí)行到達(dá)

3、指定程序點(diǎn)的能力相同（都能到達(dá)觀察點(diǎn)或者都不能，兩者是對(duì)立的），而且（若可以）到達(dá)觀察點(diǎn)處時(shí)的狀態(tài)觀察起來(lái)相同。
　　例如，最終點(diǎn)確定性指在程序執(zhí)行的最終點(diǎn)，觀察整個(gè)程序的狀態(tài)。調(diào)試確定性指在程序執(zhí)行的斷點(diǎn)處，觀察被調(diào)試線程相關(guān)的狀態(tài)。
　　2、提出一般性的確定性證明框架，將其應(yīng)用于一個(gè)基于共享消息通道的SPMC模型上并證明模型的最終點(diǎn)確定性和調(diào)試確定性
　　本文選定確定性并行編程模型SPMC(single-produ

4、cer-multiple-consumer)作為確定性的研究對(duì)象。給出模型的抽象語(yǔ)法、程序狀態(tài)定義和操作語(yǔ)義。基于此，定義并證明兩種確定性分別用于指導(dǎo)測(cè)試、調(diào)試工作。由于同時(shí)理解形式化的復(fù)雜模型和其確定性證明并不容易，為此，本文的介紹思路是先研究一些足夠簡(jiǎn)單的確定性并行編程模型，用它們展示證明模型確定性的普遍性框架，最后應(yīng)用于SPMC模型的研究。
　　總之，本文對(duì)確定性的認(rèn)識(shí)更具普遍性而且對(duì)測(cè)試、調(diào)試工作的指導(dǎo)更完善，對(duì)確定性的證