基于多線程監(jiān)控器的運(yùn)行時驗證

陳 韜，王明明

(南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 211106)

1 概 述

軟件運(yùn)行時的驗證技術(shù)[1-3]，是對其他驗證技術(shù)例如模型檢測和軟件測試的一種補(bǔ)充，是一種輕量級的新型自動化驗證技術(shù)。由于運(yùn)行時驗證技術(shù)是在程序運(yùn)行過程中進(jìn)行驗證，所以它能保證驗證程序的實時性?；谛问交Z言的程序運(yùn)行時驗證的基本思想是輸入表示描述事件和性質(zhì)的形式化規(guī)約語法，目標(biāo)監(jiān)控C程序，輸出插樁好監(jiān)控器的新C程序。并采用該方法實現(xiàn)了原型工具M(jìn)ovec[4]。該工具的基本框架主要由解析器、監(jiān)控器、插樁器構(gòu)成。

其中形式化規(guī)約主要由以下幾部分組成：

(1)形式化規(guī)約的頭部分，包含了修飾符、名字以及名字所帶的參數(shù)；

(2)規(guī)約文件變量的聲明、定義，變量可由用戶自己操作；

(3)切點聲明，采用了面向方面[5]編程思想，切點指函數(shù)調(diào)用、變量的賦值、函數(shù)執(zhí)行、變量設(shè)置等；

(4)事件聲明，即匹配的連接點之前或者之后進(jìn)行額外的操作，也可替換連接點的執(zhí)行；

(5)性質(zhì)，用形式化語言描述的規(guī)約性質(zhì)；

(6)性質(zhì)觸發(fā)器，當(dāng)滿足或者違反性質(zhì)時需要進(jìn)行什么樣的操作。

該原型工具首先對形式化規(guī)約文件進(jìn)行解析，然后構(gòu)造出監(jiān)控器。該工具支持三種邏輯形式的性質(zhì)描述：自動機(jī)[6-7]、正則表達(dá)式[8-9]和線性時序邏輯[10]。監(jiān)控器的監(jiān)控算法是通過自動機(jī)來進(jìn)行操作的。最后對源代碼進(jìn)行插樁的插樁器，主要結(jié)合形式化規(guī)約文件和Clang編譯器，對C程序的源代碼中對應(yīng)的規(guī)約文件切點進(jìn)行插樁，最后生成包含監(jiān)控器的新C程序。文中在該原型工具的基礎(chǔ)之上引入多線程技術(shù)，實現(xiàn)該原型工具的優(yōu)化。主要工作如下：提出多監(jiān)控器運(yùn)行時驗證并行化原理；使用插樁技術(shù)對多線程監(jiān)控器進(jìn)行劃分；使用多線程交互的方法進(jìn)行交互；實現(xiàn)了原型工具的優(yōu)化，并進(jìn)行了對比實驗。

2 多監(jiān)控器運(yùn)行時驗證并行化原理

本節(jié)是基于形式化語言的程序運(yùn)行時驗證的優(yōu)化，將多線程的技術(shù)應(yīng)用到原型工具M(jìn)ovec，提高工具的性能。原型工具對于多監(jiān)控器的處理是通過將監(jiān)控器的監(jiān)控事件和響應(yīng)操作直接插樁到源代碼，目標(biāo)程序運(yùn)行到觸發(fā)事件時，調(diào)用響應(yīng)操作，操作結(jié)束之后繼續(xù)執(zhí)行目標(biāo)程序。假設(shè)目標(biāo)程序運(yùn)行時間為main_time，監(jiān)控器1,2,…,n運(yùn)行的時間是m_time[1]，m_time[2]，…，m_time[n]。那么插樁之后新的程序運(yùn)行的時間為sum_time：

(1)

為了實現(xiàn)多線程程序的并行化，本節(jié)提出了運(yùn)行時驗證多監(jiān)控器下的并行方法。具體過程如下：第一步，將監(jiān)控器的響應(yīng)操作與目標(biāo)程序分離。將原來插樁到源代碼的監(jiān)控器驗證函數(shù)分離到創(chuàng)建的線程中。第二步，將目標(biāo)程序要驗證的事件信息進(jìn)行記錄。將監(jiān)控器需要驗證的事件信息存儲到指定的數(shù)據(jù)結(jié)構(gòu)。第三步，進(jìn)行事件序列的任務(wù)劃分。解決多線程負(fù)載平衡問題，防止出現(xiàn)一個處理器一直處于運(yùn)行狀態(tài)，其他處理器空閑的情況。第四步，將各個監(jiān)控器與線程進(jìn)行綁定。通過設(shè)置線程親和性，將監(jiān)控器和具體的邏輯線程ID進(jìn)行綁定，防止出現(xiàn)操作系統(tǒng)隨機(jī)調(diào)用邏輯線程的情況。第五步，多線程監(jiān)控器程序和目標(biāo)程序并行運(yùn)行。

采用以上并行方法并結(jié)合Clang編譯器[11]對原型工具M(jìn)ovec進(jìn)行改進(jìn)。改進(jìn)之后的Movec對目標(biāo)程序處理之后生成新程序的運(yùn)行過程由單線程的串行執(zhí)行變成了并行執(zhí)行，如圖1所示。

圖1 多監(jiān)控器工具框架和對應(yīng)的程序狀態(tài)

3 運(yùn)行時驗證的多線程運(yùn)行

3.1 多線程監(jiān)控器的任務(wù)劃分

在監(jiān)控器分配到各個線程并行運(yùn)行的條件下，需要采用合理的方法去解決線程之間的負(fù)載平衡問題。首先介紹一下負(fù)載平衡問題對多線程程序的重要性。在多核[12-14]的并行機(jī)上，由于在多線程程序中，整個程序的運(yùn)行時間往往取決于運(yùn)行時間最長的線程。如果操作系統(tǒng)在一個處理器分配的任務(wù)數(shù)量過多，而其他處理器空閑，這就會導(dǎo)致多線程程序執(zhí)行性能的嚴(yán)重下降。

對于原型工具M(jìn)ovec，監(jiān)控器直接通過插樁的方式直接插樁到待檢測程序，文中采用多線程技術(shù)將監(jiān)控器和待檢測程序分離，并將多監(jiān)控器分配到多處理器上實現(xiàn)并行運(yùn)行。但是在并行機(jī)上處理器個數(shù)有限的情況下，有以下兩種情況，如圖2所示。

圖2 多監(jiān)控器事件序列分配

情況一：目標(biāo)程序運(yùn)行時間main_time≤Max{corea_time，coreb_time，corec_time，cored_time},總運(yùn)行時間為：

sum_time=Max{corea_time，coreb_time，corec_time，cored_time}

(2)

情況二：目標(biāo)程序運(yùn)行時間main_time>Max{corea_time，coreb_time，corec_time，cored_time},總運(yùn)行時間為：

sun_time=main_time

(3)

3.2 多線程監(jiān)控器與待檢測程序的線程交互

在完成了多線程的任務(wù)分配問題之后，多線程還涉及到的問題就是資源的共享問題以及線程間通信。下面將對以上兩個問題進(jìn)行具體的分析和解決。

線程資源共享問題指的是多個線程對要訪問的資源只保存一份，多個線程對該資源進(jìn)行訪問，是一種并發(fā)進(jìn)行的同步機(jī)制。文中流程如下：首先目標(biāo)程序?qū)⒊绦蛑械氖录蛄写鎯υ谝粋€鏈表之中，該鏈表就是一個共享的資源；然后多個監(jiān)控器從鏈表之中讀取相應(yīng)的數(shù)據(jù)；最后每個監(jiān)控器并行運(yùn)行，處理各自對應(yīng)的事件序列。從上可知這是一個單生產(chǎn)者多消費(fèi)者的多線程問題。其中目標(biāo)程序為生產(chǎn)者線程進(jìn)行數(shù)據(jù)收集并存儲到鏈表(即數(shù)據(jù)生產(chǎn))，監(jiān)控器則是作為消費(fèi)者線程進(jìn)行數(shù)據(jù)處理(即數(shù)據(jù)消費(fèi))。事件序列數(shù)據(jù)通過線程間共享內(nèi)存塊進(jìn)行存儲。其中線程間共享的內(nèi)存塊主要由以下幾種：堆、全局變量、靜態(tài)變量、文件、棧、寄存器等。文中采用的是堆內(nèi)存進(jìn)行共享。但是單生產(chǎn)者多消費(fèi)者模型會帶來這么一個問題，如果生產(chǎn)者存放數(shù)據(jù)的速度遠(yuǎn)遠(yuǎn)大于消費(fèi)者消耗數(shù)據(jù)的速度，就可能會引起消費(fèi)者處理數(shù)據(jù)之前生產(chǎn)者多次重寫了之前的結(jié)果，反之，消費(fèi)者線程消耗數(shù)據(jù)的速度遠(yuǎn)遠(yuǎn)大于生產(chǎn)者生產(chǎn)數(shù)據(jù)的速度，就會造成消費(fèi)者提取還沒有存放的數(shù)據(jù)，或者是造成同時讀寫的競爭問題。

文中通過設(shè)計自旋鎖和鏈表解決了線程共享問題。下面的消費(fèi)者線程對應(yīng)的是監(jiān)控器所在的線程，生產(chǎn)者線程對應(yīng)的是目標(biāo)程序線程。主要思想是：讓消費(fèi)者線程訪問的節(jié)點不要超過生產(chǎn)者存放的節(jié)點。生產(chǎn)者程序初始化鏈表時，將producer_head和producer_tail同時指向頭節(jié)點并將監(jiān)控器的頭節(jié)點也指向鏈表的頭，新的節(jié)點是在producer_tail節(jié)點之后進(jìn)行插入，插入成功之后producer_tail節(jié)點后移，并且在鏈表的最后插入一個空節(jié)點，保證最后一個數(shù)據(jù)節(jié)點被消費(fèi)者訪問。消費(fèi)者線程則是通過消費(fèi)者對應(yīng)的頭節(jié)點進(jìn)行鏈表訪問。因為訪問只是讀取數(shù)據(jù)不涉及資源競爭，所以可以并行運(yùn)行。但是為了防止消費(fèi)者程序讀取還沒有插入好的的新節(jié)點，設(shè)置了一個自旋鎖。通過一個while語句的循環(huán)，循環(huán)的判斷條件是消費(fèi)者的head節(jié)點是否等于生產(chǎn)者的tail節(jié)點，如果相同就需要將消費(fèi)者線程阻塞，從而防止消費(fèi)者訪問沒存儲的數(shù)據(jù)。這個自旋鎖有效保證了多個消費(fèi)者線程在訪問共享鏈表時，只會訪問生產(chǎn)線程tail節(jié)點之前的鏈表節(jié)點，保證了消費(fèi)者并行的正確性。

由于消費(fèi)線程在訪問共享資源時涉及到了阻塞的情況，這就需要對它們進(jìn)行喚醒操作。文中使用信號量的方式來喚醒，這就是線程間通信問題。線程間通信指的是主線程和子線程、子線程與子線程進(jìn)行相互之間的通信。線程間必須有個特定的信息傳遞渠道，文中使用共享的鏈表作為信息傳輸渠道，并采用主線程去喚醒阻塞線程的方法。具體步驟如下：首先存儲事件信息；然后喚醒所有子線程，由于消費(fèi)者線程中喚醒之后，線程會從上次阻塞的位置之后開始運(yùn)行，也就是wait()方法后開始，所以線程會再次進(jìn)行自旋鎖的判斷，從而保證了消費(fèi)者線程訪問數(shù)據(jù)的安全性；最后如果自旋鎖的條件不滿足，消費(fèi)者線程就可以進(jìn)行數(shù)據(jù)的讀取和訪問，否則消費(fèi)者線程會被再次阻塞。

4 多核監(jiān)控器的運(yùn)行時驗證工具實現(xiàn)

4.1 數(shù)據(jù)結(jié)構(gòu)設(shè)計

共享資源鏈表結(jié)構(gòu)如圖3所示。

其中action為目標(biāo)動作，即監(jiān)控器的響應(yīng)操作；trace_node類型為鏈表的節(jié)點信息；通過action_id判斷當(dāng)前目標(biāo)動作是屬于哪一個監(jiān)控器；action聯(lián)合類型可以達(dá)到特定的目標(biāo)動作對應(yīng)特定的類型存儲，其中的特定存儲類型由目標(biāo)動作函數(shù)決定，如action_1類型，pfunc為函數(shù)指針，join_poin類型記錄了切點的上下文，其余是函數(shù)指針剩下的參數(shù)。

4.2 插樁實現(xiàn)

文中的工具采用的是面向方面編程的思想。其中面向方面的程序包括兩部分，一是實現(xiàn)軟件系統(tǒng)核心關(guān)注點的基礎(chǔ)代碼，二是軟件系統(tǒng)橫切關(guān)注點的代碼。面向方面編程由接入點模型、切入點、通知和方面組成。接入點指的是程序結(jié)構(gòu)中特定位置或運(yùn)行過程中的特定時刻；切點指的是符合條件的連接點集合；通知指在切入點描述的位置所做的響應(yīng)動作；方面則是由若干個關(guān)注點集合構(gòu)成，其中的關(guān)注點是由切入點和通知共同組成。

typedef struct { void(*pfunc)(struct join_point *tjp,size_t size,void * address); struct join_point tjp; size_t size; void *address;} action_1;typedef union { action_1 a1;action_2 a2; action_3 a3;action_4 a4;} action;struct trace_node{ int property_id; int action_id; action act; struct trace_node *next;};

圖3 共享資源鏈表結(jié)構(gòu)

主要思想是第一步：進(jìn)行切點的匹配，重寫切點操作，記錄響應(yīng)操作，插樁新的切點操作函數(shù)；第二步：源代碼插樁，創(chuàng)建新的線程，讀取記錄的信息并執(zhí)行響應(yīng)操作。本節(jié)詳細(xì)介紹這兩步的具體實現(xiàn)方法。

第一步實現(xiàn)。在待監(jiān)控目標(biāo)程序中，切入點可能是函數(shù)調(diào)用、函數(shù)指針調(diào)用、函數(shù)的執(zhí)行、變量的賦值、變量的取值、函數(shù)執(zhí)行流中返回值變量命名等。為了將切點進(jìn)行重寫以及對響應(yīng)操作進(jìn)行記錄，通過遍歷抽象語法樹，實現(xiàn)切點的具體插樁動作。表1為不同類型的切點對應(yīng)的抽象語法樹類型。

表1 切點類型對應(yīng)的抽象語法結(jié)構(gòu)

下面以函數(shù)調(diào)用切點為例介紹插樁的具體方法。由于Clang編譯器訪問抽象語法樹中的CallExpr類型節(jié)點是通過RecursiveASTVisitor的VisitCallExpr方法，所以通過重寫VisitCallExpr方法完成插樁。具體算法如圖4所示。

切入點函數(shù)調(diào)用插樁算法輸入:抽象語法樹中的CallExpr類型節(jié)點輸出:插樁函數(shù)后的新程序1:for(遍歷所有的監(jiān)控器){2:for(遍歷監(jiān)控器的里切點){3:if(函數(shù)調(diào)用切入點匹配成功){4:獲取切入點調(diào)用函數(shù)聲明;5:獲取切入點調(diào)用函數(shù)返回值類型;6:獲取存儲語法樹節(jié)點代碼片段的存儲器(存儲新函數(shù)的定義);7:將原來的切入點函數(shù)調(diào)用替換成新函數(shù)調(diào)用;8:構(gòu)造新函數(shù){9:新函數(shù)命名,函數(shù)參數(shù)構(gòu)造;10:函數(shù)體內(nèi)的初始化(記錄切點函數(shù)的上下文信息,參數(shù)和參數(shù)類型);11:獲取監(jiān)控器中的響應(yīng)操作條件;12:記錄響應(yīng)操作的函數(shù)名和函數(shù)參數(shù)到圖3的共享資源鏈表;13:調(diào)用原來的切入點函數(shù);14:}15:}16:}17:}

圖4 切入點函數(shù)調(diào)用插樁算法

通過這樣一個插樁算法可以對函數(shù)調(diào)用的切點進(jìn)行處理。對于其他類型的切點，文中采用類似的插樁方法分別對RecursiveASTVisitor的VisitFunctionDecl方法、VisitUnaryOperator方法、VisitCompoundAssignOperator方法、VisitVarDecl方法、VisitBinaryOperator方法、VisitDeclRefExpr方法進(jìn)行重寫，完成了切點信息記錄、響應(yīng)函數(shù)與目標(biāo)程序的分離。

第二步實現(xiàn)。要在目標(biāo)程序中加入線程創(chuàng)建，線程相關(guān)的變量定義聲明以及線程創(chuàng)建調(diào)用的執(zhí)行函數(shù)。其中線程創(chuàng)建和相關(guān)變量定義聲明通過VisitFunctionDecl方法。

對創(chuàng)建線程執(zhí)行的函數(shù)，將調(diào)用線程調(diào)用函數(shù)的定義插樁到main函數(shù)聲明的位置之前，函數(shù)定義的內(nèi)部由以下幾部分組成：

(1)3.2節(jié)中介紹的自旋鎖；

(2)根據(jù)3.1節(jié)中的任務(wù)劃分方式進(jìn)行監(jiān)控器事件序列的劃分；

(3)通過讀取共享資源中節(jié)點的action_id來判斷是否進(jìn)行監(jiān)控函數(shù)的調(diào)用，如果是指定的action_id則監(jiān)控函數(shù)執(zhí)行，否則節(jié)點后移；

(4)進(jìn)行訪問節(jié)點指針和空指針比較，如果為空，結(jié)束線程。

5 實驗分析

文中將多線程技術(shù)應(yīng)用到多監(jiān)控器與單目標(biāo)程序的運(yùn)行時監(jiān)控模式中，從而將原本串行運(yùn)行的程序轉(zhuǎn)化成并行運(yùn)行的多線程程序。實驗對象是單目標(biāo)程序與6個性質(zhì)的監(jiān)控器。6個監(jiān)控器的事件序列個數(shù)分別是：40003、40003、40003、4000、40003、20002。監(jiān)控的性質(zhì)分別是用正則表達(dá)式規(guī)約的函數(shù)執(zhí)行順序(ere: f1+f2+f1f2f3)、用正則表達(dá)式規(guī)約的內(nèi)存申請釋放(ere: (malloc free)* malloc end;)；六個性質(zhì)都是用正則表達(dá)式進(jìn)行規(guī)約，其中5個性質(zhì)是用來規(guī)約函數(shù)調(diào)用的順序，第6個性質(zhì)是用來判斷是否存在目標(biāo)程序、是否存在內(nèi)存沒有釋放。切點分別是malloc函數(shù)調(diào)用、free函數(shù)調(diào)用、main函數(shù)執(zhí)行之后以及關(guān)于被規(guī)約執(zhí)行順序的函數(shù)調(diào)用。實驗結(jié)果如圖5所示。圖中記錄的時間值都是進(jìn)行10次統(tǒng)計后取平均值的方式獲取的。

圖5 優(yōu)化實驗數(shù)據(jù)

圖中橫坐標(biāo)分別表示使用了幾個線程去驗證6個事件序列。如果使用一個線程去運(yùn)行所有事件序列的監(jiān)控函數(shù)就是一種串行結(jié)構(gòu)，所以使用的時間最長。但是隨著線程個數(shù)的增加，時間并不是一個遞減的趨勢，結(jié)果和預(yù)期的不同。這是因為該實驗的硬件平臺是四個處理器，但是支持超線程模式，一個處理器可以同時運(yùn)行兩個線程。當(dāng)超過4個線程時，就會出現(xiàn)兩個線程競爭同一個處理器資源的情況。同一時刻一個處理器也只是在運(yùn)行兩個線程中的一個。所以當(dāng)同時運(yùn)行4個線程時，才是真正意義上的并行運(yùn)算。從圖5可知，在3個線程運(yùn)行監(jiān)控器的事件序列與一個主線程的情況下，運(yùn)行的時間最短。在最優(yōu)情況下，對于該實驗的數(shù)據(jù)進(jìn)行分析。插樁后程序運(yùn)行的總時間由原來的51.51 s變?yōu)?3.53 s。程序的性能提升了45%。通過將工具優(yōu)化之前的串行執(zhí)行時間數(shù)據(jù)和優(yōu)化之后的并行運(yùn)行時間數(shù)據(jù)進(jìn)行對比，得出采用了多線程技術(shù)后的工具性能提升明顯。優(yōu)化之后的原型工具M(jìn)ovec在進(jìn)行多個監(jiān)控器監(jiān)控時，插樁之后的程序性能的提升效果顯著。

6 結(jié)束語

本文利用多核并行技術(shù)[15-17]，對原型工具M(jìn)ovec進(jìn)行優(yōu)化。通過將串行程序的監(jiān)控器分配到多線程的方式，Clang編譯器的插樁技術(shù)和多核任務(wù)分配方法，實現(xiàn)了Movec原型工具的優(yōu)化。首先介紹了多監(jiān)控器與單目標(biāo)程序情況下，將插樁之后程序并行化的原理。然后主要介紹了多線程程序中負(fù)載均衡處理方法和線程間線程通信的方式。

最后，通過具體的插樁算法實現(xiàn)了原型工具針對多監(jiān)控器與單目標(biāo)程序的并行化，實現(xiàn)了插樁之后生成新程序的并行化運(yùn)行方法。并將優(yōu)化之后的Movec與沒有改進(jìn)之前的工具進(jìn)行實驗數(shù)據(jù)對比，實驗結(jié)果表明采用并行化的運(yùn)行方法具有很好的效果。今后進(jìn)一步的工作包括下面幾個方面：

(1)結(jié)合靜態(tài)分析技術(shù)，減少C程序中不必要的一些插樁。

(2)在原有的數(shù)據(jù)結(jié)構(gòu)存儲結(jié)構(gòu)上進(jìn)行優(yōu)化，提高數(shù)據(jù)查找的速度。

(3) 將源代碼的插樁過程分配到不同的處理器核心上，提高M(jìn)ovec工具編譯運(yùn)行的性能。