基于SMT的并發(fā)程序可滿足性驗證.pdf

1、隨著多處理器和多核計算的興起,并發(fā)程序的驗證逐漸成為學術界廣泛關注的熱點問題之一。然而,由于并發(fā)程序本身存在的線程交互性,使得程序的執(zhí)行不具備確定性,即在相同的輸入下,程序多次執(zhí)行后的結果可能不同,或者執(zhí)行結果相同但內部執(zhí)行路徑不同,上述兩種情況都直接導致了傳統(tǒng)的測試技術無法精確地發(fā)現(xiàn)并發(fā)程序中隱藏的錯誤和漏洞。因此,盡可能采用一種實用的形式化驗證方法和理論技術來解決并發(fā)程序研發(fā)過程中潛在的問題,顯得尤為重要與迫切。
　　在并發(fā)程

2、序的驗證技術中,可滿足性分析是一項重要的核心技術,其基本思想主要是通過分析某一個給定的性質是否滿足該并發(fā)程序模型,從而判定該程序是否存在錯誤或漏洞。本文分別針對基于共享變量和消息隊列通信方式的并發(fā)程序進行可滿足性分析,旨在通過可滿足性分析保證此類程序的正確性和可靠性?；谏鲜鏊枷?本文的研究工作主要包括:
　　(1)針對基于消息隊列進行線程間交互的并發(fā)程序,本文采用了基于SMT(Satisfiability Modulo Theo

3、ries)的有界模型隊列對其進行可滿足性公式編碼。由于當前的SMT求解器所采用的SMT-LIB格式的輸入語言并不直接支持隊列理論,因此,為了能夠準確地編碼消息隊列的行為,本文結合SMT求解器中的相關理論域,如未解釋函數(shù)(uninterpreted function)和數(shù)組(array),分別提出兩種不同的編碼方法:shifting編碼和cyclic編碼。對于前一種編碼方式,主要是采用不依賴于任何理論的布爾和位向量顯式地表示隊列中的內容,

4、該技術可以直接應用于基于 BDD(Bounded Model Checking)或SAT/SMT的驗證過程中;而對于后一種編碼方式,本文重點采用基于未解釋函數(shù)和數(shù)組的內容表示方法。最后對這兩種編碼方式進行了復雜度的比較。
　　(2)針對基于共享變量進行線程間交互的并發(fā)程序,本文采用了基于SMT的并發(fā)程序可滿足性驗證。由于SMT在表達能力上使用了含有量詞和變量的一階邏輯,能處理更加復雜的性質驗證,并且提高程序驗證的準確度,因此本文主

5、要采用基于SMT的驗證技術,同時為了能有效地限定允許交互的上下文切換數(shù)目、進一步約簡驗證并發(fā)程序的復雜度,本文還結合上下文限界(context-bounded)的思想,以及極小不可滿足核(minimal unsatisfiable clauses)的查找技術,提出了一種針對并發(fā)路徑程序模型(CTP)的可滿足性判定算法。并且通過復雜度分析理論上證明該算法在一定程度上能夠緩解對并發(fā)程序可滿足性驗證的復雜性。最后通過一個實例闡述了該方法的有效