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

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

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

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

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

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