逄龍等

摘 要：程序驗證是保證程序安全性的重要手段。隨著采用多核技術(shù)的硬件環(huán)境日漸普及，越來越多的軟件正通過轉(zhuǎn)向基于共享內(nèi)存的并行程序模型來充分利用現(xiàn)有的計算資源。各線程在并行執(zhí)行時通過共享內(nèi)存的訪問互相干擾執(zhí)行狀態(tài)，導(dǎo)致可能執(zhí)行路徑數(shù)成幾何級數(shù)增長，進(jìn)而產(chǎn)生可達(dá)狀態(tài)空間爆炸問題。由于驗證并行程序安全性主要通過分析程序可達(dá)狀態(tài)來實(shí)現(xiàn)，因此，對并行程序可達(dá)狀態(tài)空間的約簡是決定并行程序驗證效率的關(guān)鍵因素。首先對面向并行程序驗證的并行程序可達(dá)狀態(tài)空間約簡方法進(jìn)行了分類，然后對各類可達(dá)狀態(tài)空間約簡方法分別進(jìn)行了分析和總結(jié)，最后指出了當(dāng)前存在的問題和未來解決這些問題的研究方向。

關(guān)鍵詞：程序驗證；并行程序分析；可達(dá)狀態(tài)空間約簡

中圖分類號：TP311.5 文獻(xiàn)標(biāo)識碼：A 文章編號：2095-2163（2015）01-

Abstract： Program verification is the critical means to ensure the program safety. During the mature of multi-core hardware， there have been many programs which utilize the existed computing resources by adopting the memory shared concurrent program model. The concurrent threads interference with each other via the shared variables， which makes the reachable states increase with exponent factors. As a result， it results in the problem of combination explosion. Because the program verification relies on the reachable states， reducing the reachable state space is the key to the efficiency of program verification. In this paper， the reachable state reduction methods for concurrent program verification are classified， and the different kinds of reducing reachable states are analyzed and summarized. In the end， the issues which are still open are summarized and the future research directions to address these issues are also discussed.

Key words：Program Verification； Concurrent Program Analysis； Reduction of Reachable States

0引 言

多核硬件環(huán)境的日益普及使得能夠深度挖掘計算資源的并行化軟件已然成為軟件行業(yè)的主流，進(jìn)而即刻不斷滿足日漸提高的性能需求和功能需求。其中，基于共享內(nèi)存的并行程序模型在和基于消息通訊的并行程序相較候可知，該模型具有訪問便捷、信息交換開銷低廉等優(yōu)勢特點(diǎn)，足可堪稱當(dāng)前主要的并行程序通訊模型，并在航天、武器、交通、核電、醫(yī)療和金融等安全攸關(guān)領(lǐng)域有著極為廣泛且重要的應(yīng)用。毫無疑問，并行軟件的安全性就是影響其應(yīng)用的關(guān)鍵因素。而程序驗證則是保證程序安全性的重要手段， 一般情況下是由描述驗證條件的規(guī)格說明和計算程序可達(dá)狀態(tài)的分析算法組合構(gòu)成。程序驗證的目的就是旨在通過程序分析來判斷程序的可達(dá)狀態(tài)是否滿足驗證條件。然而，各線程在并行執(zhí)行時通過共享內(nèi)存的訪問互相干擾執(zhí)行狀態(tài)，就將導(dǎo)致可能執(zhí)行路徑數(shù)成幾何量級增長，進(jìn)而產(chǎn)生可達(dá)狀態(tài)空間組合爆炸問題，也為驗證并行程序安全性制造了攻克難點(diǎn)與挑戰(zhàn)。

在此，并行程序可達(dá)狀態(tài)空間約簡可表述為：通過一定規(guī)則來合并具有相同或相似可達(dá)程序狀態(tài)路徑的搜索策略，由此即可緩解來自組合爆炸導(dǎo)致的復(fù)雜計算壓力。同時，對并行程序可達(dá)狀態(tài)空間的約簡效果還將直接決定對并行程序驗證的可實(shí)現(xiàn)效率及可應(yīng)用規(guī)模。當(dāng)前的并行程序可達(dá)狀態(tài)空間約簡方法即是從不同角度出發(fā)、并采取多樣的規(guī)則對并行程序中的路徑進(jìn)行明確劃分，有效地解決或緩解研究環(huán)境中面臨的問題，但是，其約簡方法卻仍將受到其他條件制約。所以，如何進(jìn)一步整合并行程序可達(dá)狀態(tài)空間的各種約簡方法的優(yōu)點(diǎn)并克服其各自缺點(diǎn)就依然是目前一個亟需深入探討與解決的開放性問題。

本文首先對當(dāng)前的并行程序可達(dá)狀態(tài)空間的約簡方法進(jìn)行介紹，而后又分別就其優(yōu)點(diǎn)和不足展開相應(yīng)分析，并基于此再次給出這對這些不足的研究方向綜述。

1并行程序可達(dá)狀態(tài)空間約簡方法分類

并行程序可達(dá)狀態(tài)空間約簡的目標(biāo)是如何有效緩解由交疊執(zhí)行所導(dǎo)致的狀態(tài)空間組合爆炸問題。但由于對程序并行性的不同視角則決定了在搜索可達(dá)狀態(tài)空間時的不同約簡策略，為此即根據(jù)消除并行程序空間狀態(tài)冗余的不同出發(fā)點(diǎn)而將并行程序可達(dá)狀態(tài)空間約簡方法具體分為以下四類：偏序關(guān)系約簡方法、模塊性約簡方法、對稱性約簡方法和并行干擾約簡方法。下面對這四類約簡方法進(jìn)行逐一的闡述與介紹。

1.1 偏序關(guān)系約簡方法

偏序關(guān)系約簡是從蹤跡的獨(dú)立性出發(fā)，而只搜索可能產(chǎn)生不同程序狀態(tài)的蹤跡。Godefroid就研究了獨(dú)立變遷的等價關(guān)系[1]。兩個變遷若稱為獨(dú)立，當(dāng)且僅當(dāng)在一條蹤跡中這兩個臨近的變遷調(diào)換執(zhí)行順序后該蹤跡的可達(dá)狀態(tài)不變。鑒于該方法只是分析并行線程交疊執(zhí)行等價類中的代表蹤跡，因而避免了交疊執(zhí)行等價類內(nèi)其它蹤跡的冗余分析。

近期研究則主要集中在如何提高交疊執(zhí)行等價類的劃分精度。已有研究可知，通過靜態(tài)分析的方法計算蹤跡等價類中的可調(diào)度變遷卻將占據(jù)較大時空開銷。為了解決這一問題，F(xiàn)lanagan等即相應(yīng)提出了動態(tài)偏序關(guān)系約簡[2]，通過動態(tài)跟蹤線程間交疊執(zhí)行位置來分析發(fā)生沖突的回溯點(diǎn)。然而，該方法仍然存在重復(fù)訪問等價蹤跡類內(nèi)的其他并行狀態(tài)的可能。為了避免重復(fù)訪問并行狀態(tài)問題，分別由Gueta等提出了笛卡兒偏序關(guān)系約簡[3]和Yang等提出的含有狀態(tài)的動態(tài)偏序關(guān)系約簡[4]，其主要思想是通過識別變遷間的依賴關(guān)系來區(qū)分可達(dá)狀態(tài)。同時，又依次由Kahlon等提出了單調(diào)偏序關(guān)系約簡[5]和由Abdulla等進(jìn)一步提出的優(yōu)化動態(tài)偏序關(guān)系約簡[6]，其主要成果則是通過對調(diào)度賦予權(quán)重來優(yōu)化遍歷次序。而且，Kusano等[7]又采用了動態(tài)分析和靜態(tài)分析相結(jié)合的偏序關(guān)系約簡策略，具體結(jié)合點(diǎn)則是利用提出的謂詞依賴關(guān)系而將并行程序狀態(tài)空間抽象為可能導(dǎo)致斷言失敗或死鎖的沖突內(nèi)存訪問對，其實(shí)現(xiàn)過程是將目標(biāo)程序插樁，同時再通過依賴算子分析并行操作間的依賴關(guān)系，而后又以此為依據(jù)在動態(tài)分析已插樁的目標(biāo)程序時采用動態(tài)偏序約簡策略來對冗余的交疊蹤跡完成剪枝處理。

1.2 并行程序模塊化驗證

并行程序模塊化約簡是從線程內(nèi)局部操作和全局操作的差別出發(fā)，通過分別推理線程內(nèi)程序狀態(tài)和線程間作用狀態(tài)來降低搜索空間。具體地，依賴保證約簡（Rely-Guarantee，RG）即是典型代表，如文獻(xiàn)[8-13]。該方法首先假設(shè)外界線程對本地線程的影響，作為依賴（Rely），由此推理線程內(nèi)局部狀態(tài)，再分析本地線程施加于遠(yuǎn)端并行線程對的影響，作為保證（Guarantee）。其后則迭代分析可達(dá)狀態(tài)，直到狀態(tài)空間穩(wěn)定。

歸納數(shù)據(jù)流圖（Inductive Data Flow Graph， iDFG）方法[14-15]同樣利用了線程間交互的模塊性特點(diǎn)，即通過迭代分析共享變量在線程間的數(shù)據(jù)流圖來搜索狀態(tài)空間。而與此迭代分析不同的是，本文方法是在保證目標(biāo)屬性仍然安全的條件下通過泛化當(dāng)前可達(dá)狀態(tài)，以此來實(shí)現(xiàn)狀態(tài)空間的約簡。

1.3 對稱性約簡方法

對稱性約簡就是利用相似線程間狀態(tài)變遷相似的特點(diǎn)來簡化并行程序狀態(tài)空間的方法。傳統(tǒng)約簡方法[16]中將對稱性定義為變遷等價類。對稱關(guān)系則是在程序狀態(tài)空間上的一個雙射關(guān)系π，且滿足如下約束：即（s，s）是一個變遷時，當(dāng)且僅當(dāng)存在對應(yīng)的另一個變遷（π（s）， π（s））。但是該類定義卻假設(shè)并行線程都是無法區(qū)分，這將極大限制了在該定義下的應(yīng)用范圍?；诖?，如何將對稱關(guān)系的約束拓寬至非對稱關(guān)系的約束也隨即成為近期研究的主要方向。相應(yīng)地，文獻(xiàn)[17]提出了近似對稱和粗糙對稱結(jié)定義，繼而由文獻(xiàn)[18]推廣到虛擬對稱。虛擬對稱就是滿足互模擬對稱商的最通用的條件。只是互模擬對稱商很難獲得，而且該類驗證的屬性也僅只局限于對稱屬性。文獻(xiàn)[19]則提出了“超級結(jié)構(gòu)”，并通過向該結(jié)構(gòu)增加輔助變遷來表達(dá)任意對稱關(guān)系，由此構(gòu)造保護(hù)標(biāo)記商。但是在驗證過程中卻要通過頻繁地檢測是否滿足實(shí)際對稱關(guān)系來彌補(bǔ)由于輔助變遷導(dǎo)致的精度缺失。另有，文獻(xiàn)[20]又提出了懶惰約簡策略，在分析程序前不假設(shè)任何對稱關(guān)系，而在搜索過程中對每個可達(dá)狀態(tài)也只是標(biāo)記其如何違反了對稱關(guān)系，主要依據(jù)就是：進(jìn)程的相似度越高，其所獲壓縮表示的程度將越深。該方法采用了自頂向下壓縮方式，并利用語法相似性來標(biāo)記進(jìn)程間對稱性，再通過虛擬結(jié)點(diǎn)表示構(gòu)成對稱關(guān)系的實(shí)際狀態(tài)結(jié)點(diǎn)集合，以此建立了約簡結(jié)構(gòu)。而當(dāng)模型檢測時，即將虛擬結(jié)點(diǎn)轉(zhuǎn)換為實(shí)際結(jié)點(diǎn)進(jìn)行分別驗證。此外，文獻(xiàn)[21]提出了利用克雷格插值技術(shù)以自底向上來發(fā)掘?qū)ΨQ性。具體實(shí)現(xiàn)時，由于計算克雷格插值時采用的是后向?qū)W習(xí)策略，這就在保證合并后狀態(tài)的同時，又進(jìn)一步保證了斷言的安全性，而且也避免了逐項展開的額外開銷。

1.4 并行程序干擾分析

由共享變量傳遞的并行干擾是導(dǎo)致并行程序交疊執(zhí)行下可行蹤跡組合爆炸的直接原因，第三類約簡方法即是從待驗證的目標(biāo)屬性出發(fā)，卻只分析了與目標(biāo)屬性相關(guān)的交疊執(zhí)行蹤跡和可達(dá)狀態(tài)。而并行干擾抽象方法[22-23]則是將交疊執(zhí)行轉(zhuǎn)化為共享變量讀寫匹配對的可滿足性問題而展開其實(shí)現(xiàn)研究的。該方法以有限模型檢測為基礎(chǔ)、而且以不同并行線程對共享內(nèi)存的訪問為分析目標(biāo)，在將讀系匹配對編碼為一階謂詞命題形式后，利用約束求解器（Satisfiability Modulo Theory，SMT）進(jìn)行了計算，繼而又利用關(guān)聯(lián)變量上近似和下近似來控制查詢規(guī)模，同時也利用上下近似修正規(guī)則來指導(dǎo)迭代的下一輪查詢，該過程中將基于不動點(diǎn)理論判知該過程收斂至對驗證條件的證明或者發(fā)現(xiàn)真實(shí)反例。研究可知，對于發(fā)現(xiàn)并行程序缺陷，該方法可以在精度與效率方面得到良好平衡。

2 現(xiàn)有并行程序狀態(tài)空間約簡方法的不足

綜上論述可知，基于偏序關(guān)系的約簡方法流程是分析了可能的交疊執(zhí)行劃分，再計算對共享變量的影響。而在共享內(nèi)存模型下，通過共享變量間數(shù)據(jù)流關(guān)系相較控制流則更易分析共享變量和線程內(nèi)局部變量的可達(dá)狀態(tài)。但是，該類方法卻因在獨(dú)立蹤跡實(shí)際可達(dá)狀態(tài)間的關(guān)系方面缺乏充足考慮，這就使得即便彼此獨(dú)立的代表蹤跡也仍有可能具有相同的可達(dá)狀態(tài)集合。

并行程序模塊化驗證方法具有迭代分析特點(diǎn)，但在迭代過程會產(chǎn)生虛假蹤跡的問題，針對該錯誤即需進(jìn)行修正而產(chǎn)生了額外時空開銷。這是由于估計狀態(tài)與實(shí)際狀態(tài)差異及其傳播，由此而延遲了對線程內(nèi)可達(dá)狀態(tài)的修正，致使部分時空開銷將無可避免地耗費(fèi)在對不可行全局交疊執(zhí)行路徑的分析上。

在對稱性約簡方法中，利用插值策略來約簡并行線程間對稱性的技術(shù)拓展了對稱性的限制，而且在沒有先驗知識的條件下，又利用了弱對稱關(guān)系來實(shí)現(xiàn)了并行線程間相似的交疊執(zhí)行蹤跡和狀態(tài)的有效約簡。但是該方法在應(yīng)用插值蘊(yùn)含操作時對后續(xù)交疊執(zhí)行情況的要求卻過于嚴(yán)格，導(dǎo)致可被蘊(yùn)含的蹤跡相應(yīng)地出現(xiàn)了延遲，因而產(chǎn)生額外的分析開銷。

基于并行干擾的并行程序狀態(tài)空間約簡方法，因其依賴于有界模型檢測，即其輸入是執(zhí)行序列的有限展開，就使得并行干擾抽象是借助下近似策略來截斷無限循環(huán)類語句，由此導(dǎo)致對驗證條件的安全性證明將存在不完備的可能。

3 結(jié)束語

現(xiàn)有的并行程序狀態(tài)空間約簡方法主要從相對獨(dú)立的視角出發(fā)對其中冗余狀態(tài)或路徑進(jìn)行合并，但由于并行程序特點(diǎn)的不同，實(shí)現(xiàn)的代碼與分析視角的契合程度并不相同，因此現(xiàn)有方法只能適用于具有一定特點(diǎn)的某一類并行程序。如果能夠根據(jù)并行程序內(nèi)部的實(shí)際特點(diǎn)而分別采取某幾種方法來分析將會克服單一視角的不足，但是如何融合不同視角間不同類型并行信息的表達(dá)將是進(jìn)一步研究的方向。此外，如何將靜態(tài)分析結(jié)果與動態(tài)分析觀測值相結(jié)合來進(jìn)一步提高搜索效率也是需要深入探討的研究方向之一。

參考文獻(xiàn)：

[1]GODEFROID P. Partial-Order Methods for the Verification of Concurrent Systems： An Approach to the State-Explosion Problem[M]. Secaucus， NJ， USA： Springer-Verlag New York， Inc.， 1996.

[2]FLANAGAN C， GODEFROID P. Dynamic partial-order reduction for model checking software[C]//ACM Sigplan Notices. New York： ACM Press， 2005：110-121.

[3]GUETA G， FLANAGAN C， YAHAV E， et al. Cartesian partial-order reduction[C]//Proceedings of the 14th International SPIN Conference on Model Checking Software. Berlin， Heidelberg： Springer-Verlag， 2007：95–112.

[4]YANG Y， CHEN X， GOPALAKRISHNAN G， et al. Efficient stateful dynamic partial order reduction[C]//Model Checking Software： 15th International SPIN Workshop， Los Angeles， CA， USA， August 10-12， 2008， Proceedings. Berlin： Springer-Verlag， 2008：156：288.

[5]KAHLON V， WANG C， Gupta A. Monotonic partial order reduction： An optimal symbolic partial order reduction technique[C]//Computer Aided Verification. New York： ACM Press ， 2009：398–413.

[6]ABDULLA P， ARONIS S， JONSSON B， et al. Optimal dynamic partial order reduction[C]//Proceedings of the 41th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2014. New York： ACM， POPL 14.

[7]KUSANO M， WANG C. Assertion guided abstraction： a cooperative optimization for dynamic partial order reduction[C]//Proceedings of the 29th ACM/IEEE international conference on Automated software engineering. ACM， 2014： 175-186.

[8]GUPTA A， POPEEA C， RYBALCHENKO A. Threader： a constraint-based verifier for multi-threaded programs[C]//Computer Aided Verification. Berlin： Springer， 2011：412–417.

[9] GUPTA A， POPEEA C， RYBALCHENKO A. Predicate abstraction and refinement for verifying multi-threaded programs[C]//ACM SIGPLAN Notices. New York： ACM， 2011：331–344.

[10]VAFEIADIS V. RGSep action inference[C]//Verification， Model Checking， and Abstract Interpretation. New York： Springer， 2010：345–361.

[11]VAFEIADIS V， PARKINSON M. A marriage of rely/guarantee and separation logic[C]//CONCUR 2007 Concurrency Theory. Berlin： Springer， 2007：256–271.

[12]VAFEIADIS V. Automatically proving linearizability [C]//Computer Aided Verification. Berlin： Springer， 2010：450–464.

[13]CUOQ P， KIRCHNER F， KOSMATOV N， et al. Frama-C [M]. Gilles Barthe， Alberto Pardo：Software Engineering and Formal Methods. Berlin： Springer， 2012：233–247.

[14]FARZAN A， KINCAID Z. Verification of parameterized concurrent programs by modular reasoning about data and control[C]//Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2012：570-582.

[15] Farzan A， Kincaid Z， Podelski A. Inductive data flow graphs[C]//Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York： ACM， 2013：129–142.

[16]EMERSON E A， SISTLA A P. Utilizing symmetry when model-checking under fairness assumptions： an automata-theoretic approach[J]. ACM Transactions on Programming Languages and Systems （TOPLAS）， 1997， 19（4）： 617-638.

[17]EMERSON E A， TREFLER R J. From asymmetry to full symmetry： New techniques for symmetry reduction in model checking[M]//Tiziana Margaria：Correct Hardware Design and Verification Methods. Springer Berlin Heidelberg， 1999： 142-157.

[18]EMERSON E A， HAVLICEK J W， TREFLER R J. Virtual symmetry reduction[C]//Logic in Computer Science， 2000. Proceedings. 15th Annual IEEE Symposium on. Santa Barbara， California， USA：IEEE， 2000： 121-131.

[19]SISTLA A P， GODEFROID P. Symmetry and reduced symmetry in model checking[J]. ACM Transactions on Programming Languages and Systems （TOPLAS）， 2004， 26（4）： 702-734.

[20]WAHL T， DSILVA V. A lazy approach to symmetry reduction[J]. Formal aspects of computing， 2010， 22（6）： 713-733.

[21]CHU D H， JAFFAR J. A complete method for symmetry reduction in safety verification[C]//Computer Aided Verification.Berkeley， CA，USA： CAV2012， 2012： 616-633.

[22]SINHA N， WANG C. Staged concurrent program analysis[C]//Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering. New York： ACM Press， 2010： 47–56.

[23]SINHA N， WANG C. On interference abstractions[C]// ACM SIGPLAN Notices. New York： ACM Press， 2011： 423-434.