中斷驅(qū)動型航天嵌入式軟件原子性違反檢測方法

于婷婷 李 超 王博祥 陳 睿 江云松

1（北京軒宇信息技術有限公司 北京 100190）

2（北京控制工程研究所 北京 100190）

嵌入式軟件的可信性對航天任務成敗至關重要，即使一個微小的軟件缺陷也可能導致重要任務的失敗.航天嵌入式軟件廣泛采用中斷驅(qū)動的并發(fā)機制，與硬件頻繁地進行交互并實時地響應外界事件[1].當一個系統(tǒng)中的大量處理都由中斷發(fā)起時，我們稱這類系統(tǒng)為中斷驅(qū)動型系統(tǒng)[2].

中斷驅(qū)動型嵌入式軟件使用大量的共享數(shù)據(jù)來實現(xiàn)主任務和中斷，以及不同中斷之間的通信和數(shù)據(jù)交互.如圖1 所示，航天嵌入式軟件通常由主任務和多個中斷服務程序構成.主任務的結構是一個無限循環(huán)，等待中斷的觸發(fā)進行相應的操作.中斷由來自軟件或硬件（如定時器、外設和I/O 端口）的中斷信號觸發(fā)，例如由內(nèi)部事件及“異常”，或由接收字節(jié)的串行端口控制器觸發(fā).然后，處理器通過掛起其他當前活動、保存其狀態(tài)并執(zhí)行中斷處理程序來響應當前事件.待中斷處理完成后，處理器恢復其正?；顒?由于中斷可能在任意時刻發(fā)生并搶占正在執(zhí)行的計算，因此，如果對共享數(shù)據(jù)的訪問沒有被恰當?shù)赝?，則不確定的中斷搶占可能會導致數(shù)據(jù)訪問沖突，引起嚴重的安全問題.據(jù)中國空間技術研究院軟件產(chǎn)品保證中心統(tǒng)計[3]，在航天器總裝集成測試（assembly，integration &test，AIT）階段發(fā)現(xiàn)的軟件質(zhì)量問題中，約80%為中斷相關的并發(fā)缺陷.這些缺陷在經(jīng)過各種嚴格的軟件測試后仍然被遺漏，是航天嵌入式軟件開發(fā)中最難以消除的缺陷類型之一.根據(jù)文獻[4]對航天嵌入式軟件并發(fā)缺陷的研究，原子性違反是中斷并發(fā)缺陷中最突出的一類缺陷模式.這種模式指的是程序員對共享數(shù)據(jù)連續(xù)多次訪問的原子性執(zhí)行期望由于中斷搶占而遭到破壞，導致非預期的程序行為.

Fig.1 Interrupt-driven model in aerospace embedded software圖1 航天嵌入式軟件的中斷驅(qū)動模型

原子性違反檢測是國內(nèi)外研究的熱點，已有方法大多面向多線程程序[5-14]，但這些方法不能直接應用于中斷驅(qū)動型航天嵌入式軟件，這是由于中斷驅(qū)動型航天嵌入式軟件與多線程程序在并發(fā)模型和編程范式方面存在顯著差異.例如，任務與中斷之間或中斷與中斷之間具有非對稱搶占關系，而線程之間可以互相搶占，異步并發(fā)事件及其優(yōu)先級之間的隱式依賴關系，使用于檢測競爭的happens-before 關系復雜化，這導致適用于2 類程序的缺陷檢測方法存在差異；中斷驅(qū)動型航天嵌入式軟件一般缺乏底層并發(fā)編程框架，經(jīng)常采用基于自定義標志變量的同步方式，而多線程程序多采用標準并發(fā)控制原語，自定義標志變量的存在極易導致檢測結果存在大量誤報；此外，中斷驅(qū)動型航天嵌入式軟件依賴大量的內(nèi)存映射I/O 地址與外設進行交互，若不能恰當識別這些數(shù)據(jù)，將使檢測結果存在漏報.這些差異對檢測方法的有效性具有決定性作用，直接應用針對多線程程序的檢測方法面臨檢測結果不精確的問題.

目前，僅有少量工作針對中斷驅(qū)動型程序中的原子性違反[4,15].文獻[4]采用靜態(tài)分析的方法，可擴展到工業(yè)規(guī)模的嵌入式軟件，但存在較多誤報；文獻[15]采用程序模型檢驗方法，但僅能擴展到百行規(guī)模的程序.一方面，文獻[4,15]都無法同時實現(xiàn)高精度和高可擴展性；另一方面，中斷驅(qū)動型航天嵌入式軟件的硬件依賴性強且多采用裸機編程，其并發(fā)缺陷的表現(xiàn)形式具有領域相關特征，且已有方法的有效性都未經(jīng)過真實航天嵌入式軟件的評估.

本文面向真實中斷驅(qū)動型嵌入式軟件中的原子性違反，研究精確且高效的靜態(tài)檢測方法.首先對2009—2022 年中國空間技術研究院第三方評測機構報告的82 個原子性違反缺陷進行特征研究，獲得該類缺陷在訪問交錯模式、共享數(shù)據(jù)訪問方式、訪問粒度等3 方面的表現(xiàn)特征.在此基礎上，提出了一個精確、高效的靜態(tài)缺陷檢測方法intAtom-S.該方法的核心思想是逐階段地采用更精確的技術消除不可行路徑導致的誤報，從而同時實現(xiàn)更少的誤報和更好的性能.intAtom-S 主要分為3 個階段：1）基于一個由數(shù)值不變式參數(shù)化的細粒度內(nèi)存訪問模型，引入基于規(guī)則的方法剔除標志變量訪問，并采用抽象解釋進行精確的共享數(shù)據(jù)分析，以識別程序中的所有可能造成缺陷的共享訪問點.該分析能夠排除標志變量訪問，將共享數(shù)據(jù)訪問粒度精確至數(shù)組元素，并可識別共享內(nèi)存映射I/O 地址.2）使用輕量級數(shù)據(jù)流分析技術匹配符合交錯模式的所有并發(fā)3 次訪問序作為潛在的原子性違反缺陷候選.3）采用基于路徑條件的約束求解對缺陷候選中的串行訪問對和并發(fā)3次訪問序進行路徑可行性分析，逐步消除誤報，得到最終的原子性違反結果.

本文實現(xiàn)了一個面向C 程序的中斷原子性違反靜態(tài)檢測工具intAtom-S，并在基準測試集Racebench 2.1[16]和8 個真實航天嵌入式軟件上進行了實驗評估.結果表明，與當前的研究工作相比，intAtom-S 的誤報率降低了72%，同時檢測速度提高了3 倍.此外，intAtom-S 可以非常快地完成對真實航天嵌入式軟件的分析，發(fā)現(xiàn)了23 個經(jīng)開發(fā)人員確認的錯誤，且平均誤報率僅為8.9%.本文的部分內(nèi)容已發(fā)表于文獻[17]和[18],相比已發(fā)表內(nèi)容，intAtom-S 基于更精確、更細粒度的共享數(shù)據(jù)識別結果，可以處理數(shù)組元素訪問、標志變量訪問導致的誤報，顯著提高了缺陷檢測的精度.

本文的主要貢獻包括3 個方面：

1）對來自真實航天嵌入式軟件的82 個并發(fā)缺陷進行了全面、深入的實證研究，揭示了航天嵌入式軟件原子性違反的表現(xiàn)形式特征.

2）提出了一個精確、高效的中斷驅(qū)動型程序原子性違反靜態(tài)檢測方法intAtom-S.

3）在基準測試集和真實航天嵌入式軟件上進行實驗評估，驗證了本文方法的有效性.

1 原子性違反特征研究

本節(jié)首先介紹原子性違反模式并給出真實案例；然后，對本文缺陷特征的研究方法進行闡述；最后，給出特征研究結果及對應的方法.

1.1 原子性違反缺陷模式

原子性違反缺陷模式指的是程序員對共享數(shù)據(jù)的連續(xù)多次訪問具有原子性期望,而其他并發(fā)流的搶占執(zhí)行打破了這種期望，導致非預期的程序行為.對于中斷驅(qū)動型程序，該類缺陷主要發(fā)生在對單個共享變量的并發(fā)訪問中.由于程序員通常以順序思維進行程序設計，往往會假設對同一變量的順序訪問是原子執(zhí)行的，容易忽視中斷搶占及其干擾，但程序在實際執(zhí)行時并不能確保這種原子性[4,19].

圖2 所示為一個典型的原子性違反案例，該案例來自某航天控制軟件.主任務循環(huán)執(zhí)行mode_manage函數(shù)并周期性地更新變量v_error_max的值，使其表示fabsf(set_loop-tyro_L)的最大值.若中斷在S1之后、S3之前發(fā)生搶占，則S2在這2 次訪問之間執(zhí)行，導致tyro_L的值將在S2中被改寫.若此時改寫之后的tyro_L不再使fabs f(set_loop?tyro_L)的值滿足S1的條件語句，就會造成v_error_max并不是真實的最大值.變量v_error_max用于重要的航天器控制任務，此缺陷將會引發(fā)嚴重的后果.

1.2 缺陷特征研究方法

Fig.2 An example of typical atomicity violation圖2 一個典型的原子性違反案例

中國空間技術研究院負責研制我國衛(wèi)星、飛船和深空探測器等各類航天器，包括中國空間站、天問一號火星探測器、嫦娥五號月球探測器和北斗導航衛(wèi)星等.本文以2009—2022 年中國空間技術研究院第三方評測機構軟件問題庫作為缺陷的數(shù)據(jù)來源.該問題庫包含超過28 000 個軟件缺陷，這些缺陷在經(jīng)過各種開發(fā)方測試后依舊遺留，代表了航天嵌入式軟件研制過程中最具挑戰(zhàn)性的可信問題.

在案例分析過程中，本文首先通過“中斷”“原子性”“沖突”“競爭”等關鍵字進行檢索和挖掘，得到了424 個相關缺陷案例.然后，為了篩選出具有完整的、可供進一步分析的原子性違反缺陷案例，逐一地對424 個案例進行核查.核查的標準為：1）案例包含詳細的問題報告單、原始代碼和修復后版本的代碼；2）對源代碼進行分析和理解后，確認該缺陷案例屬于原子性違反.最終，獲得了82 個信息完整的缺陷案例.這個選擇過程保證了最終研究的缺陷案例集具有代表性.

這些缺陷來源于各種不同型號的航天嵌入式軟件，覆蓋了近十年我國研制和發(fā)射的各類空間飛行器中的關鍵嵌入式軟件，包括航天器控制軟件、航天器綜合電子軟件、航天器中央數(shù)據(jù)單元軟件以及各類遙測遙控軟件等；此外，這些軟件的硬件運行環(huán)境涉及各種不同類型的處理器，如80C32，TSC695F，BM3803 等，這保證了實證研究的公平性和多樣性.

進一步，本文對所有收集的案例逐個進行研究，總結了造成原子性違反的共享數(shù)據(jù)訪問交錯模式，并對發(fā)生缺陷的共享數(shù)據(jù)的訪問方式和訪問粒度進行了分析和統(tǒng)計.

1.3 缺陷表現(xiàn)特征

本節(jié)對實證研究獲得的共享數(shù)據(jù)訪問交錯模式、訪問方式和訪問粒度等原子性違反缺陷表現(xiàn)特征進行了說明.

1）共享數(shù)據(jù)訪問交錯模式.本文借用可序列化[20]的思想，總結形成了4 種造成原子性違反的訪問交錯模式，如表1 所示，這些模式刻畫了中斷驅(qū)動型程序中的原子性違反.每個訪問交錯(ep,er,ec)都可以通過一次執(zhí)行中對同一個共享數(shù)據(jù)的3 次訪問描述.其中，ep和ec為來自主任務或低優(yōu)先級中斷isrl的本地串行訪問對，而er為來自另一個高優(yōu)先級中斷isrh的遠程交錯訪問.

Table 1 Access Interleaving Pattern of Atomicity Violation表1 原子性違反的訪問交錯模式

2）原子區(qū)范圍.發(fā)生缺陷的本地串行訪問對在源代碼上的距離范圍分布如圖3 所示，最小范圍為1 行（例如2 次訪問在同一行代碼中，如a++），最大范圍為31 行，平均范圍為5 行.其中，24 個訪問對位于同一行，17 個訪問對相鄰（范圍為2 行）.此外，有8 個訪問對位于循環(huán)結構中，6 個訪問對作為函數(shù)參數(shù)被訪問.特別的是，所有的訪問對都在同一個函數(shù)中，或作為同一主調(diào)函數(shù)內(nèi)不同被調(diào)函數(shù)的參數(shù).

Fig.3 Distribution of atomic region range圖3 原子區(qū)范圍分布

3）中斷嵌套層數(shù).在中斷驅(qū)動型程序中，并發(fā)交錯的數(shù)量會隨著中斷的數(shù)量呈指數(shù)級增長，此外中斷嵌套的存在將加劇此增長速度.然而，本文研究的82 個缺陷案例中，觸發(fā)這些缺陷所涉及的中斷數(shù)量都不超過2 個.其中，69 個缺陷發(fā)生在主任務和中斷之間；9 個發(fā)生在中斷與中斷之間；4 個發(fā)生在主程序和嵌套的中斷之間.

4）共享數(shù)據(jù)訪問方式.如表2 所示，在發(fā)生缺陷的共享數(shù)據(jù)中，有60%是通過全局變量名進行直接訪問的.在全局變量訪問方式中，程序直接將變量所在內(nèi)存單元的值取出并進行運算；有32%通過指針解引用進行間接的訪問.8%的缺陷發(fā)生于訪問內(nèi)存映射I/O（memory mapped I/O，MMIO）時.在中斷驅(qū)動型嵌入式軟件中，MMIO 是一種典型的數(shù)據(jù)類型，廣泛用于表示硬件數(shù)據(jù)資源，例如0x40008000 代表某個外設寄存器的內(nèi)存映射地址，程序可以通過*（（unsigned char*）0x40008000）對該寄存器進行讀寫.

Table 2 Access Modes and Access Granularities on Shared Data表2 共享數(shù)據(jù)訪問方式與訪問粒度

5）共享數(shù)據(jù)訪問粒度.即使是對同一塊內(nèi)存單元，程序也可能通過不同的訪問粒度進行訪問[18].如表2 所示，在研究的案例中，嵌入式軟件對共享內(nèi)存的訪問存在各種不同粒度.46%的共享內(nèi)存為整體訪問，即通過變量名對變量指代的整個內(nèi)存區(qū)域進行訪問；26%的共享內(nèi)存為通過數(shù)組下標對元素進行訪問；17%的共享內(nèi)存為通過結構體對成員進行訪問；11%的共享內(nèi)存需要精確到位訪問.此外，在所有的內(nèi)存訪問中，9%的共享內(nèi)存訪問帶有非常量的偏移量，例如數(shù)組元素BRCS T_buf[i]，其偏移量需要通過計算變量i得到，使得這些內(nèi)存地址難以靜態(tài)確定.

缺陷表現(xiàn)特征研究表明，航天嵌入式軟件中，程序員具有原子性意圖的串行訪問在源代碼上具有較近的距離，可以通過限定原子區(qū)范圍對原子區(qū)進行推斷，從而降低計算開銷并減少誤報.對原子性違反的檢測可以通過成對（主任務和中斷，或中斷與中斷）的方式進行，從而以損失較低精度的代價實現(xiàn)對絕大部分缺陷的高效檢測.對共享數(shù)據(jù)的訪問通常涉及訪問方式和粒度的復雜組合，這增加了共享數(shù)據(jù)分析的難度.若共享數(shù)據(jù)分析只關注數(shù)組對象而不能區(qū)分數(shù)組元素，將會導致大量誤報；若不能識別MMIO 類型的共享數(shù)據(jù)，則會導致漏報.因此，為了提高缺陷檢測的精度，檢測工具需要精確的共享數(shù)據(jù)分析.

2 intAtom-S

本文基于原子性違反特征研究的結果，提出intAtom-S.圖4 所示為intAtom-S 的框 架.該框架主要包括3 個階段：基于抽象解釋的共享分析（見2.1 節(jié)）、訪問交錯模式匹配（見2.2 節(jié)）、不可行路徑裁剪（見2.3 節(jié)）.

首先，intAtom-S 精確地分析程序中的共享數(shù)據(jù).intAtom-S 構建了一個數(shù)值不變式參數(shù)化的細粒度內(nèi)存訪問模型；采用區(qū)間抽象域和同余抽象域的約化積（reduced product of interval and congruence，RPIC）[21]進行基于抽象解釋的數(shù)值分析，以獲得采用內(nèi)存訪問模型表示的共享數(shù)據(jù)地址中的數(shù)值不變式，從而達到精確識別的目的.在文獻[18]的基礎上，intAtom-S引入基于規(guī)則的方法剔除標志變量，僅識別那些會導致缺陷的共享數(shù)據(jù)，這對進一步精化缺陷檢測結果至關重要.

Fig.4 intAtom-S framework圖4 intAtom-S 框架

其次，intAtom-S 使用輕量級數(shù)據(jù)流分析技術匹配符合4 種交錯模式的所有并發(fā)3 次訪問序作為潛在的原子性違反候選.intAtom-S 使用過程間分析并采用“工作單元”的概念[22]識別isrl中的串行訪問對.在此基礎上，結合來自isrh的訪問進行模式匹配以識別出屬于訪問交錯模式（表1）的并發(fā)3次訪問序.這些3 次訪問序是輸入到后續(xù)步驟的原子性違反候選.

最后，對缺陷候選采用基于路徑條件的約束求解.通過對串行訪問對和并發(fā)3 次訪問序進行路徑可行性分析，逐步消除沒有違反程序員預期和實際不可能發(fā)生的2 類誤報，得到最終的原子性違反結果：1）依次檢查isrl中2 個串行訪問之間的路徑可行性，如果不可行，表明程序員對該串行訪問沒有一致性預期，并發(fā)3 次訪問序不會造成原子性違反，因此將該類候選排除.2）intAtom-S 通過一個模塊化、路徑敏感的分析，消除在實際執(zhí)行中由于約束條件無法滿足而不可能真實發(fā)生的并發(fā)3 次訪問序.為了縮減交錯空間和提高分析效率，本文引入了2 個策略：1）intAtom-S 為每個中斷構建一個符號化的摘要，幫助進行模塊化的路徑裁剪，以消除不可行的交錯.2）intAtom-S 采用代表性搶占點策略，在不損失精度的情況下縮減交錯空間.

相比文獻[17]，intAtom-S 基于更精確、更細粒度且剔除標志變量訪問后的共享數(shù)據(jù)識別結果，可以處理數(shù)組元素訪問、標志變量訪問導致的誤報，將顯著提高精度.

2.1 基于抽象解釋的共享分析

根據(jù)缺陷特征，intAtom-S 提出一種精確的共享數(shù)據(jù)靜態(tài)分析方法.該方法主要包括：

1）參數(shù)化的內(nèi)存訪問模型.為了應對航天嵌入式軟件中共享數(shù)據(jù)訪問通常涉及的訪問方式和粒度的復雜組合，本文通過參數(shù)化的內(nèi)存訪問模型對不同粒度的共享數(shù)據(jù)訪問進行統(tǒng)一刻畫.

2）基于抽象解釋的數(shù)值分析.使用RPIC 對每一個并發(fā)流進行基于抽象解釋的數(shù)值分析，計算內(nèi)存訪問模型中偏移量的數(shù)值不變式.

3）共享訪問點識別.采用基于規(guī)則的方法剔除標志變量訪問，進而通過對不同并發(fā)流（主任務、各個中斷）之間的數(shù)據(jù)訪問點的數(shù)值抽象域進行“與操作”，識別出會導致缺陷的共享數(shù)據(jù)訪問點.

2.1.1 參數(shù)化的內(nèi)存訪問模型

本節(jié)建立了一個可對標量類型、聚合類型以及MMIO 類型的共享數(shù)據(jù)進行統(tǒng)一表示的參數(shù)化的內(nèi)存訪問模型來描述被訪問的各種抽象內(nèi)存區(qū)域.這一模型表示為一個五元組（Base，Offset，Size，Mode，ConstAccess）.

1）Base是抽象內(nèi)存區(qū)域的起始地址（一般用變量名標識，若數(shù)據(jù)為MMIO 則以ADDR_ZERO 標識）.

2）Offset是抽象內(nèi)存區(qū)域的偏移量，為處理在同一程序點訪問多個不同元素或成員的情況（例如循環(huán)訪問數(shù)組變量），可將Offset定義為一個集合.

3）Size是每一塊抽象內(nèi)存區(qū)域的大小.

4）Mode是對抽象內(nèi)存區(qū)域的訪問方式，包括讀和寫.

5）ConstAccess可判斷該抽象內(nèi)存區(qū)域是否寫入常量或者Mode為讀，若是，則置為true；否則，置為false.

表3 為圖5 案例中標量類型、聚合類型、MMIO這3 種類型數(shù)據(jù)在該模型中的表示（針對每個數(shù)據(jù)類型，以一個具有代表性的訪問為例，給出其表現(xiàn)形式）.例如，在訪問點⑤和⑥處，對upload_data[0]、upload_data[1]的寫訪問可表示為(upload_data,{0,4},4,write,false)，描述了對地址為upload_data+0、大小為4B 以及地址為upload_data+4、大小為4B 的2 個內(nèi)存單元的寫訪問.

本文通過指針分析確定內(nèi)存訪問模型中的Base值，根據(jù)發(fā)生訪問的程序語句可得到Size值和Mode類型.因此，如何精確地描述抽象內(nèi)存區(qū)域?qū)⑷Q于Offset值集的精確性.

2.1.2 基于抽象解釋的數(shù)值分析

本節(jié)采用RPIC 抽象域?qū)γ恳粋€并發(fā)流進行獨立的基于抽象解釋的數(shù)值分析，計算內(nèi)存訪問模型中Offset的數(shù)值不變式.除此之外，本節(jié)還擴展了現(xiàn)有的抽象解釋迭代算法，以實現(xiàn)對中斷干擾的上近似，保證分析無漏報.

Table 3 Representation of Different Data Types表3 不同數(shù)據(jù)類型表現(xiàn)形式

Fig.5 Example for shared data access圖5 共享數(shù)據(jù)訪問示例

2.1.2.1 RPIC 抽象域.

本文使用數(shù)值抽象域來刻畫內(nèi)存訪問模型中的Offset值集.在缺陷特征研究中發(fā)現(xiàn)偏移量的使用會出現(xiàn)在3 種情況中：1）訪問數(shù)組元素；2）訪問結構體或聯(lián)合體的成員變量；3）通過增加偏移量訪問MMIO.因此在抽象解釋過程中需要選擇適合這3 種情況的抽象域.RPIC 抽象域是區(qū)間抽象域和同余抽象域的約化積（reduced product）[21]，它可以描述連續(xù)區(qū)域和步長信息，步長信息用于分析通過間接尋址來實現(xiàn)訪問操作，如結構體成員訪問和指針解引用等.在RPIC 中，區(qū)間抽象域提供變量值的上界和下界，而同余抽象域計算值之間的步長.因此抽象元素可以表示為[a,b]∩(cZ+d).例如，圖5 示例中的訪問點⑤，⑥處，對應的偏移量被近似表示為[0,4]∩(4Z)，它表示一個下界為0、上界為4、步長為4 的離散整數(shù)集，即Offset值集為{4Z|Z∈[0,1]}.

2.1.2.2 中斷干擾的上近似.

本文擴展了現(xiàn)有的抽象解釋迭代算法，以實現(xiàn)對中斷干擾的上近似分析.對于中斷驅(qū)動型程序，若在程序分析時不考慮中斷并發(fā)對程序狀態(tài)的影響，將導致主任務中的部分執(zhí)行路徑被誤認為不可行，從而導致漏報.如圖6 所示，若不考慮中斷執(zhí)行，僅考慮主任務執(zhí)行，由于(Flag=false)∧(Flag==true)為互斥的約束，S1將不會被執(zhí)行，則KZData不會被訪問.而事實上在中斷的作用下，F(xiàn)lag會被賦值為true，即S1是可以被執(zhí)行的，因此主任務中對KZData的讀訪問也是一次共享訪問.為了保證分析結果的可靠性，本文采用了一種簡單的處理策略，即在迭代過程中認為所有分支路徑都可行，以收集到所有的數(shù)據(jù)訪問點，實現(xiàn)對中斷干擾的上近似分析.

Fig.6 A case of interrupt side effect圖6 中斷副作用示例

2.1.3 共享訪問點識別

共享訪問點識別的目的是識別被不同并發(fā)流（主任務、各個中斷）訪問的共享數(shù)據(jù).特別是intAtom-S 引入基于規(guī)則的方法將不會導致缺陷的標志變量的訪問剔除，僅返回那些會導致缺陷的共享訪問點集合.在中斷驅(qū)動型嵌入式軟件中，自定義標志變量總是遵循的規(guī)則為：標志變量為char 類型，且在整個程序執(zhí)行過程中僅被賦值為常量.而這些標志變量的并發(fā)訪問并不會導致缺陷.因此，本節(jié)首先識別出僅被寫入常量的char 類型共享數(shù)據(jù).intAtom-S 通過對不同并發(fā)流之間的數(shù)據(jù)訪問點的ConstAccess進行合取操作，識別出標志變量.例如，圖5 示例中的訪問點③，④和⑩，其共享數(shù)據(jù)分別被表示為（func_run,[0,0]∩{1Z},0,read,true ），(func_run,[0,0]∩{1Z},0,write，true )，(func_run,[0,0]∩{1Z},0,write,true).③，④和⑩具有相同的Base，對它們的constAccess字段進行合取操作，即true∧true∧true得到true，且func_run是一個char 類型數(shù)據(jù)，因此其是一個標志變量.然后，intAtom-S 通過對不同并發(fā)流之間的數(shù)據(jù)訪問點的數(shù)值抽象域進行與操作，識別出共享數(shù)據(jù)訪問.例如，圖5 示例中的訪問點⑨，其共享數(shù)據(jù)可被表示為(upload_data,[4,4]∩{1Z},4,write,true).訪 問點⑤和⑥處的共享數(shù)據(jù)為(upload_data,[0,4]∩{4Z},4,write,false).⑤和⑥與⑨具有相同的Base，對[4,4]∩{1Z}和[0,4]∩{4Z}進行與操作得到[4,4]∩{1Z}，因此upload_data[1]是主任務（⑥）與中斷（⑨）之間的共享數(shù)據(jù).在此過程中，會分析并發(fā)流的優(yōu)先級以確定它們能否并發(fā)執(zhí)行.比如，相同優(yōu)先級的中斷之間不能發(fā)生搶占，相應的數(shù)據(jù)訪問并不會構成共享.最后，將兩個或多個并發(fā)流之間的數(shù)據(jù)訪問交集標記為共享數(shù)據(jù).

intAtom-S 最終返回一個包含所有去掉標志變量訪問之后的共享訪問點和訪問點位置信息的集合，訪問點位置信息包括發(fā)生訪問的函數(shù)、程序入口、語句行號、列號、源文件等字段.

2.2 訪問交錯模式匹配

表1 中訪問交錯模式的3 次訪問序(ep,er,ec)由對同一共享數(shù)據(jù)的3 個訪問事件組成，其中ep和ec來自isrl（或主任務），er來自isrh.每一個訪問事件e由一個四元組e=(T,L,V,A)表示，其中T為任務或中斷的標識，L是事件發(fā)生的程序點，V是被訪問的共享數(shù)據(jù)，A是訪問類型（讀或?qū)懀?

算法1 描述了基于過程間數(shù)據(jù)流分析框架[23]的訪問交錯模式匹配方法.本文將對同一個共享變量v的2 次串行訪問建模為一個數(shù)據(jù)流問題.如果對于一個變量的2 次訪問ep和ec之間有一條路徑，且在該路徑上v沒有其它訪問，則構成一個串行訪問對.dataFlowAnalysis對該數(shù)據(jù)流問題進行求解，以查找出所有的串行訪問對.此外，根據(jù)Vaziri 等人[22]的工作，程序員的原子意圖與程序結構相關，可以在特定的“工作單元”邊界內(nèi)對原子性進行推斷.受此啟發(fā)，結合實證研究結果，本文根據(jù)共享變量所在位置，將原子性的邊界限制在同一函數(shù)或主調(diào)函數(shù)內(nèi)，并過濾掉那些超出邊界的訪問對.然后，對于isrh中的每個共享內(nèi)存訪問，intAtom-S 檢查它和isrl（或主任務）中的串行訪問對是否可以組合為表1 中的訪問交錯模式（行?～?）.如果可以，intAtom-S 將該3 次訪問序(ep,er,ec)添加至原子性違反候選集.

算法1.訪問交錯模式匹配算法.

輸入：源程序P；

輸出：原子性違反候選集合C={(ep,er,ec)}.

2.3 不可行路徑裁剪

本階段利用路徑約束求解進行串行訪問，對可行性分析和并發(fā)3 次訪問序進行可行性分析，逐步消除誤報，從而得到最終的原子性違反結果.

2.3.1 串行訪問對可行性分析

在這個階段，本文通過識別路徑不可行的串行訪問對(ep,ec)消除一類誤報.如果某串行訪問對不可行，說明程序員對它們并沒有進行原子性假設，此類原子性違反候選將被過濾掉.如圖7 所示，對共享數(shù)據(jù)YCData共有3 次訪問，S1、S2與S3顯然滿足(W,W,R)模式.在該案例中，中斷Timer0_ISR通過S2周期性地更新YCData，并將標志變量fgAh置為true.只有當中斷將YCData數(shù)據(jù)更新后，主任務才會通過S3讀取YCData的值，該程序有意設計語句if(fgAh==true)以判斷中斷是否已經(jīng)發(fā)生.雖然S1和S3是2 個連續(xù)的串行訪問，但它們具有互斥的約束(fgAh=false)∧(fgAh==true)，因此，這2 個訪問組成的串行訪問對是不可行的，表明程序員對它們沒有進行原子性假設.所以，有必要排除這些不可行的連續(xù)訪問對.

Fig.7 A case of infeasible consecutive access pair圖7 不可行串行訪問對示例

為了提高分析效率，本文建立依賴圖[23]對程序進行稀疏的表示.并在此基礎上構建串行訪問對的路徑約束，然后利用SMT 求解器進行約束求解.若路徑中存在循環(huán)，為了防止過高的開銷，對循環(huán)展開2次后跳出.

對于一個給定的串行訪問對(ep,ec)，P1 和P2 分別是由入口到ep和ec的路徑.路徑條件PC(ep,ec)由P1 與P2 的有效路徑條件[24-25]合取得到.其中，有效路徑條件通過對該路徑相關的數(shù)據(jù)依賴和控制依賴合取得出.因此，給定一條從入口出發(fā)的路徑P，vi為P的路徑約束所依賴的變量，P的路徑條件計算公式為

一個路徑條件由3 個部分組成：

1）C D(vi)為控制依賴，表示到達vi的條件約束；

2）vi?1=vi描述vi中存儲的值流向vi?1；

3）DD(vi?1,vi)表示值從vi流向vi?1是可行的.

2.3.2 并發(fā)3 次訪問序可行性分析

在串行訪問對(ep,ec)可行的前提下，分析3 次訪問序(ep,er,ec)并發(fā)路徑的可行性，進一步消除誤報.由于中斷程序的副作用，仍然存在一些原子性違反候選在實際的并發(fā)執(zhí)行中永遠不會發(fā)生，即不存在一條可行的并發(fā)路徑包含該3 次訪問序.如圖8 所示，當中斷在主任務中的S1后被搶占，則S2是不可能發(fā)生的.這是由于如果在該搶占點的狀態(tài)需滿足(ono f fn um>0)∧(fgExecute==1)，則從ONOFFManage入口到S2的路徑條件(fgExecute==0)將不能被滿足.因此，給定一個原子性違反候選(ep,er,ec)，若要檢查其可行性，需要對ep與ec之間的每個搶占點p分別檢查其子路徑（p→entryisr→…→er）與（exitisr→p→…→ec）的可行性.由于并發(fā)路徑的數(shù)量為指數(shù)級，這一步驟非常耗時.

Fig.8 A case of infeasible concurrent triple access interleaving圖8 不可行并發(fā)3 次訪問序示例

如算法2 所示，intAtom-S 采用了一種組合方法以降低不可行并發(fā)3 次訪問序裁剪的開銷.

1）模塊化地構建中斷摘要.intAtom-S 首先通過constructSummary對每個中斷構建符號化摘要，從而避免冗余路徑條件計算（行①～③）.摘要使用符號約束描述了er的路徑條件與exitisr的狀態(tài).

2）選擇具有代表性的搶占點.對于每一個原子性違反候選，intAtom-S 通過函數(shù)selectPreemptPoint選擇具有代表性的搶占點，以縮減交錯空間（行④～⑤）.

3）利用約束求解驗證可行性.對于每一個選擇出的代表性搶占點p，分別檢查其子路徑（p→entryisr→…→er）與（exitisr→p→…→ec）的可行性.

intAtom-S 通過函數(shù)obtainState（行⑧）獲得代表性搶占點處的全局程序狀態(tài)，并將此信息作為上下文傳遞給中斷.然后，函數(shù)isFeasible提取摘要中的約束條件，并利用約束求解器來檢查以搶占點p為上下文時，路徑entryisr到er的可行性（行⑨）.如果這條路徑不可行，則意味該3 次訪問序為誤報，需要被裁剪掉；否則，intAtom-S 將繼續(xù)分析以exitisr為上下文時，搶占點p和ec之間路徑的可行性（行?）.constructPC使用與2.3.1 節(jié)相同的方法構建路徑條件.如果（p→entryisr→…→er）與（exitisr→p→…→ec）這2 條 路徑都可行，intAtom-S 將向用戶報告一個原子性違反.由于intAtom-S 區(qū)分了每個搶占點的上下文并檢查每條路徑的可行性，因此是上下文敏感和路徑敏感的.

intAtom-S 還在全局程序狀態(tài)中對中斷屏蔽的使用進行了建模.本文將中斷屏蔽寄存器作為全局變量，并在每個中斷的入口檢查是否被屏蔽.因此，本文的方法可以處理通用中斷屏蔽.

算法2.并發(fā)3 次訪問序可行性分析算法.

輸入：原子性違反候選集合C={(ep,er,ec)}、源程序P；

輸出：原子性違反.

接下來，將詳細介紹中斷摘要構建與代表性搶占點選取的細節(jié).

1）中斷摘要構建.當檢查并發(fā)3 次訪問序可行性時，需要獲取2 個中斷信息：①了解entryisr到er的路徑條件，用于檢查路徑ep到er的可行性；②了解經(jīng)過er的路徑在中斷出口處全局變量的狀態(tài)，以確定是否存在從中斷退出回到ec的可行路徑.因此，本文構建包含這2 個中斷信息的中斷摘要，當檢查路徑可行性時，在不同的搶占點處復用這些

摘要.給定一個中斷isr和一組變量集合Π={e0,e1，…}，該集合代表isr中所有可能的er，isr的摘要可由集合S ummisr表示，可以表示為三元組集合其中pcei代表從entryisr到ei的路徑條件，代表isr出口處的全局狀態(tài).

本文單獨分析每個中斷來構建它的摘要，可在并發(fā)3 次訪問序可行性檢查時直接復用.對于isr中的訪問事件er，存在2 種情況可以重用中斷摘要.一是檢查涉及er的多個原子性違反候選的可行性；二是對同一個候選的多個搶占點進行檢查.

2）代表性搶占點選取.并發(fā)3 次訪問序(ep,er,ec)的可行性取決于2 條子路徑（p→entryisr→…→er）與（exitisr→p→…→ec）的可行性.然而，只有當程序語句直接修改了2 條并發(fā)子路徑的約束條件，或者修改了約束條件所依賴的變量時才會影響到并發(fā)3次訪問序的可行性.也就是說，某些程序語句的副作用可能對這2 條子路徑可行性檢查的結果沒有影響.因此，可以選擇性地檢查部分搶占點對應的并發(fā)路徑，而無需檢查所有的路徑，這些搶占點就被稱為代表性搶占點.

從ep到ec路徑上的所有程序語句可用集合S={S1,S2,…,Sn}表示，其中Si是Si+1的直接前序語句.用P={p1,p2,…,pn}表示搶占點集合，其中pi位于Si與Si+1之間，稱Si為搶占點pi對應的程序語句.本文代表性搶占點定義為：給定搶占點pi與pi+1，如果pi滿足2個條件之一，那么其為一個代表性搶占點.1）Si+1為一個賦值語句，且Si+1沒有改變?nèi)魏温窂郊s束中包含的變量的取值；2）Si+1包含一個條件表達式，該條件表達式的控制變量與中包含的變量不重合.

因此，通過按順序遍歷P以選取所有ep到ec之間的代表性搶占點.對于每一個搶占點pi，如果其未滿足上述條件，那么pi+1將被選擇為代表性搶占點；否則，pi+1可以被當前選定的代表性搶占點代表.

圖9 顯示一個選擇代表性搶占點的例子.(ep,er,ec)為一個原子性違反候選.主任務與中斷中的語句記為Si，搶占點記為pi.S2對變量fgCurrentB進行了寫操作.由于路徑(p→entryisr→…→er)的路徑條件與變量fgCurrentB無關，且S2不是分支語句，因此p2可以被p1代表；同樣p3可以被p2代表.而S4對全局變量fgAh進行了寫操作，fgAh在路徑條件中，因此p4不能被p3代表.本文選擇p4為新的代表性搶占點.S5對變量fgCharge進行寫操作，然后fgCharge用于S6中條件表達式中.然而fgCharge不包含于中，因此p5與p6可以被p4代表.對于S7，fgPower是條件表達式的控制變量，且包含在中，因此p7不能被p4代表.最后，選擇3 個代表性搶占點p1，p4與p7.

3 實驗評估與應用

本文在一臺配備Intel(R) Xeon(R) E5-2 620 CPU、32GB RAM 和Ubuntu 20.04 操作系 統(tǒng)的計 算機上 進行了實驗.為了評估intAtom-S，考慮4 個研究問題：

問題1：intAtom-S 在檢測中斷驅(qū)動型程序的原子性違反方面有效性如何?

問題2：intAtom-S 在檢測中斷驅(qū)動型程序的原子性違反方面的效率如何?

問題3：intAtom-S 分析共享數(shù)據(jù)的有效性如何？

問題4：intAtom-S 路徑裁剪的有效性和效率如何?

3.1 實驗設置

為了評估intAtom-S 的缺陷檢測能力，本文將其與Rchecker[15]進行實驗對比，Rchecker 是與intAtom-S 最相近且最新提出的方法，它們針對的都是中斷驅(qū)動型程序中的原子性違反.然而Rchecker 不是開源工具，且只在基準測試集Racebench2.1 上進行過實驗，因此本文同樣在Racebench2.1 上對intAtom-S 進行實驗.為了進一步評估本文方法的實用性，還在8 個真實的中斷驅(qū)動型航天嵌入式軟件上進行了實驗.目前為止，intAtom-S 是唯一一個在工業(yè)嵌入式軟件上進行評估的并發(fā)缺陷檢測工具.此外，本文還將intAtom-S與static-TSA[26]進行實驗對比，以評估其分析共享數(shù)據(jù)的有效性.實驗中使用了2 個數(shù)據(jù)集.

Fig.9 An example of representative preemption points selection圖9 代表性搶占點選擇示例

1）數(shù)據(jù)1 是基準測試集.本文使用開源基準測試集Racebench 2.1 來評估intAtom-S 是否可以在各種場景中檢測原子性違反.Racebench2.1 最初被用于作為評估NASAC 2019 并發(fā)缺陷檢測工具競賽的參賽工具.后來，它也被用于Rchecker[15]的實驗分析.Racebench 2.1 由31 個中斷驅(qū)動型案例和54 個手動注入的原子性違反構成.這些案例都是基于真實航天嵌入式軟件的特點設計的，能夠反映現(xiàn)實世界中斷并發(fā)程序的語法和語義特點.這些案例涵蓋原子性違反的各種表現(xiàn)形式，如訪問交錯模式、共享數(shù)據(jù)類型、訪問方式、控制流場景等.Racebench 2.1 考慮了發(fā)生缺陷的不同場景，有助于對工具進行全面的評估.

2）數(shù)據(jù)2 是真實中斷驅(qū)動型航天嵌入式軟件.為了評估intAtom-S 是否能夠有效檢測真實中斷驅(qū)動型軟件中的原子性違反，從實證研究的缺陷案例中選取了8 個具有代表性的軟件，如表4 所示，所選案例的規(guī)模從970 行到5 099 行不等，是中斷驅(qū)動型航天嵌入式軟件最典型的代碼規(guī)模.首先，標記了這些軟件的CPU 類型、程序規(guī)模和中斷個數(shù)，這是反映真實嵌入式軟件多樣性的3 個重要屬性.然后，以涵蓋這3 個屬性的多種組合為目標，選取具有代表性的案例.盡管我們希望選用盡可能多的案例進行實驗，然而評估真實的航天嵌入式軟件需要消耗大量的時間和資源.主要原因為：①嵌入式軟件的編譯平臺多種多樣，不同的編譯器（如MCS-51，MSP430）采用不同的語言擴展，如數(shù)據(jù)類型、關鍵字等.由于原型工具只支持ANSI C，因此需要對源代碼進行大量修改才能將原始代碼轉(zhuǎn)換為等價的ANSI C 代碼.②原子性違反的確認需要應用程序（系統(tǒng)）相關的特定知識.所有原始報告中的警報都需要開發(fā)人員單獨分析確認.一般來說，每個項目需要一個多月的時間才能完成確認.因此，本文最終選擇了8 個具有代表性的案例作為實驗對象.

Table 4 Analyzed Real-world Aerospace Software Projects表4 被分析的真實航天軟件項目

3.2 檢測有效性（針對問題1）

1）基準測試集檢測結果.

在基準測試集Racebench 2.1 上的實驗結果如表5所示.intAtom-S 可以在基準測試集中檢測出所有的原子性違反，并顯著減少誤報.intAtom-S 在31 個基準測試集案例中只有6 個誤報，相比Rchecker 誤報率降低了72%.

我們發(fā)現(xiàn)，Rchecker 誤報的主要原因是因為忽視了對程序員的原子性意圖的推斷.因此，沒有原子性期望的3 次訪問序也被報告為缺陷.而intAtom-S則有效地解決了這一問題.進一步分析了intAtom-S的6 個誤報，誤報原因都是因為在循環(huán)中使用了簡化路徑條件計算.由于有一些在循環(huán)中被訪問的共享數(shù)據(jù)，是被循環(huán)計數(shù)變量相關的約束所保護的.為了避免循環(huán)展開，intAtom-S 簡單地忽略了該路徑約束.因此可能會錯誤地將條件訪問視為對同一變量的多次訪問.可以通過對循環(huán)使用路徑進行敏感分析以消除這些誤報.然而，這將不可避免地增加開銷.因為當循環(huán)計數(shù)非常龐大的時候，會產(chǎn)生巨額開銷.

Table 5 Results of Benchmark表5 基準測試集檢測結果

續(xù)表 5

2）真實中斷驅(qū)動型航天嵌入式軟件檢測結果.

表6 給出了在真實航天嵌入式軟件上的檢測結果.每個階段的結果分別由3 部分組成，“違反個數(shù)”表示進行當前階段的原子性違反候選個數(shù)；“減少比例”指與上一階段相比，原子性違反減少的比例；“時間占比”表示當前階段的時間開銷占總時間的百分比.每一個報告的原子性違反都經(jīng)過開發(fā)人員檢查與確認，最終確定是否為一個真實缺陷.從表6 可以看出，intAtom-S 在8 個真實軟件中檢測出45 個原子性違反，平均誤報率為8.9%.實驗結果顯示，intAtom-S 可以有效地檢測真實工業(yè)嵌入式軟件中的原子性違反，且具有非常低的誤報率.

Table 6 Detection Results of Real-World Interrupt-Driven Aerospace Embedded Software表6 真實中斷驅(qū)動型航天嵌入式軟件檢測結果

進一步分析這些檢測結果，將其分為3 類：有害原子性違反、良性原子性違反和誤報.其中缺陷是否為良性也需要經(jīng)過領域?qū)＜业臋z查與確認.intAtom-S 檢測到23 個有害的原子性違反都已經(jīng)得到開發(fā)人員的確認.檢測到的18 個良性原子性違反可分為2 類.1）雖然ep和er是2 個連續(xù)的本地訪問，但是開發(fā)人員對它們沒有原子性的期望.例如，開發(fā)人員預計ep之后會出現(xiàn)中斷，并使用ec進行容錯.2）原子性違反對結果沒有影響.例如，一個并發(fā)3 次訪問序(ep,er,ec)匹配模式(W,W,R)，如果ep和er將相同的值存儲到共享數(shù)據(jù)中，ec總是讀取期望值.值得注意的是，本文基于文獻[17] 中的intAtom 進行擴展，intAtom共檢測到3類良性原子性違反，除去這2 類，還有一類是由開發(fā)人員有意設計的.例如，在模式(R,W,W)中，ep對標志變量的讀訪問 處于循環(huán)條件語句中，等待特定的中斷搶占并執(zhí)行er以改變此標志變量的值使條件滿足，從而執(zhí)行循環(huán)體中的代碼段；執(zhí)行完畢后通過ec重置此標志變量的值.然而，本文在共享數(shù)據(jù)識別階段去除了標志變量訪問，所以檢測階段不會再報告此類良性原子性違反，這表示intAtom-S 的檢測結果更加精確.

intAtom-S 結果中存在的4 個誤報都是由于在循環(huán)中使用了簡化的路徑條件計算所導致.相比intAtom，intAtom-S 的檢測結果更加精確，如表7 所示.intAtom 在這8 個真實程序的檢測結果中存在11個誤報，其中有6 個是由于當循環(huán)計數(shù)變量用作數(shù)組下標時，intAtom 不能區(qū)分這些數(shù)組元素所導致的；還有1 個是由于標志變量訪問造成的.而本文方法采用精確的共享數(shù)據(jù)分析，能夠識別標志變量訪問，且區(qū)分數(shù)組元素，因此可以避免這些誤報.

Table 7 Comparison of Effectiveness and Efficiency Between intAtom-S and intAtom表7 intAtom-S 與intAtom 有效性及效率對比

3.3 檢測效率（針對問題2）

表5 顯示了intAtom-S 和Rchecker 的在基準測試集Racebench 2.1 上的運行時間.為了公平地分析時間性能，本文只比較了2 個工具都能完成檢測的案例上所花費的時間.例如，由于Rchecker 無法分析案例24.因此，本文只關注其余30 個案例的實驗數(shù)據(jù).從總體上看，相比Rchecker，intAtom-S 在大多數(shù)案例（26/30）上花費更短的檢測時間，intAtom-S 的平均檢測時間為0.196 s，而Rchecker 的平均 檢測時間為0.592 s.

由表5 可知，在所有的案例中，intAtom-S 的最長檢測時間為0.578 s.而Rchecker 在某些案例上的檢測時間則都多于1 s（如案例5、17、29），甚至最長檢測時間達到了5.2 s.檢查這些案例的代碼，發(fā)現(xiàn)它們都具有龐大而復雜的交錯空間，這導致Rchecker 的分析時間呈指數(shù)級增長.intAtom-S 使用函數(shù)摘要和代表性搶占點，可以有效緩解交錯空間爆炸，從而達到更高的檢測效率.

表7 顯示了intAtom-S 與intAtom 在真實中斷驅(qū)動型程序上的檢測時間對比.真實的中斷驅(qū)動型程序規(guī)模相對較大，包含數(shù)千行代碼.intAtom-S 可以在305 s 內(nèi)分析5 000 行的真實航天嵌入式軟件，雖然比intAtom 時間開銷略高（額外開銷介于1.8%～50.4%），卻實現(xiàn)了更高的檢測精度，能夠滿足實際工業(yè)需求.

3.4 共享數(shù)據(jù)分析效果（針對問題3）

由于基準測試集中都是代碼規(guī)模較小的案例，對于不同數(shù)據(jù)類型的代表性不強，不具有統(tǒng)計學意義.本文在8 個真實的航天嵌入式軟件上進行了intAtom-S 與static-TSA 的共享數(shù)據(jù)分析對比實驗.在這8 個軟件中，存在3 種共享數(shù)據(jù)類型（標量類型、聚合類型、I/O 地址）.值得注意的是，static-TSA 利用調(diào)用圖和指向分析來識別共享數(shù)據(jù)訪問，然而與intAtom-S 相比，static-TSA 既不能處理I/O 地址訪問，也不能區(qū)分數(shù)組中的各個數(shù)組元素，這導致其實驗結果存在大量誤報與漏報.

表8 顯示了intAtom-S 與static-TSA 共享數(shù)據(jù)分析的結果.本文手動分析每個檢測到的共享數(shù)據(jù)并進行最終確認.由于intAtom-S 以原子性違反檢測為目標，進行共享數(shù)據(jù)分析時剔除了標志變量訪問，而static-TSA 并不進行此操作，為了保證對比實驗的公平性，本文將static-TSA 結果中的標志變量訪問手動剔除,進而對兩者進行對比.對于這8 個程序，intAtom-S 檢測所有共享數(shù)據(jù)都沒有誤報；而static-TSA 具有191 個誤報.這是由于static-TSA 不能區(qū)分數(shù)組索引，導致對不同數(shù)組元素的訪問被標識為同一數(shù)據(jù)的訪問.此外，static-TSA 遺漏了29 個共享的I/O 地址訪問；而intAtom-S 不僅可以區(qū)分數(shù)組索引，且能有效檢測共享的I/O 地址訪問，因此能夠精確檢測航天嵌入式軟件中各種類型的共享數(shù)據(jù).

Table 8 Results of Shared Data Analysis表8 共享數(shù)據(jù)分析結果

3.5 路徑裁剪效果（針對問題4）

為了更好了解intAtom-S 路徑裁剪的有效性和效率，本文關注通過模式匹配檢測到的原子性違反候選的數(shù)量、經(jīng)過路徑裁剪后剩余的候選數(shù)量，以及它們的時間開銷，分析結果如表6 和表9 所示.

實驗結果表明，路徑裁剪具有非常顯著的貢獻.在模式匹配階段，intAtom-S 檢測每個項目中潛在的原子性違反候選，平均每個項目有238 個候選.在路徑裁剪階段，intAtom-S 首先通過串行訪問對可行性分析裁剪了42.2%的候選，平均每個項目剩余100 個候選.然后intAtom-S 通過并發(fā)3 次訪問序可行性分析裁剪了97.6%的候選.每個階段的時間開銷如表6所示.在模式匹配和路徑裁剪階段，intAtom-S 花費的時間分別占總時間的37.8%和46.3%.

為了進一步評估所提出的符號化中斷摘要和代表性搶占點選擇方法的有效性，本文實現(xiàn)了2 個額外的intAtom-S 變體：Naive 和Naive+RPPS（使用代表性搶占點選擇）.Naive 可以被看作是一種基線方法，它在沒有中斷摘要的情況下，檢查并發(fā)3 次訪問序的可行性.Naive+RPPS 同樣不使用中斷摘要，但僅在每個代表性搶占點處進行路徑約束求解.本文在8 個真實航天嵌入式軟件上進行了實驗，比較了intAtom-S，Naive 和Naive+RPPS 進行并發(fā)3 次訪問序可行性分析時的時間開銷.如表9 所示，Naive+RPPS 的效率是Naive 的1.2～3.6 倍，平均1.8 倍；intAtom-S 的效率是Naive的2.6～8.5 倍，平均3.0 倍.結果表明，符號化摘要和代表性搶占點對提高方法可擴展性是至關重要的.

Table 9 Time Cost of Naive+RPPS and intAtom-S Compared with That of Naive表9 Naive+RPPS 和 intAtom-S 與Naive 的時間開銷對比

4 相關工作

近年來，學者們提出大量檢測多線程程序原子性違反的方法[5-10,20,27-29].Lu 等人[20]基于同一原子區(qū)中共享數(shù)據(jù)的訪問交錯定義了可串行化.在此基礎上，他們提出了訪問交錯不變量，并根據(jù)該不變量檢測原子性違反.在他們后續(xù)的工作中進一步提出CTrigger[27]，通過軌跡分析以識別不可串行交錯，并測試低概率交錯以暴露原子性違反.Lucia 等人[28]提出Atom-Aid，使用硬件簽名來檢測原子性違反，動態(tài)地調(diào)整塊邊界，在不需要任何程序注釋的情況下規(guī)避缺陷.Chew 等人[29]提出Kivati，通過結合靜態(tài)和動態(tài)分析以檢測和避免原子性違反.Wang 等人[10]提出了一種基于預測的檢測原子性違反的方法，通過監(jiān)視執(zhí)行交錯以記錄執(zhí)行序列，并根據(jù)訪問交錯候選序列預測潛在的缺陷.Razavi 等人[8]提出一種基于人工智能的預測原子性缺陷的方法.Sorrentino 等人[9]提出一種算法挖掘一組導致原子性違反的執(zhí)行序列，并使程序按這種序列執(zhí)行以暴露缺陷.然而，中斷模型無論在調(diào)度、同步還是搶占關系上都與線程模型不同.而且，大多數(shù)方法所依賴的動態(tài)分析很難直接應用于中斷驅(qū)動型程序中.

目前有一些方法用于檢測中斷驅(qū)動型程序中的數(shù)據(jù)競爭[19,30-33].Wang 等人[19]提出SDRacer，將靜態(tài)分析與符號執(zhí)行相結合，通過為中斷驅(qū)動型嵌入式軟件生成輸入數(shù)據(jù)來自動檢測數(shù)據(jù)競爭.Wu 等人[32-33]自動化地將中斷程序順序化為一個非確定的順序程序，分別采用限界模型檢測框架和抽象解釋的方法來分析程序中的數(shù)據(jù)競爭.Chopra 等人[30]為中斷程序定義了數(shù)據(jù)競爭與happens-before 的自然概念，他們還提出不相交塊的概念來定義同步以及高效的“sync-CFG”，從而展開靜態(tài)分析.然而中斷程序經(jīng)常使用定制的同步機制，例如用戶定義的基于標志變量的同步.很多數(shù)據(jù)競爭是專門設計出來進行數(shù)據(jù)共享的，這些數(shù)據(jù)競爭都是良性的，若以數(shù)據(jù)競爭為檢測目標，會存在大量誤報.相比之下，本文的方法側(cè)重于最可能有害的原子性違反.

據(jù)我們所知，目前只有文獻[4,15,17]可用于檢測中斷驅(qū)動型程序中的原子性違反.文獻[4]采用基于抽象解釋的方法，可以有效地識別程序中潛在的原子性違反.然而，由于其分析對路徑不敏感，存在大量誤報.文獻[15]提出基于限界模型檢測的檢測方法，可以得到比較準確的結果，但可擴展性很差.文獻[17]采用了階段性的方法，可以同時實現(xiàn)更高的精度和分析.而本文在文獻[17]的基礎上增加了精確的共享數(shù)據(jù)分析，使結果進一步精確，能夠有效檢測工業(yè)規(guī)模的中斷驅(qū)動型嵌入式軟件.

5 總結

本文對航天嵌入式軟件中原子性違反缺陷的表現(xiàn)形式進行了系統(tǒng)的實證研究，獲得了原子區(qū)范圍、中斷嵌套層數(shù)、共享數(shù)據(jù)訪問交錯模式、訪問方式、訪問粒度等5 方面的表現(xiàn)特征.基于這些特征，提出了一個精確、高效的中斷驅(qū)動型程序原子性違反靜態(tài)檢測方法intAtom-S.該方法首先進行精確的共享數(shù)據(jù)分析，將共享數(shù)據(jù)訪問粒度精確至數(shù)組元素，并可識別標志變量訪問與共享的內(nèi)存映射I/O 地址.然后，使用輕量級數(shù)據(jù)流分析技術匹配符合缺陷訪問交錯模式的所有并發(fā)3 次訪問序作為潛在的原子性違反缺陷候選.最后，采用基于路徑條件的約束求解對缺陷候選中的串行訪問對和并發(fā)3 次訪問序進行路徑可行性分析，逐步消除誤報，得到最終的原子性違反結果.本文分別在基準測試集與真實航天嵌入式軟件中對intAtom-S 進行了評估.結果表明，intAtom-S 顯著降低了誤報率，提高了檢測效率，并可滿足真實航天嵌入式軟件的檢測需求.

進一步的研究工作包括：

1）中斷驅(qū)動型軟件的設計中往往隱含了一些時序約束，而這種約束并不體現(xiàn)在代碼中，對于以源代碼為唯一分析對象的工具，該類誤報很難消除.未來可考慮對由用戶創(chuàng)建的系統(tǒng)時序模型進行精確檢測；

2）使用訪問交錯模式雖然很好地刻畫了原子性違反，但其中仍涵蓋了一些并不是缺陷的情況，未來可以進一步精化該模式.

作者貢獻聲明：于婷婷和李超為共同第一作者，提出了算法框架和實驗方案，完成實證研究并撰寫論文；王博祥負責完成工具開發(fā)和實驗；陳睿提出總體研究思路并撰寫論文；江云松提出指導意見并修改論文.