在弱一致性模型中線程模塊化的靜態(tài)分析方法

◆楊舜堯

(阜新高等?？茖W(xué)校工程系 遼寧 123000)

0 引言

對于當(dāng)代計算機架構(gòu)來說，并發(fā)軟件的編寫是容易實現(xiàn)的，但是對于靜態(tài)編程分析仍然具有一定的挑戰(zhàn)性。盡管抽象解釋方法是非常強大的靜態(tài)分析技術(shù)，并且優(yōu)于線程模塊化的方法，而且減少了交織爆炸的發(fā)生。但是沒有為在弱一致性模型下運行的軟件系統(tǒng)而設(shè)計的分析方法。

由于弱一致性模型中所表現(xiàn)出的行為是不能被單處理器所接受的，這是一種嚴重的缺陷。例如：低速的內(nèi)存訪問或許造成延遲，增加了性能，但是也產(chǎn)生了額外的內(nèi)部線程不確定性。因此，在這種處理器中運行多線程軟件顯示出錯誤的行為，而在順序一致的存儲器中則沒有這樣的問題。

以x86-TSO存儲模式為例。在TSO模式下，每個處理器都有寫操作存儲緩沖區(qū)緩存，這樣就能使順序指令得到順利執(zhí)行，沒有任何障礙。理論上，處理器在后續(xù)的時間中，用一些列的寫操作命令去清空內(nèi)存。清空內(nèi)存的行為在程序執(zhí)行期間，在不確定的任意時間發(fā)生。這種延遲發(fā)生在寫操作命令執(zhí)行和寫操作命令起效的期間，并造成在同一線程執(zhí)行期間，寫命令的重復(fù)調(diào)用。圖1顯示了在順序一致的存儲器（SC）模式下得到了證實，而在TSO中沒有發(fā)生。由于x和y初始化為0，并且沒有定義為原子性變量，這種寫操作（x=1，y=1）把變量存儲在緩沖區(qū)中，每個變量占用一個線程，因此在讀操作過程中會造成延遲發(fā)生。

圖1 斷言在SC模式下得到證實，在x86-TSO，SPACRC-PSO，和SPARC-RMO存儲模式下并未發(fā)生

assert(!(a == 0 && b == 0));SPARC-PSO情況下有更多的非SC模式下的行為發(fā)生：對于每個內(nèi)存地址的存儲采用獨立的存儲緩沖區(qū)。也就是說，x=1和y=1在統(tǒng)一線程的情況下，用不同的存儲緩沖區(qū)進行數(shù)據(jù)緩存，并分別獨立清空各自的緩存。這種模式下，在相同的線程中，可以對變量x重復(fù)調(diào)用一些列的寫操作，并把y的內(nèi)容傳遞給x，還可以把其他變量傳遞給x。這種值的傳遞方式與SPARC-RMO模式情況下是相似的。

一般來說，現(xiàn)有的線程模塊化抽象解釋器分為兩個類型，每種類型都與弱存儲模型不相關(guān)。第一種是特定SC模型：就只考慮與SC存儲模型兼容的行為，并且就線程交互模型而言，特定的SC模式被設(shè)計成流感知的模型。第二種是弱化存儲模式的方式，這種模式可以調(diào)用寫入內(nèi)存的命令，并越過線程調(diào)用命令。因此，弱化的存儲模式會產(chǎn)生虛假錯誤（虛假報警）。然而特定的SC模式對于SC存儲更加精準，但是在弱化的存儲模式中會丟失很多真正的錯誤。傳統(tǒng)方式修復(fù)這種缺陷是不容易的。例如：由于在所有程序節(jié)點上，一直保持這種狀態(tài)，使得傳統(tǒng)分析方法付出了很大代價。

對于弱一致性模式下的并發(fā)程序的分析，本文建議用第一種線程模塊化抽象解釋器來進行。本文的方法模仿了在流感知模式下的線程互動性，并結(jié)合專有的內(nèi)存存儲模式。方法在處理器級別的內(nèi)存模式下，模仿了內(nèi)存操作。

本文的方法建立了一個統(tǒng)一的框架來模仿內(nèi)存一致性語義。特別的，內(nèi)存互動是可行性。通過數(shù)據(jù)記錄所發(fā)現(xiàn)的約束性問題，在線程互動的可行性論證中已經(jīng)形成。本文的方法有效地解決了多項式時間問題，并適應(yīng)各種硬件級別的存儲模式。此外，本文的方法是在線程模塊化條件下，以線程敏感的方式處理線程間的交互。一次分析一個線程的程序，而不是分析整個程序，特別的對于大型程序，更是提高了分析效率。然而，不同于弱化的存儲模式，本文的方法不會考慮所有的遠程存儲效果，這樣能夠保證其精準度?？傊?，本文的方法不同于其他方法。傳統(tǒng)方式既是非模塊化的，又不是以弱內(nèi)存模式為目標的。

本文的方法既不同于尋找程序漏洞的技術(shù)，也不同于獲取正確性證據(jù)的技術(shù)。例如：在并發(fā)測試中，無界動態(tài)檢測范圍從順序一致性內(nèi)存模式到弱化的內(nèi)存模式。在有界模型檢測中，由阿爾格拉芙等做出的用代碼轉(zhuǎn)換或者系統(tǒng)編碼所做出的弱化內(nèi)存模式。然而，這些方法都不能用來修改這些屬性，如果系統(tǒng)沒有找到漏洞，不能意味著程序是正確的。本文的方法，與其他抽象解釋器一樣，重點是獲取程序正確性的證據(jù)。

實現(xiàn)本文方法用的是一種叫AppleTree的工具，這種工具使用的是以 C語言作為前端的底層虛擬機（LLVM）框架。衡量AppleTree，用209項嚴格的測試，和52個線程C語言程序的測試，共 61981行代碼。方法的可行性可表示為嵌入式斷言。AppleTree明顯比其他先進技術(shù)更加精準，并且在中等運行時開銷的情況下。

綜上所述，本文方法做了以下幾點：

提出了一種存儲模式下，明智的靜態(tài)分析方法，其中方法是基于線程模塊化的抽象解釋器。提出一種開源的分析框架，來論證在弱化內(nèi)存模式下的線程之間干擾的可能性。基于一系列的標準，實現(xiàn)并評估了本文方法，并證明了方法的高準確性和節(jié)約運行時的開銷。

圖2 斷言通常都會得到證實，但是在fence移除的情況下，斷言在PSO和RMO情況下就會失敗

觀察圖2中的程序。斷言手段證實了在SC，TSO和RMO模式下的真實情況。但是一旦移除fence，造成在PSO和RMO模式下失敗的情況。在第2部分闡述了在MM-oblivious（健忘性存儲器模式）模式下產(chǎn)生的嚴重錯誤的原因。特殊SC模式下產(chǎn)生嚴重報警的原因，以及如何修復(fù)這兩個錯誤。

1 在SC，TSO和RMO模式下的表現(xiàn)行為

首先，請注意在圖2中的斷言，是在SC模式下進行的，斷言證實了每個線程執(zhí)行的是程序中的調(diào)用指令，所以，在x=5在y=10之前生效，意味著，5賦值給x以后，線程2將10賦值給y。其次，本文解釋了在TSO模式下斷言能夠證實的情況。在加載一系列地址不相交內(nèi)存的情況下，TSO可以允許這種存儲模式時間上的延遲。這種程序上的調(diào)用指令的方法，是一種性能上的優(yōu)化。例如：在慢速存儲中的緩存技術(shù)，能夠加速序列化指令的加載。然而，由于所有的存儲都在同一線程中進行，并進入同一緩沖區(qū)，TSO模式不能記錄兩個存儲數(shù)據(jù)。因此，即使沒有fence，x=5也會在y=10之前賦值，這也證實了斷言的意義。

再次，本文也證實了移除fence會造成斷言在PSO和RMO模式下的失敗的原因。兩種模式都可以進行存儲，記錄由每個處理器分別存儲在不同地址內(nèi)存的緩沖區(qū)。這樣，x和y分別存儲在各自的緩沖區(qū)中。

由于緩沖區(qū)在各自獨立的內(nèi)存中被刷新，隨著fence的移除，y=10或許在x=5之前被賦值，即便這兩個指令在同一線程中被調(diào)用。因此，第2個線程或許在y讀取10之后，5才能被寫入x，在全局的內(nèi)存中，這樣的情況會造成斷言的失敗。fence很重要，在fence之前強制執(zhí)行所有的存儲事件，并在fence之后，所有的程序加載都是可見的。

對存儲模式的處理。由于之前的技術(shù)會過大估計線程干擾的作用，往往會導(dǎo)致嚴重的報警。例如：這些技術(shù)允許從遠程內(nèi)存中讀取數(shù)據(jù)來加載內(nèi)存，忽略了單一數(shù)據(jù)流或聯(lián)合數(shù)據(jù)流是否可行。由于其他技術(shù)低估了線程干擾的作用，可能導(dǎo)致錯過漏洞的查找。例如：不允許通過任何形式的非SC模式下的數(shù)據(jù)流。觀察圖2，x加載內(nèi)存，讀取0或5，y讀取0或10，但是，兩者是不可能同時進行的。但是，為實現(xiàn)這種不可能的方式，本文驗證了在弱化內(nèi)存語義的模式下，組合干擾的可行性。為此，提出兩種方法。第一種是流敏感性的線程干擾。與之前技術(shù)考慮加入所有線程干擾不同，本文分別處理每一次的組合干擾。第二種是在內(nèi)存一致性語義條件下，一種陳述式的建模，來適應(yīng)SC，TSO，PSO模式。兩種方法減少了組合線程干擾帶來的不可行性。例如：x和y讀取0和10的情況下，如圖2所示。

本文的方法是分析圖2中的線程2，考慮4種組合干擾的情況，a1-a4情況：

(1) a1∶ y[0,0],x[0,0]；

(2) a2∶ y[10,10], x[5,5] ;

(3) a3∶ y[0,0], x[5,5]；

(4) a4∶ y[10,10], x[0,0]。

本文適用兩種方式來檢驗方法的準確性。第一，移除由不可能組合的情況產(chǎn)生的無關(guān)值。第二，按照需求查詢輕量級約束系統(tǒng)，快速減小組合干擾的不可行性。a1,a2,a3都是可行的，不會造成斷言的失敗。

在多項式時間可解的情況下，使用數(shù)據(jù)記錄來檢查組合干擾的不可行性?，F(xiàn)在，請觀察圖2中的a4，演繹這種情況下地不可行性。

(1) y=0已經(jīng)執(zhí)行；

(2) x=5也已經(jīng)執(zhí)行了；

(3）x 的加載沒必要用初始化值[0,0]。

這種演繹從形式上證明了，a4在具體運算時是不存在的。由于a1-a3的組合沒有違反斷言，a4的情況是不可行的，這種特性也被證實了。

2 實驗

本文實現(xiàn)了弱化內(nèi)存感知的抽象解釋器，命名為AppleTree，并在代碼開源的平臺上進行實驗，例如：LLVM，Apron。特別指出，這里使用的是靜態(tài)分析方法，該方法在LLVM平臺上，把C語言代碼轉(zhuǎn)成LLVM平臺運行的比特代碼。

應(yīng)用先進的MM-obviouy型抽象解釋器，由Mine制作，還有WATTS的特殊的SC模式，在相同的平臺上進行實驗對比。并且把DUET的方法也進行了比較。

測試的結(jié)果：

首先，展示的是測試的結(jié)果。由于這些程序代碼數(shù)量較小，所有方法在同一衡量標準下測試，都會迅速地完成。因此，本文不會比較程序運行的時間，只是比較結(jié)果的精準性。尤其是在真實報警，虛假報警，真實證明，虛假證明方面，出現(xiàn)的次數(shù)與本文的AppleTree方法進行比較。

這里虛假報警是一種有效地屬性，但這種屬性不能被證實。然而，虛假這證明是一種可以隨時改變的屬性，并且是不可靠的的警告，也許被錯誤的證明。嚴格的測試是非常有用的，不僅是因為它能夠全面的考慮所有的問題，而且可以預(yù)先知道某一特性是否成立。

表1 在TSO模式下的嚴格測試結(jié)果

表1總結(jié)了在TSO模式下嚴格測試的結(jié)果。第一欄是每種方法的名稱，接下來的幾個欄分別是每種方法的真實報警，虛假報警，真實取證，虛假取證的出現(xiàn)的次數(shù)。由于WATTS的方法被設(shè)計成特殊SC模式，忽略了非SC模式行為，意味著在弱化內(nèi)存模式下進行的驗證是不可靠的。最后一欄是每種方法測試的整體分析時間?？傊Y(jié)果顯示，由于之前的Mine方法的線程模塊化技術(shù)，可以接受很多不適用的運行命令，導(dǎo)致207次的虛假報警，和143次的真實證明。因此，比之前的那些技術(shù)更加精準。

雖然WATTS只有13次的虛假報警，對于TSO模式來說是無效的，這種方法只考慮了SC模式下的行為，而且是不可靠的。再者，DUET的有效性都是在TSO或其他非SC模式下產(chǎn)生的，并且不是很清晰。在表中有34次的真實證明。

表2總結(jié)了PSO模式下的測試結(jié)果。WATTS在弱化內(nèi)存模式下的報警是無效的。在 PSO模式下所使用的測試程序與 TSO模式下所使用的是相同的，但是報警次數(shù)發(fā)生了變化。無論報警是真實的還是虛假的，Mine證明了8次特性的驗證，DUET有34個驗證，而本文有143次的驗證。

表2 在PSO模式下的嚴格測試結(jié)果

表3 在RMO模式下的嚴格測試結(jié)果

表3總結(jié)了在RMO模式下的測試結(jié)果。在RMO模式下，由于系統(tǒng)指令集不同于TSO和PSO模式下的情況，所以使用一系列不同的測試程序。否則，會觀察到與之前相似的結(jié)果。在表3中，AppleTree方法會獲取很多次的真實驗證，和叫少量的虛假報警。

3 總結(jié)

總體來說，本文的方法比之前的技術(shù)更加精準，然而，由于分析出的值大于計算值，所以不能排除所有的虛假報警的可能性，通常，大多數(shù)的虛假報警是由AppleTree產(chǎn)生的，并且要有多于2個線程的推理過程。由于本文的方法是線程模塊化的，所以線程通過經(jīng)其他線程抽象為一些列的干擾進行單獨分析。它不能捕獲涉及多于兩個線程的多的約束。原則上，我們可以通過擴大干擾可行性分析來解除這種限制：我們將此作為今后的工作。

[1]張一峰，方勇.基于LLVM的Android Native文件保護方法.通信技術(shù)，2017.

[2]Frontiers of Information Technology & Electronic Engineering; Modeling and noise analysis of a fence structure micro machined capacitive accelerometer system, 2010.

[3]Bertrand Jeannet and Antoine Mine. Apron: A library of numerical abstract domains for static analysis. In Ahmed Bouajjani and Oded Maler, editors, International Conference on Computer Aided Verification，2009.

[4]Antoine Mine. Relational thread-modular static value analysis by abstract interpretation. In International Conference on Verification, Model Checking, and Abstract Interpretation，2014.

[5]Markus Kusano and Chao Wang. Flow-sensitive composition of thread-modular abstract interpretation. In ACM SIGSOFT Symposium on Foundations of Software Engineering， 2016.

[6]Alan Huang. Maximally stateless model checking for concurrent bugs under relaxed memory models. In International Conference on Software Engineering，2016.