陳睿，楊孟飛

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

?

航天嵌入式軟件數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集研究

陳睿1，2，楊孟飛3，*

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

針對(duì)數(shù)據(jù)訪問(wèn)沖突問(wèn)題的檢測(cè)方法及工具的研究很多，但缺少對(duì)其進(jìn)行評(píng)估的基準(zhǔn)測(cè)試集。文章基于大量真實(shí)航天嵌入式軟件中斷數(shù)據(jù)訪問(wèn)沖突案例研究的結(jié)果，總結(jié)出影響數(shù)據(jù)訪問(wèn)沖突檢測(cè)的6類(lèi)要素，設(shè)計(jì)開(kāi)發(fā)了嵌入式軟件中斷數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集程序RaceBench，對(duì)SpaceDRC工具進(jìn)行了指標(biāo)評(píng)估。結(jié)果表明，RaceBench能夠有效評(píng)估工具的適用性。

數(shù)據(jù)訪問(wèn)沖突；基準(zhǔn)測(cè)試集；航天嵌入式軟件；數(shù)據(jù)競(jìng)爭(zhēng)；軟件測(cè)試

數(shù)據(jù)訪問(wèn)沖突問(wèn)題是嵌入式軟件中一類(lèi)典型的并發(fā)缺陷，曾經(jīng)引發(fā)嚴(yán)重的安全事故[1-2]，也是當(dāng)前航天型號(hào)軟件開(kāi)發(fā)中最難解決的問(wèn)題之一[3]。在學(xué)術(shù)領(lǐng)域或工程領(lǐng)域，數(shù)據(jù)競(jìng)爭(zhēng)(Data Race)、原子性問(wèn)題、數(shù)據(jù)訪問(wèn)沖突或共享數(shù)據(jù)問(wèn)題都屬于這一概念。這類(lèi)問(wèn)題發(fā)生在中斷驅(qū)動(dòng)型程序或多任務(wù)程序中，當(dāng)兩個(gè)不同的中斷(或任務(wù))對(duì)同一個(gè)共享數(shù)據(jù)進(jìn)行同時(shí)的讀寫(xiě)訪問(wèn)，且至少存在一次寫(xiě)操作時(shí)。由于兩次訪問(wèn)的時(shí)序不可確定，程序會(huì)因此產(chǎn)生異常行為，如關(guān)鍵數(shù)據(jù)被非預(yù)期地修改，嚴(yán)重時(shí)甚至導(dǎo)致系統(tǒng)或軟件失效。例如，某衛(wèi)星翼板驅(qū)動(dòng)線路盒轉(zhuǎn)角跳變導(dǎo)致控制偏差等。根據(jù)數(shù)據(jù)統(tǒng)計(jì)，近五年在中國(guó)衛(wèi)星總裝集成測(cè)試階段發(fā)現(xiàn)的軟件質(zhì)量問(wèn)題中，超過(guò)13%都與數(shù)據(jù)訪問(wèn)沖突問(wèn)題密切相關(guān)。這些問(wèn)題一旦遺漏至實(shí)際飛行階段，后果將不堪設(shè)想。

值得注意的是，數(shù)據(jù)訪問(wèn)沖突問(wèn)題發(fā)生概率小、難以復(fù)現(xiàn)，往往在特殊的外部條件和中斷(或任務(wù))交迭情況下才會(huì)出現(xiàn)，難以通過(guò)傳統(tǒng)的軟件測(cè)試方法發(fā)現(xiàn)，遺漏率較高。因此，近年來(lái)數(shù)據(jù)訪問(wèn)沖突自動(dòng)檢測(cè)方法已成為研究熱點(diǎn)，國(guó)家自然科學(xué)基金“可信軟件基礎(chǔ)研究”重大研究計(jì)劃及民用航天預(yù)先研究等都先后資助了相關(guān)課題，產(chǎn)生了一批有價(jià)值的方法或工具成果[4-13]，隨著研究的不斷深入，未來(lái)還將產(chǎn)生更多的成果。

不同的數(shù)據(jù)訪問(wèn)沖突檢測(cè)方法或工具在實(shí)際代碼中應(yīng)用時(shí)，檢出率、誤報(bào)率、性能等技術(shù)指標(biāo)存在較大差異。一方面，在工程實(shí)踐中選取合適的工具時(shí)需要一個(gè)統(tǒng)一的評(píng)價(jià)標(biāo)準(zhǔn)進(jìn)行指導(dǎo)；另一方面，工具的研究設(shè)計(jì)者也希望了解自己的成果在工程實(shí)踐中的適用性及與其他競(jìng)爭(zhēng)成果的優(yōu)劣比較，為進(jìn)一步改進(jìn)研究提供指導(dǎo)。

基準(zhǔn)測(cè)試集是一種有效、低成本的評(píng)估和度量手段。一個(gè)獲得廣泛認(rèn)可的基準(zhǔn)測(cè)試集具有重要的技術(shù)價(jià)值和社會(huì)影響。目前有很多應(yīng)用廣泛的標(biāo)準(zhǔn)測(cè)試集，如用于性能評(píng)估的SPEC[14]和TPC[15]系列。對(duì)于代碼缺陷檢測(cè)，近年來(lái)也出現(xiàn)一些基準(zhǔn)測(cè)試集，如BegBunch[16]，BugBench[17]及美國(guó)國(guó)家標(biāo)準(zhǔn)技術(shù)研究院的SAMATE SRD項(xiàng)目[18]。這些基準(zhǔn)測(cè)試集都基于開(kāi)源軟件建立，多面向非嵌入式程序和通用類(lèi)型缺陷，由于數(shù)據(jù)訪問(wèn)沖突問(wèn)題的特殊性及嵌入式軟件的封閉性和多樣性，并不能用于評(píng)估針對(duì)數(shù)據(jù)訪問(wèn)沖突的檢測(cè)工具。

因此本文對(duì)航天嵌入式軟件數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集開(kāi)展研究，通過(guò)對(duì)大量真實(shí)案例的系統(tǒng)研究得出6類(lèi)影響數(shù)據(jù)訪問(wèn)沖突檢測(cè)的關(guān)鍵要素，基于此設(shè)計(jì)開(kāi)發(fā)了已知首個(gè)中斷數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集RaceBench，該基準(zhǔn)測(cè)試集的構(gòu)建遵循代表性、多樣性、公平性和適應(yīng)性原則。本文基于RaceBench對(duì)一個(gè)已有的數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)工具SpaceDRC進(jìn)行評(píng)估，驗(yàn)證了該基準(zhǔn)測(cè)試集能夠有效評(píng)估工具的檢出率和誤報(bào)率等指標(biāo)。我們計(jì)劃未來(lái)公開(kāi)RaceBench的源代碼，可為其他研究中斷數(shù)據(jù)訪問(wèn)沖突問(wèn)題的學(xué)者提供開(kāi)放的測(cè)試集。

1 中斷數(shù)據(jù)訪問(wèn)沖突問(wèn)題要素

本文對(duì)大量真實(shí)航天嵌入式軟件數(shù)據(jù)訪問(wèn)沖突案例進(jìn)行系統(tǒng)分析，綜合檢測(cè)技術(shù)、軟件特征、缺陷特征等多種因素，提煉出數(shù)據(jù)訪問(wèn)沖突問(wèn)題的關(guān)鍵要素，作為構(gòu)建基準(zhǔn)測(cè)試集的基礎(chǔ)。

本節(jié)對(duì)問(wèn)題特征分析的方法學(xué)和結(jié)果進(jìn)行說(shuō)明。

1.1 案例分析方法概述

首先，對(duì)航天嵌入式軟件第三方評(píng)測(cè)問(wèn)題庫(kù)、第三方評(píng)測(cè)遺漏問(wèn)題庫(kù)和北京控制工程研究所軟件問(wèn)題案例進(jìn)行了分析，通過(guò)關(guān)鍵字查詢(xún)的方式初步篩選出124個(gè)相關(guān)缺陷。經(jīng)過(guò)進(jìn)一步的去重和精化，最終獲得100個(gè)樣本缺陷。

然后，進(jìn)行缺陷特征信息采集，包括：1)確定與缺陷特征與統(tǒng)計(jì)分析相關(guān)的因素，包括軟件名、運(yùn)行環(huán)境、并發(fā)體系結(jié)構(gòu)、規(guī)模、問(wèn)題，描述、代碼片段、共享數(shù)據(jù)類(lèi)型、問(wèn)題處理方式；2)設(shè)計(jì)相應(yīng)的表格收集缺陷信息。缺陷特征信息的收集是一個(gè)迭代的過(guò)程，在此過(guò)程中，需要查看問(wèn)題管理系統(tǒng)中的問(wèn)題描述、定位代碼，比對(duì)獲取后續(xù)版本的修改策略。

最后，經(jīng)過(guò)統(tǒng)計(jì)分析，得出特征結(jié)果。

1.2 數(shù)據(jù)訪問(wèn)沖突問(wèn)題要素

經(jīng)案例分析得出，數(shù)據(jù)訪問(wèn)沖突問(wèn)題有軟件特征和缺陷特征兩方面的要素，如圖1所示。其中，軟件特征包括并發(fā)體系結(jié)構(gòu)、開(kāi)發(fā)語(yǔ)言及運(yùn)行環(huán)境等；缺陷特征包括并發(fā)關(guān)系、數(shù)據(jù)訪問(wèn)方式、共享數(shù)據(jù)的類(lèi)型、控制流場(chǎng)景和缺陷模式。

1.2.1 要素1：軟件并發(fā)體系結(jié)構(gòu)

數(shù)據(jù)訪問(wèn)沖突是一種典型的并發(fā)缺陷，軟件的并發(fā)體系結(jié)構(gòu)與缺陷檢測(cè)之間存在直接的關(guān)系。航天嵌入式軟件是典型的強(qiáng)實(shí)時(shí)系統(tǒng)，且存在多種并發(fā)方式。主要采用兩種并發(fā)體系結(jié)構(gòu)：

(1)主循環(huán)+中斷結(jié)構(gòu)(Round-Robin with Interrupts)

在簡(jiǎn)單輪詢(xún)式結(jié)構(gòu)的基礎(chǔ)上引入中斷，稱(chēng)為主循環(huán)+中斷結(jié)構(gòu)(Round Robin with Interrupts，RRI)。在這種結(jié)構(gòu)下，緊急任務(wù)可以在中斷服務(wù)程序中得到處理，某些情況下可能在中斷中設(shè)置標(biāo)志，在主循環(huán)中完成后續(xù)處理，圖2給出了一個(gè)RRI架構(gòu)的示例程序。主循環(huán)+中斷結(jié)構(gòu)提高了對(duì)高優(yōu)先級(jí)任務(wù)的響應(yīng)能力，但與此同時(shí)，引入了新的問(wèn)題，即共享數(shù)據(jù)的訪問(wèn)沖突。如果中斷在使用共享變量進(jìn)行計(jì)算的過(guò)程中發(fā)生，并且修改了共享變量的值，則會(huì)導(dǎo)致數(shù)據(jù)訪問(wèn)沖突問(wèn)題。這種情況下，必須采取措施保護(hù)低優(yōu)先級(jí)計(jì)算過(guò)程的原子性，例如通過(guò)中斷屏蔽方式保護(hù)臨界代碼段。

(2)實(shí)時(shí)多任務(wù)操作系統(tǒng)+中斷結(jié)構(gòu)

隨著航天嵌入式系統(tǒng)功能越來(lái)越復(fù)雜，軟件的模塊和規(guī)模越來(lái)越大，使用實(shí)時(shí)多任務(wù)操作系統(tǒng)(Real Time Operating System，RTOS)逐漸變得普遍。在基于RTOS的應(yīng)用程序中，沒(méi)有主循環(huán)，通過(guò)創(chuàng)建新任務(wù)可以實(shí)現(xiàn)主循環(huán)的功能。由于航天嵌入式系統(tǒng)對(duì)外部事件響應(yīng)的實(shí)時(shí)性要求高、與外界交互多，一般在RTOS中也引入中斷，用于處理非常關(guān)鍵的外部事件，形成一種異構(gòu)的并發(fā)體系結(jié)構(gòu)，本文稱(chēng)之為RTOS-ISR。在這種并發(fā)結(jié)構(gòu)中，高優(yōu)先級(jí)和低優(yōu)先級(jí)任務(wù)之間可以對(duì)稱(chēng)交迭，但中斷與任務(wù)的搶占關(guān)系是非對(duì)稱(chēng)的，即只有中斷可以搶占任務(wù)，反之則不行。

(3)并發(fā)體系結(jié)構(gòu)分布分析

根據(jù)案例分析數(shù)據(jù)統(tǒng)計(jì)，并發(fā)體系結(jié)構(gòu)為RR-ISR的缺陷占82%，RTOS-ISR占18%。這種差異主要是由于航天嵌入式軟件本身采用的并發(fā)體系結(jié)構(gòu)分布導(dǎo)致的。需要注意的是，RTOS-ISR結(jié)構(gòu)的程序呈上升趨勢(shì)，為研究帶來(lái)新的問(wèn)題。本文在構(gòu)建基準(zhǔn)測(cè)試集時(shí)考慮到了這種統(tǒng)計(jì)差異。

1.2.2 要素2：軟件形態(tài)及運(yùn)行環(huán)境

軟件形態(tài)包括編程語(yǔ)言和軟件規(guī)模兩個(gè)方面。

一般而言，無(wú)論是動(dòng)態(tài)還是靜態(tài)的檢測(cè)工具都依賴(lài)于被測(cè)軟件的編程語(yǔ)言，其中動(dòng)態(tài)工具需要對(duì)源代碼進(jìn)行插樁以獲取運(yùn)行時(shí)信息，靜態(tài)工具直接面向源程序。在本文所研究的案例中，95%的軟件采用C語(yǔ)言編程，其余采用相應(yīng)體系架構(gòu)(如SPARC、x86等)的匯編語(yǔ)言，語(yǔ)法及特征并不統(tǒng)一，因此本文研究的基準(zhǔn)測(cè)試集僅考慮C語(yǔ)言程序。

軟件規(guī)模從數(shù)百行到上萬(wàn)行不等，并發(fā)流個(gè)數(shù)與體系結(jié)構(gòu)相關(guān)，中斷服務(wù)程序少于5個(gè)。

航天嵌入式軟件的硬件運(yùn)行環(huán)境多樣，以SPARC、x86、MCS-51、DSP等體系結(jié)構(gòu)的處理器為主。中斷并發(fā)機(jī)制與處理器架構(gòu)相關(guān)，多為固定優(yōu)先級(jí)非對(duì)稱(chēng)搶占，各種處理器都有類(lèi)似的中斷屏蔽機(jī)制實(shí)現(xiàn)中斷并發(fā)的互斥。

表1給出了案例在不同處理器上的分布數(shù)據(jù)。其中，68%的缺陷發(fā)生在8051平臺(tái)上，這類(lèi)軟件多為中小規(guī)模。同時(shí)，隨著SPARC處理器及DSP處理器在航天領(lǐng)域的廣泛應(yīng)用，在中大規(guī)模的軟件中該類(lèi)缺陷也逐漸增多。

表1 數(shù)據(jù)訪問(wèn)沖突缺陷處理器分布

1.2.3 要素3：共享數(shù)據(jù)類(lèi)型及訪問(wèn)方式

共享數(shù)據(jù)的類(lèi)型是影響中斷數(shù)據(jù)訪問(wèn)沖突檢測(cè)的關(guān)鍵因素。不同數(shù)據(jù)類(lèi)型的共享數(shù)據(jù)在沖突方式上表現(xiàn)不同，例如結(jié)構(gòu)體變量的沖突多發(fā)生在不同成員訪問(wèn)的不一致性，數(shù)組變量的沖突發(fā)生在不同元素訪問(wèn)中，因此對(duì)檢測(cè)工具的能力要求也不同。目前航天嵌入式軟件并發(fā)問(wèn)題中表現(xiàn)出的沖突變量類(lèi)型包括：

1)基本類(lèi)型：共享數(shù)據(jù)為int、short、double等多字節(jié)基本類(lèi)型，對(duì)這類(lèi)變量的沖突發(fā)生在單個(gè)變量單次訪問(wèn)、單個(gè)變量多次訪問(wèn)或者多個(gè)變量一致性訪問(wèn)等幾種情況中?；绢?lèi)型的數(shù)據(jù)也包括對(duì)I/O端口的訪問(wèn)。

2)數(shù)組：共享數(shù)據(jù)的類(lèi)型為數(shù)組。當(dāng)按照一定順序依次訪問(wèn)數(shù)組多個(gè)元素時(shí)，可能發(fā)生多個(gè)元素訪問(wèn)不一致的情況。

3)結(jié)構(gòu)體：共享數(shù)據(jù)采用結(jié)構(gòu)體類(lèi)型，同一個(gè)數(shù)據(jù)的不同成員之間可能由于沖突導(dǎo)致完整性被破壞。

4)聯(lián)合體：代碼中對(duì)聯(lián)合體不同成員的訪問(wèn)應(yīng)當(dāng)作對(duì)同一數(shù)據(jù)單元的操作，但是很多檢測(cè)工具往往不能進(jìn)行這種處理，因此是否支持聯(lián)合體是對(duì)工具評(píng)估的一項(xiàng)要素。

5)指針類(lèi)型：指針變量本身發(fā)生沖突，可能導(dǎo)致被訪問(wèn)的具體數(shù)據(jù)是不一致的。

在C語(yǔ)言程序中，對(duì)上述類(lèi)型的共享數(shù)據(jù)進(jìn)行訪問(wèn)的方式通常有兩種，一是通過(guò)變量賦值和讀取，二是通過(guò)指針解引用間接訪問(wèn)。其中，工具對(duì)前者的支持相對(duì)容易，對(duì)后者的支持需要引入稍復(fù)雜的指針?lè)治黾夹g(shù)，而是否精確又取決于所采用的指針?lè)治鏊惴ǖ木?。在本文研究的案例中，通過(guò)指針解引用進(jìn)行共享數(shù)據(jù)訪問(wèn)占到15%，共享數(shù)據(jù)訪問(wèn)方式也是對(duì)工具評(píng)估的要素之一。

1.2.4 要素4：控制流場(chǎng)景

無(wú)論動(dòng)態(tài)或靜態(tài)檢測(cè)技術(shù)，控制流場(chǎng)景都可能影響分析的精度和效率。在航天嵌入式軟件中，控制流場(chǎng)景包括：

1)函數(shù)嵌套：對(duì)于靜態(tài)檢測(cè)，對(duì)函數(shù)嵌套的支持需要引入過(guò)程間分析技術(shù)，否則將無(wú)法正確識(shí)別出通過(guò)底層函數(shù)對(duì)共享數(shù)據(jù)的讀寫(xiě)操作。

2)中斷嵌套：中斷嵌套可被看作一種特殊的函數(shù)嵌套，但與函數(shù)調(diào)用不同，內(nèi)層中斷的觸發(fā)不是顯式的，具有不確定性。對(duì)中斷嵌套的支持意味著分析的復(fù)雜度會(huì)指數(shù)級(jí)增長(zhǎng)。

3)分支訪問(wèn)：分支訪問(wèn)會(huì)影響檢測(cè)工具的誤報(bào)率，當(dāng)沒(méi)有引入路徑敏感分析時(shí)，工具不能識(shí)別出兩個(gè)互斥分支是不可行路徑，將導(dǎo)致較高的誤報(bào)率。

1.2.5 要素5：并發(fā)關(guān)系

在不同并發(fā)體系結(jié)構(gòu)下，數(shù)據(jù)訪問(wèn)沖突涉及的并發(fā)關(guān)系對(duì)工具的檢測(cè)能力是一項(xiàng)挑戰(zhàn)。并發(fā)關(guān)系包括：

1)任務(wù)與中斷：任務(wù)中的數(shù)據(jù)訪問(wèn)被中斷搶占而發(fā)生沖突。其中任務(wù)泛指主循環(huán)任務(wù)或?qū)崟r(shí)操作系統(tǒng)中的任務(wù)；

2)中斷與中斷：指低優(yōu)先級(jí)中斷被高優(yōu)先級(jí)中斷搶占而發(fā)生沖突。

3)任務(wù)與任務(wù)：在實(shí)時(shí)操作系統(tǒng)下，多個(gè)任務(wù)之間未正確進(jìn)行同步或互斥導(dǎo)致發(fā)生數(shù)據(jù)訪問(wèn)沖突。

在不同并發(fā)關(guān)系下，數(shù)據(jù)訪問(wèn)沖突發(fā)生的場(chǎng)景及缺陷特征表現(xiàn)不同，因此對(duì)檢測(cè)技術(shù)及工具的要求也不同。

1.2.6 要素6：缺陷模式

根據(jù)本文前期研究[6]，航天嵌入式軟件中存在共7種數(shù)據(jù)訪問(wèn)沖突缺陷模式。其中模式1、模式2、模式3、模式5等4種缺陷模式可在軟件代碼上體現(xiàn)，且適合用工具進(jìn)行自動(dòng)化檢測(cè)。模式4屬于系統(tǒng)設(shè)計(jì)導(dǎo)致的缺陷，需從設(shè)計(jì)層面解決；模式6通過(guò)相關(guān)編碼規(guī)范來(lái)進(jìn)行約束，并不屬于一般數(shù)據(jù)訪問(wèn)沖突檢測(cè)工具研究的重點(diǎn)；模式7無(wú)法采用自動(dòng)化的方法，一般通過(guò)代碼審查即可有效識(shí)別。本文所關(guān)注的4種模式(詳見(jiàn)文獻(xiàn)[6])如下：

1)模式1：?jiǎn)巫兞吭L問(wèn)序模式。

2)模式2：多個(gè)關(guān)聯(lián)變量訪問(wèn)一致性被破壞。

3)模式3：多字節(jié)變量訪問(wèn)原子性被破壞。

4)模式5：重復(fù)加鎖解鎖。

2 數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集 RaceBench

2.1 設(shè)計(jì)準(zhǔn)則

基于第1節(jié)研究的要素集，本文按照以下原則設(shè)計(jì)開(kāi)發(fā)了一個(gè)航天嵌入式軟件數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集RaceBench：

1)代表性?；鶞?zhǔn)測(cè)試集要能夠接近真實(shí)程序，代表真實(shí)軟件和真實(shí)缺陷。由于嵌入式軟件的封閉性，RaceBench無(wú)法像其他基準(zhǔn)測(cè)試集一樣通過(guò)收集開(kāi)源程序完成，而是基于一個(gè)廣泛應(yīng)用于航天型號(hào)的實(shí)時(shí)嵌入式操作系統(tǒng)SpaceOS2開(kāi)發(fā)。該操作系統(tǒng)具有多任務(wù)管理和中斷管理特性，能夠支持航天嵌入式軟件常用的兩種并發(fā)體系結(jié)構(gòu)，在軟件特征方面與真實(shí)嵌入式軟件保持一致，保證RaceBench的真實(shí)性和代表性。

2)多樣性。要能夠覆蓋不同類(lèi)型的程序及程序不同的特征，包括程序的體系結(jié)構(gòu)、程序的語(yǔ)法特征、缺陷模式類(lèi)型；RaceBench通過(guò)選取或設(shè)計(jì)相應(yīng)的程序，覆蓋航天嵌入式軟件特征及數(shù)據(jù)訪問(wèn)沖突缺陷特征的各個(gè)要素，保證基準(zhǔn)測(cè)試集具有多樣性。

3)適應(yīng)性。基準(zhǔn)測(cè)試集要能夠適應(yīng)不同的硬件平臺(tái)，具有平臺(tái)無(wú)關(guān)性；RaceBench將平臺(tái)無(wú)關(guān)的特征考慮到構(gòu)建中，而與平臺(tái)相關(guān)的一些特性對(duì)檢測(cè)方法研究并不具有普適性，本文并未考慮。

4)公平性。基準(zhǔn)測(cè)試集的設(shè)計(jì)不應(yīng)傾向于某個(gè)特定的工具或方法，保證具有公平的評(píng)價(jià)能力。RaceBench的設(shè)計(jì)和選取完全來(lái)源于案例及其要素，不依賴(lài)于特定的方法和工具。

一個(gè)完善的基準(zhǔn)測(cè)試集需要持續(xù)地開(kāi)發(fā)豐富，RaceBench采用模塊化設(shè)計(jì)，便于對(duì)新要素覆蓋的擴(kuò)展。未來(lái)我們計(jì)劃開(kāi)源RaceBench，為其他研究中斷數(shù)據(jù)訪問(wèn)沖突檢測(cè)方法的學(xué)者提供研究基礎(chǔ)。

2.2 RaceBench的設(shè)計(jì)與實(shí)現(xiàn)

RaceBench是一個(gè)運(yùn)行在SpaceOS2上的應(yīng)用程序，采用實(shí)時(shí)多任務(wù)操作系統(tǒng)+中斷結(jié)構(gòu)，由主控調(diào)度程序及若干用例程序組成。其中，主控調(diào)度程序根據(jù)并發(fā)場(chǎng)景的設(shè)計(jì)調(diào)用各個(gè)用例程序，不同的用例程序覆蓋不同的數(shù)據(jù)訪問(wèn)沖突要素集合。

目前RaceBench包含14個(gè)用例程序，所有用例程序都來(lái)源于代表性的航天嵌入式軟件案例，各個(gè)用例程序的覆蓋情況如表2所示。表格填充表示測(cè)試程序?qū)υ撘馗采w。例如：用例1覆蓋了缺陷模式1中R-W-R的訪問(wèn)序情況，涉及了一個(gè)基本類(lèi)型的共享變量，沖突發(fā)生在任務(wù)與中斷中，程序通過(guò)變量讀寫(xiě)的方式訪問(wèn)共享數(shù)據(jù)，控制流場(chǎng)景中涉及了分支訪問(wèn)。

從表2可以看出，RaceBench的用例程序?qū)Ω鱾€(gè)要素都進(jìn)行了完整的覆蓋，具有多樣性的特征。在并發(fā)設(shè)計(jì)上，主控程序包括5個(gè)任務(wù)及4個(gè)中斷，優(yōu)先級(jí)各不相同。任務(wù)為循環(huán)運(yùn)行方式，每次循環(huán)完畢調(diào)用延時(shí)任務(wù)以實(shí)現(xiàn)任務(wù)的切換。4個(gè)中斷中3個(gè)為隨機(jī)觸發(fā)，1個(gè)為定時(shí)觸發(fā)。用例程序與各個(gè)任務(wù)和中斷的關(guān)系如表3所示。

主控程序負(fù)責(zé)發(fā)起5個(gè)任務(wù)，向操作系統(tǒng)掛載4個(gè)中斷，并在各個(gè)任務(wù)和中斷入口函數(shù)中按照設(shè)計(jì)調(diào)用用例程序。各個(gè)任務(wù)和中斷的屬性如表4所示。通過(guò)上述并發(fā)場(chǎng)景設(shè)計(jì)，RaceBench能夠模擬多級(jí)中斷嵌套和多種并發(fā)搶占，對(duì)檢測(cè)方法或工具的可伸縮性能夠較好地評(píng)估。

基于RaceBench可擴(kuò)展性設(shè)計(jì)，未來(lái)還將不斷加入新的樣例程序。

表2 用例程序?qū)Ω鱾€(gè)要素的覆蓋

表3 用例程序與任務(wù)和中斷的關(guān)系

表4 RaceBench中各個(gè)任務(wù)的屬性

3 試驗(yàn)評(píng)估

為了驗(yàn)證RaceBench對(duì)數(shù)據(jù)訪問(wèn)沖突檢測(cè)工具進(jìn)行評(píng)估的能力，本文選取一個(gè)靜態(tài)中斷數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)工具SpaceDRC進(jìn)行了試驗(yàn)。SpaceDRC是一個(gè)面向變量訪問(wèn)序模式的中斷數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)工具，是本文前期的研究工作。該工具能夠?qū)Σ糠謹(jǐn)?shù)據(jù)訪問(wèn)沖突問(wèn)題進(jìn)行有效識(shí)別，但受所采用技術(shù)的限制，仍然存在誤報(bào)和漏報(bào)，還處在不斷地優(yōu)化中。

SpaceDRC運(yùn)行于一臺(tái)型號(hào)為HP Compaq dc7900的計(jì)算機(jī)上，CPU為Intel Core2 Quad Q9650(3.00GHz，四核)，內(nèi)存為4GB，操作系統(tǒng)為Microsoft Windows 7。針對(duì)RaceBench的分析，SpaceDRC共報(bào)告23數(shù)據(jù)訪問(wèn)沖突，涉及96種場(chǎng)景，分析耗時(shí)69 s。經(jīng)分析，工具報(bào)告結(jié)果中包含21處真實(shí)缺陷、2處誤報(bào)和3處漏報(bào)。

其中2處誤報(bào)原因?yàn)椋篠paceDRC未考慮中斷的觸發(fā)時(shí)機(jī)，所涉及的并發(fā)場(chǎng)景在真實(shí)環(huán)境中無(wú)法復(fù)現(xiàn)。

對(duì)漏報(bào)情況的詳細(xì)分析如下：

1)case5中，在任務(wù)中對(duì)case5_x，case5_y和case5_z三個(gè)全局變量進(jìn)行讀，在中斷中取地址傳引用給writeVariable()函數(shù)中，再通過(guò)指針解引用對(duì)3個(gè)變量進(jìn)行寫(xiě)操作，如圖3(a)所示。SpaceDRC未能識(shí)別出通過(guò)指針解引用進(jìn)行共享數(shù)據(jù)訪問(wèn)導(dǎo)致的沖突。

2)case12中預(yù)埋了兩種類(lèi)型的沖突，包括指針解引用方式和聯(lián)合體成員別名方式，如圖3(b)所示。

對(duì)于前者，在低優(yōu)先級(jí)中斷中通過(guò)指向g1_case12的指針tmp解引用(*tmp=1)進(jìn)行寫(xiě)操作，在高優(yōu)先級(jí)中斷中直接對(duì)變量進(jìn)行寫(xiě)操作，兩者實(shí)際上存在沖突，但SpaceDRC未報(bào)告。

對(duì)于后者，在低優(yōu)先級(jí)中斷中對(duì)聯(lián)合體packet_case12的第1個(gè)成員header進(jìn)行賦值，在高級(jí)中斷中對(duì)其第2個(gè)成員進(jìn)行賦值，根據(jù)聯(lián)合體的語(yǔ)義定義，其第1個(gè)成員和第2個(gè)成員指向同一個(gè)內(nèi)存數(shù)據(jù)，因此上述操作是潛在的數(shù)據(jù)訪問(wèn)沖突，但SpaceDRC未報(bào)告。

根據(jù)以上試驗(yàn)結(jié)果可以得出對(duì)SpaceDRC的評(píng)估結(jié)論：

1)SpaceDRC的檢測(cè)能力覆蓋了各類(lèi)缺陷模式、并發(fā)關(guān)系和控制流場(chǎng)景；

2)SpaceDRC能夠支持3級(jí)中斷和5個(gè)以?xún)?nèi)任務(wù)的檢測(cè)；

3)SpaceDRC不支持指針解引用數(shù)據(jù)訪問(wèn)方式和聯(lián)合體數(shù)據(jù)類(lèi)型，根據(jù)第1.2.3節(jié)對(duì)共享數(shù)據(jù)訪問(wèn)方式的統(tǒng)計(jì)分析，指針解引用和聯(lián)合體別名方式僅占到15%?；诮y(tǒng)計(jì)學(xué)規(guī)律可得出SpaceDRC對(duì)數(shù)據(jù)訪問(wèn)沖突問(wèn)題的檢出率為84%。

因此，RaceBench能夠有效評(píng)估數(shù)據(jù)訪問(wèn)沖突檢測(cè)工具的檢出率、可伸縮性等各項(xiàng)指標(biāo)，并為SpaceDRC的進(jìn)一步改進(jìn)提供了方向。

4 結(jié)束語(yǔ)

本文對(duì)航天嵌入式軟件真實(shí)數(shù)據(jù)訪問(wèn)沖突案例進(jìn)行了系統(tǒng)分析，提出了影響數(shù)據(jù)訪問(wèn)沖突檢測(cè)的6類(lèi)要素，為中斷數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集以及檢測(cè)方法的研究提供了基礎(chǔ)。基于這些要素，設(shè)計(jì)開(kāi)發(fā)了已知首個(gè)中斷數(shù)據(jù)訪問(wèn)沖突問(wèn)題基準(zhǔn)測(cè)試集RaceBench。RaceBench來(lái)源于真實(shí)案例，體現(xiàn)了中斷數(shù)據(jù)訪問(wèn)沖突各個(gè)方面的要素，滿(mǎn)足了一個(gè)基準(zhǔn)測(cè)試集的代表性、多樣性、公平性和適應(yīng)性特征。試驗(yàn)表明，RaceBench能夠有效評(píng)估相應(yīng)工具的技術(shù)指標(biāo)。本文構(gòu)建的基準(zhǔn)測(cè)試集對(duì)工具選型具有現(xiàn)實(shí)意義，也為中斷數(shù)據(jù)競(jìng)爭(zhēng)研究提供指導(dǎo)。一個(gè)完善的缺陷基準(zhǔn)測(cè)試集構(gòu)建是一個(gè)長(zhǎng)期的過(guò)程，未來(lái)RaceBench將繼續(xù)擴(kuò)展新的缺陷特征和場(chǎng)景，提供更完備的評(píng)估能力。

References)

[1] LEVESON N G，TURNER C. An investigation of the Therac-25 accidents[J]. IEEE Computer，1993，16(7)：18-41.

[2] US-Canada Power System Outage Task Force. Final report on the August 14，2003 blackout in the United States and Canada：Causes and Recommendations[EB/OL]. 2004-04-01. http：∥energy.gov/sites/prod/files/oeprod/DocumentsandMedia/BlackoutFinal-Web.pdf.

[3] 楊孟飛，顧斌，郭向英，等. 航天嵌入式軟件可信性保障技術(shù)及應(yīng)用研究[J]. 中國(guó)科學(xué)：技術(shù)科學(xué)，2015，45(2)：198-203.

YANG M F，GU B，GUO X Y，et al. Aerospace embedded software dependability guarantee technology and application[J]. Scientia Scinica Technologica，2015，45(2)：198-203(in Chinese).

[4] 段永顥，陳睿. 基于啟發(fā)式的靜態(tài)中斷數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)方法[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(in Chinese).

[5] CHEN R，GUO X Y，DUAN Y H，et al. Static data race detection for interrupt-driven embedded software[C]∥ Proceedings of International Conference on Secure Integration and Reliability Improvement 2011，Jesu Island，South Korea，June 27-29，2011.Washington,D.C.:IEEE Reliability Society，2011.

[6] 陳睿，楊孟飛，郭向英. 基于變量訪問(wèn)序模式的中斷數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)方法[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(in Chinese).

[7] REGEHR J，COOPRIDER N. Interrupt verification via thread verification[J]. Electron. Notes Theoretical Computer Science，2007，174(9)：139-150.

[8] 周筱羽，顧斌，趙建華，等.中斷驅(qū)動(dòng)系統(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(in Chinese).

[9] WU X G，WEN Y J，CHEN L Q，et al. Data race detection for interrupt-driven programs via bounded model checking[C]∥ Proc.Of IEEE 7th International Conference on Software Security and Reliability-Companion(SERE-C)，Washington，D.C.，USA，18-20 June,2013.

[10] 霍瑋，于洪濤，馮曉兵，等. 靜態(tài)檢測(cè)中斷驅(qū)動(dòng)程序的數(shù)據(jù)競(jìng)爭(zhēng)[J].計(jì)算機(jī)研究與發(fā)展，2011，48(12)：2290-2299.

HUO W，YU H T，F(xiàn)ENG X B，et al. Static data race detection of interrupt-driven programs[J].Journal of Computer Research and Development，2011，48(12)：2290-2299(in Chinese).

[11] 陳園軍，石浚菁，王林章，等.中斷驅(qū)動(dòng)的嵌入式系統(tǒng)數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)工具[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(in Chinese).

[12] WU X G，CHEN L Q，MINE A，et al. Static analysis of run-time errors in interrupt-driven programs via sequentialization[J]. ACM Transactions on Embedded Computing Systems(TECS)，2016，15(4)：1-26.

[13] 于廣良，楊孟飛，徐建，等. 面向多級(jí)中斷系統(tǒng)的任務(wù)最差響應(yīng)時(shí)間分析[J]. 中國(guó)空間科學(xué)技術(shù)，2016，36(2)：28-36.

YU G L，YANG M F，XU J，et al. Worst case response time analysis of multi-level interrupt systems[J]. Chinese Space Science and Technology，2016，36(2)：28-35(in Chinese).

[14] Standard Performance Evaluation Corporation. SPEC benchmarks[EB/OL].2017-03-28.URL：http：∥www.spec.org.

[15] Transaction Processing Council. TPC benchmarks[EB/OL].2016-10-26. URL：http：∥www.tpc.org/.

[16] CIFUENTES C，HOERMANN C，KEYNES N，et al. BegBunch：benchmarking for C bug detection tools[C]. The 2nd International Workshop on Defects in Large Software Systems，Chicago，USA，July 19，2009.

[17] LU S，LI Z，QIN F，TAN L，et al. BugBench：a benchmark for evaluating bug detection tools[C]∥Proc. of Workshop on the Evaluation of Software Defect Detection Tools，June，2005.

[18] NIST. National Institute of Standards and Technology SAMATE Reference Dataset (SRD) project[EB/OL].2016-01-01. http：∥samate.nist.gov/SRD，January，2006.

(編輯：車(chē)曉玲)

Study on aerospace embedded software data race benchmark

CHEN Rui1，2，YANG Mengfei3，*

1.BeijingInstituteofControlEngineering，Beijing100190，China2.BeijingSunwiseInformationTechnologyCo.Ltd.，Beijing100190，China3.ChinaAcademyofSpaceTechnology，Beijing100094，China

No good benchmark suite was made to evaluate the detection methods or tools for the advent of interrupt data race. Based on the real aerospace embedded software data race bugs，six essential factors related to data race detection were proposed，and the data race benchmark suite named RaceBench for aerospace embedded software was designed. The RaceBench，which is close to real programs and is extensible，covers all six factors. The RaceBench was used to evaluate a data race detection tool named SpaceDRC. The result shows that RaceBench can evaluate the capabilities of the tool effectively.

data access conflict；benchmark；aerospace embedded software；data race；software testing

10.16708/j.cnki.1000-758X.2017.0052

2017-04-10；

2017-04-20；錄用日期：2017-05-18；網(wǎng)絡(luò)出版時(shí)間：2017-05-31 09:44:37

http:∥kns.cnki.net/kcms/detail/11.1859.V.20170531.0944.004.html

國(guó)家自然科學(xué)基金(91118007，61632005)

陳睿(1984-)，男，博士研究生，高級(jí)工程師，chenrui@sunwiseinfo.com，研究方向?yàn)榍度胧杰浖y(cè)試

*通訊作者：楊孟飛(1962-)，男，研究員，yangmf@bice.org.cn，研究方向?yàn)榭臻g飛行器系統(tǒng)設(shè)計(jì)、控制計(jì)算機(jī)系統(tǒng)及嵌入式軟件

陳睿，楊孟飛. 航天嵌入式軟件數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集研究[J].中國(guó)空間科學(xué)技術(shù)，2017，37(3)：62-70.

CHENR,YANGMF.Studyonaerospaceembeddedsoftwaredataracebenchmark[J].ChineseSpaceScienceandTechnology，2017，37(3)：62-70(inChinese).

TP311

A

http:∥zgkj.cast.cn