陳 睿，楊孟飛

(1.北京控制工程研究所，北京 100190； 2.北京軒宇信息技術(shù)有限公司，北京 100190；3.中國空間技術(shù)研究院，北京 100190)

?

基于編碼規(guī)則的中斷數(shù)據(jù)訪問沖突檢測方法*

陳 睿1,2，楊孟飛3

(1.北京控制工程研究所，北京 100190； 2.北京軒宇信息技術(shù)有限公司，北京 100190；3.中國空間技術(shù)研究院，北京 100190)

針對“重復(fù)加鎖解鎖”和“volatile修飾符誤用”兩種數(shù)據(jù)訪問沖突缺陷模式，提出基于編碼規(guī)則的檢測方法.首先，對缺陷模式的故障機(jī)理進(jìn)行分析，提煉出3條編碼規(guī)則用以在開發(fā)階段避免缺陷發(fā)生，并基于一個靜態(tài)代碼檢查工具SpaceCCH進(jìn)行了規(guī)則檢測方法研究和實(shí)現(xiàn).在實(shí)際星上軟件上的實(shí)驗(yàn)結(jié)果表明，擴(kuò)展的SpaceCCH能夠高效、低誤報(bào)、低漏報(bào)地發(fā)現(xiàn)規(guī)則違反，從而有效避免這兩種的數(shù)據(jù)訪問沖突問題.本文的貢獻(xiàn)在于將一類復(fù)雜缺陷的檢測轉(zhuǎn)換為相應(yīng)的編碼規(guī)則及其檢測. 關(guān)鍵詞： 數(shù)據(jù)訪問沖突；編碼規(guī)則；靜態(tài)分析；航天嵌入式軟件

0 引 言

數(shù)據(jù)訪問沖突問題是當(dāng)前航天型號軟件開發(fā)中最難解決的問題之一[1].這類問題發(fā)生在中斷驅(qū)動型程序或多任務(wù)程序中，當(dāng)兩個不同的中斷(或任務(wù))對同一個共享數(shù)據(jù)進(jìn)行同時的讀寫訪問，且至少存在一次寫操作時.由于兩次訪問的時序不可確定，程序會產(chǎn)生異常行為，如關(guān)鍵數(shù)據(jù)被非預(yù)期地修改，嚴(yán)重時甚至導(dǎo)致系統(tǒng)或軟件失效.然而，數(shù)據(jù)訪問沖突問題發(fā)生概率小、難以復(fù)現(xiàn)，往往在特殊的外部條件和中斷(或任務(wù))交迭情況下才會出現(xiàn)，難以通過傳統(tǒng)的軟件測試方法發(fā)現(xiàn)，遺漏率較高.因此，近年來數(shù)據(jù)訪問沖突自動檢測方法已成為研究熱點(diǎn)，國家自然科學(xué)基金“可信軟件基礎(chǔ)研究”重大研究計(jì)劃以及民用航天預(yù)先研究等都先后資助了相關(guān)課題，產(chǎn)生了一批有價值的方法或工具成果[2-9].

在安全關(guān)鍵領(lǐng)域，在軟件編碼過程中采用一定的編碼標(biāo)準(zhǔn)是缺陷預(yù)防的最有效手段之一.各個行業(yè)組織和機(jī)構(gòu)都根據(jù)應(yīng)用領(lǐng)域或軟件開發(fā)的特點(diǎn)制定各自的編碼標(biāo)準(zhǔn)，比較著名的有汽車工業(yè)軟件可靠性協(xié)會的MISRA C[10]、NASA噴氣推進(jìn)實(shí)驗(yàn)室的“The Power of Ten”[11]以及中國空間技術(shù)研究院院標(biāo)準(zhǔn)《航天器C語言軟件編程約定》等.一般地，一個編碼標(biāo)準(zhǔn)包含若干編碼規(guī)則，每條規(guī)則在編程語言標(biāo)準(zhǔn)語言特性的基礎(chǔ)上增加使用限制，以使相應(yīng)的危險程序行為受限或降低其發(fā)生風(fēng)險.實(shí)踐證明，通過應(yīng)用編碼規(guī)則及相應(yīng)的自動化檢查工具，能夠在編碼階段有效地預(yù)防一些潛在的問題.

文獻(xiàn)[2]通過大量真實(shí)案例分析提出刻畫有害數(shù)據(jù)訪問沖突的7種缺陷模式，并針對其中部分模式提出了相應(yīng)的檢測方法.本文針對尚缺乏自動化檢測方法的模式5和模式6，對其故障機(jī)理進(jìn)行分析，提煉形成3條相應(yīng)的編碼規(guī)則；在軟件編碼過程應(yīng)用這些編碼規(guī)則可以避免相應(yīng)模式的缺陷；進(jìn)一步提出基于規(guī)則的數(shù)據(jù)訪問沖突檢測方法，對上述3條編碼規(guī)則進(jìn)行自動化檢測，實(shí)現(xiàn)對相應(yīng)缺陷的保障.上述研究方法學(xué)如圖1所示.本文提出的方法在一個C語言靜態(tài)代碼檢查工具SpaceCCH基礎(chǔ)上實(shí)現(xiàn)，并在實(shí)際航天型號軟件中進(jìn)行了實(shí)驗(yàn)評估，驗(yàn)證了方法的有效性.

1 缺陷模式及實(shí)例分析

文獻(xiàn)[2]中的缺陷模式5和6是本文研究的問題.本節(jié)結(jié)合實(shí)例對這兩個模式進(jìn)行說明和分析.

模式5. 重復(fù)加鎖解鎖

開關(guān)中斷類似于多線程程序中的鎖機(jī)制,可用于屏蔽中斷處理,從而保證一段代碼的原子性.這兩個操作總是成對出現(xiàn)的.若在沒有意識到此時已經(jīng)處于鎖保護(hù)狀態(tài)下再次進(jìn)行加鎖解鎖操作,會導(dǎo)致第二次解鎖時候的代碼未被保護(hù),從而引發(fā)非預(yù)期的數(shù)據(jù)訪問沖突.

圖3給出了模式5對應(yīng)的的程序示例,為了保證StarTime變量計(jì)算的完整性，主程序main中采用ET0=0和ET0=1這一對加鎖解鎖操作來屏蔽中斷2中對Time結(jié)構(gòu)體的更新.然而，實(shí)際執(zhí)行中可能出現(xiàn)下面的場景：

1)主程序main執(zhí)行ET0=0，清除ET0寄存器以關(guān)閉中斷2；

2)中斷1打斷主程序，進(jìn)行某種操作，由于需要對中斷2進(jìn)行屏蔽，也進(jìn)行了ET0=0和ET0=1的操作分別對中斷2進(jìn)行關(guān)閉和打開；

3)從中斷1返回主程序后，當(dāng)前中斷2處于未屏蔽狀態(tài)，與主程序原期望不符；

4)中斷2打斷主程序，并對Time變量進(jìn)行了寫操作，導(dǎo)致主程序和中斷2發(fā)生了數(shù)據(jù)訪問沖突，StarTime計(jì)算錯誤.

上述場景是在系統(tǒng)實(shí)際運(yùn)行中真實(shí)暴露的，通過傳統(tǒng)的測試非常難以發(fā)現(xiàn).但從加鎖解鎖操作的時序特征比較容易刻畫，中斷2的加鎖解鎖操作序列為加鎖、加鎖、解鎖、解鎖.這一模式便于將這類缺陷規(guī)則化，易于研究進(jìn)一步的檢查方法.

模式6. volatile修飾符誤用

volatile是C語言中一個極易被誤解的特性.該關(guān)鍵字告訴編譯器被修飾的變量可能被中斷、任務(wù)或編譯器不知道的其他并發(fā)操作所修改.當(dāng)變量被volatile修飾時，編譯器知道處理器必須每次都從內(nèi)存中讀取該變量的值，因此編譯器不會對這類變量的訪問進(jìn)行優(yōu)化.一些較老的編譯器不支持volatile關(guān)鍵字，開發(fā)人員必須關(guān)閉編譯器優(yōu)化以獲得正確的結(jié)果.

在下面的示例中，secondsToday為long類型，長度為4字節(jié)，無論是8位機(jī)還是16位機(jī)，對secondsToday變量的一條操作語句會拆分為多條目標(biāo)碼指令.當(dāng)完成對該變量的第一個字節(jié)進(jìn)行讀，若發(fā)生中斷，則會導(dǎo)致13行語句執(zhí)行后IReturn值與secondsToday值不一致.為了避免這種情況，在第14～16行增加一個while循環(huán)對13行語句是否正確執(zhí)行進(jìn)行再次判斷和賦值，最終保證返回當(dāng)前實(shí)際的secondsToday值.

若secondsToday變量未采用volatile修飾，大多數(shù)編譯器做這樣的假設(shè)：除非程序修改變量的值，否則變量值會在內(nèi)存中保持，在編譯優(yōu)化打開的情況下，在第14行處，程序會從寄存器中讀取secondsToday的值，與程序編寫預(yù)期不同；一些優(yōu)化編譯器會認(rèn)為在13行secondsToday的值剛剛復(fù)制到IReturn變量，14行的while條件總是為假，則會優(yōu)化掉整個while循環(huán)體.

由于對volatile特性的不了解，上述案例常常被認(rèn)為是編譯器的缺陷.上述問題的最優(yōu)解決方法是：制定編碼規(guī)則，通過編碼規(guī)則來保證程序在共享變量上正確使用volatile修飾符，進(jìn)一步通過規(guī)則自動檢查的方法來實(shí)現(xiàn)對該缺陷模式的自動檢測.

2 檢測方法及工具

針對缺陷模式5和6，提煉形成3條相應(yīng)的編碼規(guī)則，基于一個已有的靜態(tài)代碼檢查工具SpaceCCH進(jìn)行了規(guī)則的擴(kuò)展實(shí)現(xiàn).其中，規(guī)則1和規(guī)則2的自動檢查采用符號表檢索和類型檢查方法，通過SpaceCCH已有分析引擎可較容易實(shí)現(xiàn)；針對規(guī)則3，本文提出了面向狀態(tài)機(jī)規(guī)則的靜態(tài)分析方法，并擴(kuò)展了SpaceCCH的分析引擎.最終，實(shí)現(xiàn)了所有規(guī)則的自動檢查.

2.1 面向數(shù)據(jù)訪問沖突的編碼規(guī)則

本文對缺陷模式5和6進(jìn)行了分析，提煉出3條用于避免缺陷發(fā)生的編碼規(guī)則.

規(guī)則1.對于下列情況必須使用volatile進(jìn)行數(shù)據(jù)聲明修飾.

a)被任意中斷服務(wù)程序使用的全局變量；

b)在兩個以上搶占式任務(wù)中使用的全局變量；

c)指向I/O端口或外設(shè)寄存器組的指針變量.

規(guī)則原理：強(qiáng)制上述數(shù)據(jù)的聲明使用volatile修飾，可以保證編譯器優(yōu)化不會改變對這些數(shù)據(jù)的讀寫訪問及其順序，避免部分關(guān)鍵操作在實(shí)際目標(biāo)碼中丟失，引發(fā)數(shù)據(jù)訪問沖突.

規(guī)則2.volatile修飾符應(yīng)在變量所有的聲明或定義處保持一致.

規(guī)則2的違反示例如圖4所示.程序中，smp.c中ipi_count的定義采用volatile修飾，而smp.h中該變量的外部聲明未采用volatile修飾，這兩處volatile修飾符的使用不一致.

規(guī)則原理：按照規(guī)則1，對有關(guān)共享數(shù)據(jù)采用volatile進(jìn)行修飾.但若頭文件中的聲明和c文件中的定義使用不一致時，在包含該頭文件的源代碼中對應(yīng)共享數(shù)據(jù)不被視為volatile，導(dǎo)致volatile修飾無效，可能引發(fā)問題.這種不一致的定義聲明方式在一些編譯器中是合法的，因此需要進(jìn)行約束.

規(guī)則3.當(dāng)采用中斷屏蔽機(jī)制進(jìn)行原子區(qū)加鎖保護(hù)時，禁止在同一條執(zhí)行路徑上出現(xiàn)兩次以上嵌套加鎖/解鎖操作.

規(guī)則原理：每一對加鎖/解鎖操作都期望保護(hù)一段完整的臨界區(qū)不被打斷，若嵌套額外的加鎖/解鎖操作隊(duì)時，內(nèi)層的解鎖操作會使外層臨界區(qū)處于開放狀態(tài)，從而引發(fā)非預(yù)期的數(shù)據(jù)訪問沖突.

2.2 SpaceCCH工具及規(guī)則擴(kuò)展

SpaceCCH工具是由北京控制工程研究所自主研發(fā)的面向高安全軟件系統(tǒng)的靜態(tài)代碼檢查工具，能夠?qū)Τ^250條編碼規(guī)則進(jìn)行自動審查.SpaceCCH工具采用插件式的體系結(jié)構(gòu)，提供基于統(tǒng)一中間表示(抽象語法樹、符號表、控制流圖)的擴(kuò)展開發(fā)API，支持自定義規(guī)則的快速開發(fā).SpaceCCH工具的系統(tǒng)結(jié)構(gòu)如圖5所示.

SpaceCCH工具由前端分析器和靜態(tài)分析引擎兩部分組成.

其中，前端分析器又包括詞法分析器、語法分析器和AST分析器三部分.以給定源程序?yàn)檩斎?，首先由詞法分析器和語法分析器處理，并獲得程序的抽象語法樹，此后AST分析器通過對AST的一系列分析處理，最終產(chǎn)生靜態(tài)分析過程所需的中間表示，主要包括控制流圖(control flow graph, CFG)、調(diào)用圖、符號表和抽象語法樹(abstract syntax tree, AST).

靜態(tài)分析引擎包括控制流分析器、數(shù)據(jù)流分析器、規(guī)則檢查引擎等.其中，控制流分析器主要用于對提取控制路徑、檢測循環(huán)、處理函數(shù)調(diào)用等；數(shù)據(jù)流分析器主要完成對循環(huán)的局部數(shù)據(jù)流分析，產(chǎn)生迭代分析的結(jié)果供整體分析過程利用；規(guī)則檢查器以及實(shí)例化的規(guī)則實(shí)現(xiàn)負(fù)責(zé)完成相應(yīng)的規(guī)則檢查功能.靜態(tài)分析引擎以前端輸出的四種中間表示為輸入，經(jīng)過控制流分析器、數(shù)據(jù)流分析器和規(guī)則檢查器的共同處理，最后生成缺陷報(bào)告.

SpaceCCH提供了符號表檢索、AST遍歷、數(shù)據(jù)流分析和類型檢查等豐富的擴(kuò)展接口，本文基于上述接口對規(guī)則1、2進(jìn)行了擴(kuò)展.其中，規(guī)則1通過調(diào)用圖分析結(jié)果，根據(jù)AST特征收集中斷或任務(wù)中使用的所有I/O端口、全局變量、絕對地址指針變量，進(jìn)一步根據(jù)規(guī)則1的要求篩選出相關(guān)數(shù)據(jù)的聲明語句，判斷其是否采用volatile修飾，確定是否違反規(guī)則、存在潛在的數(shù)據(jù)訪問沖突風(fēng)險；規(guī)則2通過跨文件符號表檢索獲得所有volatile修飾的符號定義，再判斷該定義對應(yīng)的符號聲明是否也用volatile修飾，實(shí)現(xiàn)對該規(guī)則的檢查.

2.3 面向有限狀態(tài)機(jī)規(guī)則的靜態(tài)分析

針對規(guī)則3，本文提出一種基于有限狀態(tài)機(jī)規(guī)則的靜態(tài)分析方法.在這種方法中，一條規(guī)則R可以采用一個擴(kuò)展的有限狀態(tài)機(jī)來表示，其對應(yīng)的擴(kuò)展?fàn)顟B(tài)機(jī)模型為M=〈Q,P,δ,q0,F〉，其中：

1)Q是規(guī)則中定義的狀態(tài)的集合.

2)P是M的模式集合，只有輸入字母能與P中某個模式相匹配時，該輸入才被狀態(tài)機(jī)所接收，從而觸發(fā)狀態(tài)轉(zhuǎn)移.

3)δ是M的轉(zhuǎn)移函數(shù)，指定狀態(tài)機(jī)從某一狀態(tài)遷移到下一狀態(tài).

4)q0是M的初始狀態(tài).

5)F是狀態(tài)機(jī)的終止?fàn)顟B(tài)，即規(guī)則的錯誤狀態(tài).

規(guī)則3對應(yīng)的狀態(tài)機(jī)模型示例圖如圖6所示.其中，狀態(tài)集Q={初始態(tài),加鎖態(tài),多重加鎖態(tài),錯誤態(tài)}，模式集P={lock, unlock}，對應(yīng)中斷屏蔽和打開的C語言操作.狀態(tài)機(jī)模型是靜態(tài)分析時狀態(tài)機(jī)實(shí)例的元模型，狀態(tài)機(jī)實(shí)例的狀態(tài)值來源于該模型的狀態(tài)集合，同樣初始狀態(tài)和終止?fàn)顟B(tài)也是在模型中所定義的.當(dāng)一個M的狀態(tài)機(jī)實(shí)例到達(dá)狀態(tài)機(jī)模型中的錯誤狀態(tài)時即表明違反給定規(guī)則的錯誤出現(xiàn).

在對該規(guī)則進(jìn)行檢查的算法(如圖7所示)是：

1)給定被測程序的入口函數(shù)控制流圖cfg、當(dāng)前程序狀態(tài)ps和規(guī)則r，調(diào)用check函數(shù)進(jìn)行檢查；初始時ps為基于該狀態(tài)機(jī)模型創(chuàng)建的狀態(tài)機(jī)實(shí)例I，I為初始態(tài)；

2)靜態(tài)分析引擎依次對主程序或中斷的入口函數(shù)CFG進(jìn)行深度優(yōu)先遍歷；

3)在對路徑中每個節(jié)點(diǎn)進(jìn)行分析時，規(guī)則檢查器根據(jù)狀態(tài)機(jī)實(shí)例當(dāng)前狀態(tài)、節(jié)點(diǎn)操作與模式的匹配情況決定是否進(jìn)行狀態(tài)轉(zhuǎn)移，當(dāng)程序狀態(tài)中的某個狀態(tài)機(jī)實(shí)例轉(zhuǎn)移到錯誤狀態(tài)時，表示程序中出現(xiàn)了違反給定規(guī)則的錯誤.

為了提高錯誤檢測的精確性，SpaceCCH靜態(tài)分析引擎引入路徑敏感分析，并且支持上下文敏感的過程間分析.考慮到效率和可伸縮性，SpaceCCH在遍歷分析的環(huán)節(jié)采用了一系列緩存優(yōu)化機(jī)制，顯著地加快了分析過程，這些方法與文獻(xiàn)[2]相同.

3 實(shí)驗(yàn)與評估

為了對SpaceCCH的分析性能和分析精確度等指標(biāo)進(jìn)行評估，針對本文提出的3條與數(shù)據(jù)訪問沖突相關(guān)的編碼規(guī)則，選取4個真實(shí)的星上軟件樣本進(jìn)行了實(shí)驗(yàn).實(shí)驗(yàn)是在一臺普通的HP PC機(jī)(CPU為Intel Core 2 2.40 G，內(nèi)存為2 GB)上進(jìn)行的，表1給出了每個被分析軟件的屬性以及分析的各項(xiàng)指標(biāo).

從實(shí)驗(yàn)結(jié)果中可以看出，SpaceCCH能夠適應(yīng)于各種編譯配置下的軟件，如軟件B和軟件D分別采用Keil C51和SPARC擴(kuò)展的C方言進(jìn)行編程.對于規(guī)模最大的軟件A，SpaceCCH在12.185秒內(nèi)就能完成分析，并且只占用28.65 M的內(nèi)存，表明工具具有良好的可伸縮性.由于軟件樣本的限制，本文沒有對規(guī)模更大的軟件進(jìn)行實(shí)驗(yàn).

被分析項(xiàng)編譯配置規(guī)模(LOC)分析時間/s內(nèi)存峰值/M規(guī)則1違反預(yù)埋規(guī)則2違反預(yù)埋規(guī)則3違反預(yù)埋誤報(bào)漏報(bào)軟件AANSIC1086212.185028.6561000軟件BKeilC5116710.76504.4121100軟件CANSIC942716.387023.4272000軟件DgccforSPARC34871.37504.5331000

本文針對3條規(guī)則在4個被測軟件中預(yù)埋了一定數(shù)量的違反，如表1所示.在實(shí)驗(yàn)中，未發(fā)現(xiàn)SpaceCCH的分析結(jié)果中存在誤報(bào)，并且實(shí)現(xiàn)了零漏報(bào).這是因?yàn)?，本文從方法學(xué)上把一個復(fù)雜數(shù)據(jù)訪問沖突缺陷的檢測轉(zhuǎn)換為了對特定編碼規(guī)則的檢查，編碼規(guī)則檢查方法較少涉及程序行為的分析，是可判定的.

上述實(shí)驗(yàn)結(jié)果表明：

1)SpaceCCH具有良好的可伸縮性，能夠適用于大規(guī)模航天嵌入式軟件的編碼規(guī)則檢查，而且具有較好的分析精度和分析性能；

2)本文提出的3條編碼規(guī)則在SpaceCCH中得到了實(shí)現(xiàn)，并能夠有效檢測出潛在的數(shù)據(jù)訪問沖突缺陷.

4 結(jié)束語

本文針對航天嵌入式軟件中斷數(shù)據(jù)訪問沖突中兩類難以測試的缺陷模式，提出了相應(yīng)的3條編碼規(guī)則，用以在編碼階段有效避免相關(guān)的數(shù)據(jù)訪問沖突問題.基于編碼規(guī)則，對一個已有的靜態(tài)代碼檢查工具SpaceCCH進(jìn)行了擴(kuò)展，并提出了一個基于有限狀態(tài)機(jī)規(guī)則的靜態(tài)分析方法，實(shí)現(xiàn)了對3條編碼規(guī)則的自動檢查.實(shí)驗(yàn)結(jié)果表明，擴(kuò)展后的SpaceCCH能夠高效、精確地對相應(yīng)的編碼規(guī)則違反進(jìn)行自動檢查，從而避免數(shù)據(jù)訪問沖突問題的發(fā)生.

[1] 楊孟飛, 顧斌, 郭向英, 等. 航天嵌入式軟件可信性保障技術(shù)及應(yīng)用研究[J]. 中國科學(xué): 技術(shù)科學(xué), 2015(2):198-203. YANG M F， GUO B, GUO X Y, et al. Aerospace embeded software dependability guarantee technology and application[J]. Scientia Sinica Technologica, 2015(2):198-203.

[2] 陳睿, 楊孟飛, 郭向英. 基于變量訪問序模式的中斷數(shù)據(jù)競爭檢測方法[J].軟件學(xué)報(bào),2016, 27(3): 547-561. CHEN R, YANG M F, GUO X Y. Interrupt data race detection based on shared variable access order pattern[J]. Journal of Software, 2016, 27(3): 547-561.

[3] 段永顥,陳睿.基于啟發(fā)式的靜態(tài)中斷數(shù)據(jù)競爭檢測方法[J].計(jì)算機(jī)工程與設(shè)計(jì),2013,34(1):140-145. DUAN Y H, CHEN R. Heuristic static data race detection for interrupt-driven software[J]. Computer Engineering and Design, 2013,34(1):140-145.

[4] CHEN R, GUO X Y, DUAN Y H, et al. Static data race detection for interrupt-driven embedded software[C]//International Conference on Secure Integration and Reliability Improvement. New York: IEEE,2011，47-52.

[5] REGEHR J, COOPRIDER N. Interrupt verification via thread verification[J]. Electron. Notes Theoretical Computer Science,2007,174(9).

[6] 周筱羽, 顧斌, 趙建華,等.中斷驅(qū)動系統(tǒng)模型檢驗(yàn)[J]. 軟件學(xué)報(bào),2015,26(9):2221-2230. ZHOU X Y, GU B,ZHAO J H, et al. Model checking technique for interrupt-driven system[J]. Journal of Software,2015,26(9):2221-2230.

[7] WU X G, Wen Y J, CHEN L Q, et al. Data race detection for interrupt-driven programs via bounded model checking[C]//The IEEE 7thInternational Conference on Software Security and Reliability-Companion(SERE-C).New York: IEEE,2013,204-210.

[8] 霍瑋,于洪濤, 馮曉兵,等.靜態(tài)檢測中斷驅(qū)動程序的數(shù)據(jù)競爭[J].計(jì)算機(jī)研究與發(fā)展,2011,48(12):2290-2299. HUO W YU H T, FENG X B, et al. Static data race detection of interrupt-driven programs[J].Journal of Computer Research and Development,2011,48(12):2290-2299.

[9] 陳園軍,石浚菁,王林章,等.中斷驅(qū)動的嵌入式系統(tǒng)數(shù)據(jù)競爭檢測工具[J].計(jì)算機(jī)科學(xué)與探索, 2015, 9(8):914-925. CHEN Y J, SHI J J, WANG L Z, et al. Data race detection tool for interrupt-driven embedded system[J]. Journal of Frontiers of Computer Science and Technology, 2015,9(8):914-925.

[10] Motor Industry Software Reliability Association (MISRA). Guidelines for the use of the C language in critical systems[S].MISRA-C, 2004.

[11] The Power of Ten . Rules for developing safety critical code[J]. IEEE Computer, 2006:93-95.

Coding Rule Based Interrupt Data Race Detection Method

CHEN Rui1,2, YANG Mengfei1,3

(1.BeijingInstituteofControlEngineering，Beijing100190，China；2.BeijingSunwiseInformationTechnologyCo.Ltd.，Beijing100190，China；3.ChinaAcademyofSpaceTechnology,Beijing100094,China)

To solve pattern “double lock & unlock” and pattern “misuse of volatile”, a detection method based on coding rules is proposed. Firstly, the failure mechanism is analyzed, and then 3 coding rules are proposed to avoid corresponding defects in development stage. These rules and corresponding checking methods are researched and implemented by extending an existing static analysis tool named SpaceCCH. The evaluation result based on real world on-board software show that, the extended SpaceCCH can find rules violations efficiently with low false positive rate and low false negative rate, by which the data race bugs of pattern “double lock & unlock” and pattern “misuse of volatile” can be avoided effectively. The main contribution of this paper is that the detection of a really complex bug is transformed to corresponding coding rules and their automatic detection.

data race； coding rule； static analysis； aerospace embedded software

*國家自然科學(xué)基金資助項(xiàng)目(91118007,61632005).

2017-02-01

陳 睿(1984—)，男，高級工程師，研究方向?yàn)槌绦蚍治雠c軟件測試；楊孟飛(1962—),男,研究員,研究方向?yàn)榭臻g飛行器系統(tǒng)設(shè)計(jì)、控制計(jì)算機(jī)系統(tǒng)及嵌入式軟件.

TP311

A

1674-1579(2017)03-0059-07

10.3969/j.issn.1674-1579.2017.03.010