面向程序驗證的并行程序狀態空間態約簡技術綜述

逄龍等

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

關鍵詞：程序驗證；并行程序分析；可達狀態空間約簡

中圖分類號：TP311.5 文獻標識碼：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引 言

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

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

本文首先對當前的并行程序可達狀態空間的約簡方法進行介紹，而后又分別就其優點和不足展開相應分析，并基于此再次給出這對這些不足的研究方向綜述。

1并行程序可達狀態空間約簡方法分類

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

1.1 偏序關系約簡方法

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

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

1.2 并行程序模塊化驗證

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

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

1.3 對稱性約簡方法

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

1.4 并行程序干擾分析

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

2 現有并行程序狀態空間約簡方法的不足

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

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

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

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

3 結束語

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

參考文獻：

[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.