并發(fā)程序精化驗證及其應用.pdf

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

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

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

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