并發(fā)程序精化驗(yàn)證及其應(yīng)用.pdf

1、許多程序驗(yàn)證問題都可以被歸結(jié)為精化驗(yàn)證，即證明一個(gè)較具體的程序不會(huì)比一個(gè)較抽象的程序產(chǎn)生更多的行為。本文發(fā)掘了在并發(fā)環(huán)境下精化驗(yàn)證的應(yīng)用場(chǎng)景，并提出若干種可以支持這些精化應(yīng)用實(shí)例的驗(yàn)證技術(shù)。具體來說，本文在理解和驗(yàn)證并發(fā)程序精化方面做出了如下貢獻(xiàn)。
　　首先，本文提出了一種基于依賴/保證的模擬關(guān)系RGSim，作為并發(fā)程序精化的通用驗(yàn)證手段。這一新穎的模擬關(guān)系將線程和并發(fā)環(huán)境之間的交互作為參數(shù)，從而獲得可組合性，支持模塊化驗(yàn)證。同時(shí)

2、，它將精化應(yīng)用中對(duì)并發(fā)環(huán)境的特定前提參數(shù)化，因而具有較好的靈活性和實(shí)用性。我們應(yīng)用RGSim驗(yàn)證了并發(fā)環(huán)境下的幾種程序優(yōu)化。此外，我們還將并發(fā)垃圾收集器的驗(yàn)證歸結(jié)為精化驗(yàn)證，并提出一種基于RGSim的通用驗(yàn)證框架。使用這一框架，我們驗(yàn)證了Boehm等人提出的并發(fā)的標(biāo)記-清掃垃圾收集算法。
　　其次，本文提出了一種霍爾風(fēng)格的程序邏輯，用于高效地、模塊化地驗(yàn)證并發(fā)對(duì)象的線性一致性。這是并發(fā)程序精化驗(yàn)證的一種重要應(yīng)用。作為該程序邏輯的一

3、部分，我們提出了一種輕量的輔助代碼插樁機(jī)制。我們的程序邏輯支持可線性化點(diǎn)不固定的并發(fā)算法，這些算法的驗(yàn)證難度很大。具體包括:使用幫助機(jī)制的無鎖算法（如 HSY棧），可線性化點(diǎn)依賴未來不確定執(zhí)行的算法（如懶惰集合算法），以及同時(shí)有這兩種特性的算法（如RDCSS算法）。我們還擴(kuò)展了模擬關(guān)系RGSim以支持可線性化點(diǎn)不固定的程序，新的模擬關(guān)系保證了我們的程序邏輯的可靠性，它可以蘊(yùn)涵一種上下文精化關(guān)系，該精化關(guān)系與線性一致性等價(jià)。我們應(yīng)用這一程

4、序邏輯驗(yàn)證了12個(gè)著名的并發(fā)算法，其中兩個(gè)算法已經(jīng)在Java并發(fā)包java.util.concurrent中使用。
　　最后，本文展示了一個(gè)用精化關(guān)系刻畫并發(fā)對(duì)象完整正確性（包括線性一致性以及各種進(jìn)展性性質(zhì)）的統(tǒng)一框架。我們證明了對(duì)于滿足線性一致性的并發(fā)對(duì)象，每種進(jìn)展性性質(zhì)等價(jià)于一種特定的對(duì)終止性敏感的上下文精化關(guān)系。我們用上下文精化關(guān)系統(tǒng)一了并發(fā)對(duì)象的線性一致性和所有常見的進(jìn)展性性質(zhì)，包括無等待性、無鎖性、無阻礙性、無饑餓性和無