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

最大化性能對于軍事嵌入式系統(tǒng)尤為重要，因為在日益數(shù)字化的戰(zhàn)場上，人們越來越需要保持低成本，同時滿足連接要求。隨著制造商達(dá)到小型化和集成度提高所能達(dá)到的極限，提高性能的最佳方法是使用多核處理器。

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

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

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

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

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

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

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

圖1：訪問共享變量的兩個線程中的代碼

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

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

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

消除并發(fā)缺陷

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

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

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

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

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

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

多核權(quán)衡

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

審核編輯：郭婷