多核處理器在安全關(guān)鍵型應(yīng)用中越來(lái)越受歡迎，因?yàn)樗鼈兲峁┝孙@著的價(jià)格和性能改進(jìn)。但是，為多核硬件編寫(xiě)多線程應(yīng)用程序是出了名的困難，并可能導(dǎo)致災(zāi)難性故障。下面描述了用于識(shí)別問(wèn)題（包括數(shù)據(jù)爭(zhēng)用）的符號(hào)執(zhí)行技術(shù)？最常見(jiàn)的并發(fā)缺陷之一？以及靜態(tài)分析如何幫助開(kāi)發(fā)人員找到并消除它們。

最大化性能對(duì)于軍事嵌入式系統(tǒng)尤為重要，因?yàn)樵谌找鏀?shù)字化的戰(zhàn)場(chǎng)上，人們?cè)絹?lái)越需要保持低成本，同時(shí)滿(mǎn)足連接要求。隨著制造商達(dá)到小型化和集成度提高所能達(dá)到的極限，提高性能的最佳方法是使用多核處理器。

缺點(diǎn)是，為了充分利用并行執(zhí)行的許多內(nèi)核，必須將軟件編寫(xiě)為本質(zhì)上是多線程的。為單核處理器編寫(xiě)為單線程的軟件在多核處理器上執(zhí)行時(shí)將實(shí)現(xiàn)很少或沒(méi)有性能優(yōu)勢(shì)：必須重寫(xiě)或調(diào)整它以使用多線程。關(guān)鍵挑戰(zhàn)是盡可能保持核心繁忙，同時(shí)確保它們正確協(xié)調(diào)對(duì)共享資源的訪問(wèn)。不幸的是，編寫(xiě)這樣的代碼比編寫(xiě)單線程代碼要困難得多。當(dāng)存在死鎖或爭(zhēng)用條件等缺陷時(shí)，它們可能會(huì)以難以診斷的方式表現(xiàn)出來(lái)。查找和消除并發(fā) bug 的傳統(tǒng)技術(shù)可能無(wú)效。

并發(fā)錯(cuò)誤如此困難的核心原因之一是，當(dāng)線程執(zhí)行時(shí)，線程中的事件可以通過(guò)多種方式交錯(cuò)。隨著線程或指令數(shù)量的增加，交錯(cuò)的數(shù)量呈指數(shù)級(jí)增長(zhǎng)。如果線程 A 執(zhí)行 M 條指令，線程 B 執(zhí)行 N 條指令，則兩個(gè)線程可能存在 N+MCN 交錯(cuò)。例如，給定兩個(gè)平凡的線程，每個(gè)線程有 10 條指令，這些指令有 184，756 個(gè)可能的交錯(cuò)。即使使用非常小的程序，很明顯也幾乎不可能測(cè)試所有可能的組合。其次，即使可以識(shí)別導(dǎo)致故障的單個(gè)交錯(cuò)，也很難設(shè)置使用該特定交錯(cuò)的可重復(fù)測(cè)試用例，因?yàn)榫€程調(diào)度實(shí)際上是不確定的。因此，調(diào)試并發(fā)程序可能非常昂貴且耗時(shí)。爭(zhēng)用條件是一類(lèi)并發(fā)缺陷，很容易意外引入，并且很難通過(guò)常規(guī)測(cè)試消除。但是，程序員可以使用一些技術(shù)來(lái)查找和刪除它們。

潛在的災(zāi)難性故障

與單線程代碼相比，并發(fā)程序中可能會(huì)出現(xiàn)全新的缺陷類(lèi)別，包括死鎖、饑餓和爭(zhēng)用條件。這些缺陷主要會(huì)導(dǎo)致開(kāi)發(fā)過(guò)程中難以診斷和消除的神秘故障。我們合作過(guò)的一家航空電子制造商花了兩個(gè)人年的時(shí)間應(yīng)用傳統(tǒng)的調(diào)試技術(shù)，努力找到間歇性軟件故障的根本原因，結(jié)果證明這是一種競(jìng)爭(zhēng)條件。有時(shí)后果可能很可怕——有史以來(lái)最臭名昭著的兩個(gè)軟件故障是由競(jìng)爭(zhēng)條件引起的。Therac-25放射治療機(jī)具有導(dǎo)致幾名患者死亡的種族條件。同樣，2003 年?yáng)|北停電因競(jìng)爭(zhēng)條件而加劇，導(dǎo)致誤導(dǎo)性信息被傳達(dá)給技術(shù)人員。

有幾種不同類(lèi)型的競(jìng)爭(zhēng)條件。最常見(jiàn)和最隱蔽的形式之一 - 數(shù)據(jù)競(jìng)爭(zhēng) - 是涉及訪問(wèn)內(nèi)存位置的競(jìng)爭(zhēng)條件類(lèi)。

當(dāng)有兩個(gè)或多個(gè)執(zhí)行線程訪問(wèn)共享內(nèi)存位置，至少一個(gè)線程正在更改該位置的數(shù)據(jù)，并且沒(méi)有用于協(xié)調(diào)訪問(wèn)的顯式機(jī)制時(shí)，就會(huì)發(fā)生數(shù)據(jù)爭(zhēng)用。如果發(fā)生數(shù)據(jù)爭(zhēng)用，則可能會(huì)使程序處于不一致?tīng)顟B(tài)。

考慮控制襟翼位置的航空電子代碼。在正常情況下，襟翼處于飛行控制軟件指示的位置，但飛行員可以通過(guò)按下控制面板上的按鈕來(lái)覆蓋該位置，在這種情況下，使用手動(dòng)設(shè)置的位置。為了簡(jiǎn)單起見(jiàn)，假設(shè)程序中有兩個(gè)線程：一個(gè)控制翻蓋，另一個(gè)監(jiān)視控制面板上元素的位置。還有一個(gè)名為 is_manual 的共享布爾變量，它對(duì)手動(dòng)覆蓋是否設(shè)置進(jìn)行編碼。擺動(dòng)位置螺紋檢查is_manual的值，如果為 true，則相應(yīng)地設(shè)置位置。控制面板線程偵聽(tīng)按鈕按下事件，如果按下替代按鈕，它將is_manual設(shè)置為 true。圖 1 顯示了為實(shí)現(xiàn)此規(guī)范而可能編寫(xiě)的代碼。此代碼可能在大多數(shù)情況下都有效;但是，由于 is_manual 變量對(duì)兩個(gè)線程共享的狀態(tài)進(jìn)行編碼，因此它容易受到數(shù)據(jù)爭(zhēng)用的影響，因?yàn)閷?duì)它的訪問(wèn)不受鎖保護(hù)。如果在飛行員按下超控按鈕的確切時(shí)間執(zhí)行襟翼定位代碼，則程序可能會(huì)進(jìn)入不一致的狀態(tài)，并且將使用錯(cuò)誤的襟翼位置。圖 2 顯示了這種情況是如何發(fā)生的。

圖1：訪問(wèn)共享變量的兩個(gè)線程中的代碼

圖2：導(dǎo)致數(shù)據(jù)爭(zhēng)用的指令交錯(cuò)

這個(gè)例子巧妙地說(shuō)明了數(shù)據(jù)爭(zhēng)用的一個(gè)屬性，這使得它們難以診斷：損壞的癥狀可能只有在數(shù)據(jù)爭(zhēng)用發(fā)生很久之后才能觀察到。在這種情況下，只有當(dāng)飛行員注意到飛機(jī)沒(méi)有按預(yù)期響應(yīng)時(shí)，才會(huì)注意到使用錯(cuò)誤的襟翼位置的事實(shí)。

人們普遍認(rèn)為，數(shù)據(jù)競(jìng)爭(zhēng)的某些實(shí)例是良性的，可以容忍。然而，現(xiàn)在毫無(wú)疑問(wèn)，這很少是真的。C 標(biāo)準(zhǔn)［4］ 明確指出，編譯器可以假設(shè)沒(méi)有數(shù)據(jù)爭(zhēng)用，因此優(yōu)化器可以并且確實(shí)進(jìn)行了對(duì)提高單線程代碼性能有效的轉(zhuǎn)換，但在存在明顯良性的競(jìng)爭(zhēng)條件時(shí)引入了錯(cuò)誤。這些都是微妙的影響——即使是經(jīng)驗(yàn)豐富的程序員也經(jīng)常對(duì)它們感到驚訝。（有關(guān)完整的解釋和幾個(gè)令人信服的示例，請(qǐng)參閱參考文獻(xiàn) ［1］。因此，為了實(shí)現(xiàn)高水平的保證并避免災(zāi)難性故障，查找并刪除所有數(shù)據(jù)爭(zhēng)用非常重要。

消除并發(fā)缺陷

鑒于并發(fā)缺陷，尤其是數(shù)據(jù)爭(zhēng)用，風(fēng)險(xiǎn)很大，因此使用多種技術(shù)來(lái)消除它們非常重要。由于不確定性，傳統(tǒng)的動(dòng)態(tài)測(cè)試不太適合發(fā)現(xiàn)許多并發(fā)缺陷。通過(guò)測(cè)試數(shù)百次的程序以后可能會(huì)在具有完全相同輸入的相同環(huán)境中失敗，因?yàn)樵撳e(cuò)誤可能對(duì)時(shí)間非常敏感。尋求高保證的工程師如果要消除并發(fā)缺陷，就必須轉(zhuǎn)向其他技術(shù)。

靜態(tài)分析工具提供了一種查找此類(lèi)錯(cuò)誤的方法。測(cè)試和靜態(tài)分析之間的主要區(qū)別在于，它針對(duì)給定的一組輸入測(cè)試程序的特定執(zhí)行，而靜態(tài)分析查找適用于所有可能執(zhí)行和所有輸入的屬性。（在實(shí)踐中，靜態(tài)分析工具進(jìn)行近似以獲得可接受的性能和精度，因此達(dá)不到這個(gè)理想模型。盡管如此，它們確實(shí)涵蓋了比傳統(tǒng)測(cè)試更多的情況。

粗略地說(shuō)，靜態(tài)分析工具的工作原理是創(chuàng)建程序模型并對(duì)該模型進(jìn)行符號(hào)執(zhí)行，在此過(guò)程中查找錯(cuò)誤條件。例如，GrammaTech的CodeSonar靜態(tài)分析工具通過(guò)創(chuàng)建哪些鎖由哪些線程持有的映射，并通過(guò)推理可能導(dǎo)致對(duì)共享變量的不同步訪問(wèn)的可能交錯(cuò)來(lái)查找數(shù)據(jù)競(jìng)爭(zhēng)。使用類(lèi)似的技術(shù)發(fā)現(xiàn)死鎖和其他并發(fā)缺陷（包括鎖管理不善）。

自定義并發(fā)構(gòu)造：案例研究

當(dāng)程序使用標(biāo)準(zhǔn)方法來(lái)管理并發(fā)時(shí)，標(biāo)準(zhǔn)缺陷檢測(cè)技術(shù)最有用。大多數(shù)工具識(shí)別并推理標(biāo)準(zhǔn)庫(kù)（如POSIX線程庫(kù)）或?qū)Ｓ?a target="_blank">接口（如VxWorks）的特殊屬性。但是，許多系統(tǒng)使用自定義技術(shù)來(lái)管理并發(fā)性。

例如，與我們合作的另一家制造商在使用自定義搶占式多線程軟件接口的平臺(tái)上構(gòu)建了一個(gè)安全關(guān)鍵型設(shè)備。在此設(shè)計(jì)中，一個(gè)關(guān)鍵約束是，必須使用適當(dāng)?shù)谋Ｗo(hù)構(gòu)造保護(hù)可以從多個(gè)優(yōu)先級(jí)線程訪問(wèn)的所有數(shù)據(jù)實(shí)例。在使用靜態(tài)分析之前，驗(yàn)證是否遵守此約束需要花費(fèi)人工月的手動(dòng)分析時(shí)間。為了降低成本，他們通過(guò)轉(zhuǎn)向靜態(tài)分析來(lái)尋求解決方案。現(xiàn)代高級(jí)靜態(tài)分析工具的一個(gè)重要特性是它們是可擴(kuò)展的：它們提供了一個(gè)帶有抽象的 API，可以方便地實(shí)現(xiàn)自定義靜態(tài)分析算法。使用 CodeSonar 的 API，他們能夠編寫(xiě)一個(gè)解決方案，該解決方案利用現(xiàn)有分析核心使用的算法來(lái)查找代碼中違反設(shè)計(jì)約束的位置。生成的工具作為插件實(shí)現(xiàn)，能夠自動(dòng)查找違反關(guān)鍵約束的情況，所有這些都只需一小部分成本和比以前少得多的時(shí)間。

多核權(quán)衡

轉(zhuǎn)向多核處理器設(shè)計(jì)有令人信服的理由，但風(fēng)險(xiǎn)在于這樣做可能會(huì)在軟件中引入并發(fā)缺陷。這些很容易引入 - 即使是看似無(wú)辜的代碼也可能隱藏令人討厭的多線程錯(cuò)誤 - 并且眾所周知，當(dāng)它們發(fā)生時(shí)很難診斷和消除。僅靠傳統(tǒng)的測(cè)試技術(shù)不足以確保高質(zhì)量的軟件，這主要是因?yàn)楦叨鹊姆谴_定性。使用使用符號(hào)執(zhí)行的高級(jí)靜態(tài)分析工具是一種可以提供幫助的方法，因?yàn)榇祟?lèi)工具可以推理代碼執(zhí)行的所有可能方式。這些工具可以在使用標(biāo)準(zhǔn)多線程庫(kù)的代碼中發(fā)現(xiàn)數(shù)據(jù)爭(zhēng)用和死鎖等缺陷，甚至可以適應(yīng)使用非標(biāo)準(zhǔn)并發(fā)構(gòu)造的設(shè)計(jì)。

審核編輯：郭婷