作者：BENJAMIN BROSGOL，DR. DUDREY SMITH，DR. PATRICK ROGERS

需要占用空間小或必須符合行業(yè)保證標(biāo)準(zhǔn)（如 DO-178B或 DO-178C）的機(jī)載系統(tǒng)對(duì)運(yùn)行時(shí)支持庫(kù)中的尺寸和復(fù)雜性成本很敏感。為了滿足這些需求，未來(lái)機(jī)載能力環(huán)境（FACE？技術(shù)標(biāo)準(zhǔn)已將 Ada 編程語(yǔ)言任務(wù)功能的 Ravenscar 子集指定為必須滿足安全和/或安全保證要求的軟件組件的可接受并發(fā)方法之一。

FACE方法是一種政府-行業(yè)軟件標(biāo)準(zhǔn)和商業(yè)戰(zhàn)略，旨在獲得價(jià)格合理的軟件系統(tǒng)，在全球國(guó)防項(xiàng)目中快速集成便攜式功能，并吸引創(chuàng)新并快速且經(jīng)濟(jì)地部署。它通過(guò)通用參考體系結(jié)構(gòu)上下文中定義良好的標(biāo)準(zhǔn)接口促進(jìn)組件可移植性和重用性。參考體系結(jié)構(gòu)包括一個(gè)操作系統(tǒng)段 （OSS），它提供應(yīng)用程序可能需要的運(yùn)行時(shí)服務(wù)。OSS 對(duì) FACE 組件的支持的通用性取決于組件的配置文件，該配置文件是基于性能、安全和/或安全性要求的完整 FACE 功能的子集。FACE技術(shù)標(biāo)準(zhǔn)定義了幾個(gè)配置文件：

通用（根據(jù)需要保證，不保證確定性，可選時(shí)間分區(qū)，需要空間分區(qū)）

安全性（安全/安保保證、確定性和時(shí)間/空間劃分）

安全（安全保證、確定性和時(shí)間/空間劃分）——基礎(chǔ)和擴(kuò)展

與這些配置文件對(duì)應(yīng)的是 C、C++、Ada 和 Java 的語(yǔ)言子集（“功能集”）。功能集定義了允許哪些功能，禁止哪些功能：允許確保足夠的表現(xiàn)力，禁止有助于根據(jù)相關(guān)保證要求簡(jiǎn)化分析/認(rèn)證。運(yùn)行時(shí)支持庫(kù)必須實(shí)現(xiàn)允許的功能，并且可能提供更多功能，但（對(duì)于安全功能集）以確保確定性并促進(jìn)保證分析的方式。

FACE技術(shù)標(biāo)準(zhǔn)為Ada定義了幾個(gè)功能集：

Ada 95 安全 – Ada 95 安全基礎(chǔ)和安保以及 Ada 95 安全擴(kuò)展

Ada 95 通用型

Ada 2012 通用

這些配置文件以兩種方式支持并發(fā)：通過(guò)操作系統(tǒng)環(huán)境（POSIX 或 ARINC 653）中的線程 API，或通過(guò)語(yǔ)言構(gòu)造（任務(wù)）。

使用語(yǔ)言中定義的并發(fā)功能具有源代碼可移植性的優(yōu)勢(shì)，因?yàn)槊總€(gè) Ada 實(shí)現(xiàn)都需要支持 Ada 任務(wù)模型。Ada任務(wù)的高級(jí)性質(zhì)也傾向于提高可靠性，因?yàn)?a target="_blank">程序員可以直接表達(dá)典型的通信范式，而不是通過(guò)信號(hào)量或條件變量等較低級(jí)別的結(jié)構(gòu)。

允許的任務(wù)功能在通用和安全功能集之間有所不同。對(duì)于通用集，幾乎允許使用完整的 Ada 任務(wù)功能。但是，在需要安全或安全保證的情況下，運(yùn)行時(shí)支持的復(fù)雜性將是有問(wèn)題的，并且由于實(shí)現(xiàn)依賴性，完整模型還引入了應(yīng)用程序非確定性。

需要任務(wù)功能的確定性子集。該子集需要具有足夠的表現(xiàn)力，以便對(duì)現(xiàn)實(shí)世界的航空電子應(yīng)用程序進(jìn)行編程，并且還需要足夠簡(jiǎn)單以高效實(shí)施。它應(yīng)該有助于靜態(tài)分析，以驗(yàn)證關(guān)鍵屬性，包括硬實(shí)時(shí)系統(tǒng)的可調(diào)度性（確保滿足所有截止日期），并支持根據(jù)保證標(biāo)準(zhǔn)進(jìn)行認(rèn)證。Ravenscar任務(wù)子集是專門(mén)為滿足這些目標(biāo)而設(shè)計(jì)的，并且由FACE安全功能集允許;它是 Ada 95 任務(wù)功能的一個(gè)子集，是 Ada 2005 語(yǔ)言標(biāo)準(zhǔn)的一部分。

艾達(dá)任務(wù)和烏鴉限制

并發(fā) Ada 程序由一組任務(wù)（控制線程）組成，這些任務(wù)通過(guò)稱為會(huì)合的任務(wù)間通信設(shè)施直接相互通信，或通過(guò)共享數(shù)據(jù)間接通信。對(duì)于后一個(gè)目的，該語(yǔ)言提供了一種稱為受保護(hù)對(duì)象的高級(jí)機(jī)制，用于基于狀態(tài)/條件的互斥，同時(shí)避免競(jìng)爭(zhēng)條件和死鎖。其他形式的安全數(shù)據(jù)共享也由語(yǔ)言定義，例如依賴于硬件強(qiáng)制的訪問(wèn)原子性。

Ada 任務(wù)模型包括用于終止任務(wù)的功能（例如，中止語(yǔ)句）、與時(shí)間相關(guān)的支持（例如相對(duì)和絕對(duì)延遲）和具有實(shí)時(shí)時(shí)鐘操作的包，以及基于事件或超時(shí)的異步機(jī)制。為了防止數(shù)據(jù)損壞，某些代碼節(jié)被定義為中止延遲，并且需要在異步終止之前執(zhí)行到完成。

任務(wù)和受保護(hù)對(duì)象可以全局定義，也可以在本地范圍內(nèi)定義;語(yǔ)義防止懸而未決的引用（例如，子程序在其所有本地任務(wù)終止之前不允許返回）。

任務(wù)可以在多個(gè)處理器/內(nèi)核上以實(shí)際并行方式執(zhí)行，也可以在單個(gè)處理器/內(nèi)核上的調(diào)度程序控制下多路復(fù)用。可以為任務(wù)分配優(yōu)先級(jí)，無(wú)論是靜態(tài)的還是動(dòng)態(tài)的，并且根據(jù)任務(wù)調(diào)度策略，當(dāng)多個(gè)任務(wù)有資格執(zhí)行時(shí)，在程序執(zhí)行期間的不同時(shí)間點(diǎn)考慮優(yōu)先級(jí)。

圖 1 顯示了一個(gè) Ada 任務(wù)程序的簡(jiǎn)單示例，該程序具有兩個(gè)任務(wù)（讀取器和寫(xiě)入器），通過(guò)受保護(hù)的數(shù)據(jù)對(duì)象（資源）進(jìn)行互斥通信。

圖1：Ada任務(wù)程序的示例，其中讀取器和編寫(xiě)器通過(guò)資源進(jìn)行通信。

完整的任務(wù)模型具有很強(qiáng)的表現(xiàn)力，但需要復(fù)雜的運(yùn)行時(shí)實(shí)現(xiàn)。為了支持Ada中的高效，高完整性的并發(fā)應(yīng)用程序，特別是那些具有硬實(shí)時(shí)要求的應(yīng)用程序，1997年和1999年在英國(guó)Ravenscar舉行的研討會(huì)指定了一組限制，允許任務(wù)程序在其功能和時(shí)間屬性方面進(jìn)行靜態(tài)分析。這個(gè)子集被稱為Ravenscar Profile;為了避免與“輪廓”的FACE概念混淆，這里將其稱為Ravenscar子集。

遵循 Ravenscar 子集限制的程序具有以下幾個(gè)屬性：它包含固定數(shù)量的非終止任務(wù)，所有任務(wù)都是全局定義的;每個(gè)任務(wù)都有一個(gè)觸發(fā)事件，要么基于時(shí)間，要么基于事件（從另一個(gè)任務(wù)或環(huán)境發(fā)出信號(hào)），觸發(fā)事件的發(fā)生次數(shù)可能不受限制;唯一的任務(wù)交互是通過(guò)共享/受保護(hù)的數(shù)據(jù)對(duì)象。

這些限制是通過(guò)標(biāo)準(zhǔn) Ada 語(yǔ)言功能定義的，特別是實(shí)現(xiàn)強(qiáng)制執(zhí)行的一系列編譯指示。兩個(gè)這樣的編譯指示任務(wù)調(diào)度和對(duì)象鎖定策略：

雜注Task_Dispatching_Policy （FIFO_Within_Priorities）

雜注Locking_Policy （Ceiling_Locking）

這些策略有助于調(diào)度性分析方法，如速率單調(diào)分析 ［5］，并有助于最小化優(yōu)先級(jí)倒置，防止基于互斥的死鎖，并保證任務(wù)始終滿足其截止日期（有關(guān)進(jìn)一步說(shuō)明，請(qǐng)參閱側(cè)欄）。

Ravenscar的其他限制是對(duì)特定語(yǔ)言功能的限制。其中包括禁止相對(duì)延遲語(yǔ)句（因?yàn)樗鼈儾皇潜匦璧模膊荒芸煽康赜糜趯?shí)現(xiàn)周期性）、中止語(yǔ)句、本地定義的任務(wù)或受保護(hù)的對(duì)象、任務(wù)集合、動(dòng)態(tài)優(yōu)先級(jí)、任務(wù)分配和異步控制轉(zhuǎn)移。簡(jiǎn)化實(shí)現(xiàn)或促進(jìn)可調(diào)度性分析的其他限制包括每個(gè)受保護(hù)對(duì)象最多一個(gè)隊(duì)列（條目）的限制，在任何給定時(shí)間最多有一個(gè)調(diào)用方掛起，以及禁止任務(wù)終止。Ravenscar子集的完整定義出現(xiàn)在Ada 2012標(biāo)準(zhǔn)［6］中。

雖然具有限制性，但 Ravenscar 子集也足夠通用，可以表達(dá)一系列有用的任務(wù)習(xí)語(yǔ)，例如循環(huán)（周期性）任務(wù);事件驅(qū)動(dòng)（非定期或零星）任務(wù)、中斷處理程序和共享資源（簡(jiǎn)單的受保護(hù)對(duì)象）。

圖 2 顯示了圖 1 中讀取器/寫(xiě)入器示例變體中的 Ravenscar 子集，其中包含避免漂移的循環(huán)（周期性）任務(wù)。

圖2：圖 1 中示例變體中的 Ravenscar 子集。

在 FACE 上下文中實(shí)現(xiàn) Ravenscar 任務(wù)子集

除了允許 Ravenscar 子集外，Ada 95 安全功能集還允許或禁止各種順序語(yǔ)言功能。例如，安全基礎(chǔ)功能集允許中斷支持、具有單個(gè)默認(rèn)處理程序的預(yù)定義異常以及來(lái)自 Ada 預(yù)定義環(huán)境的某些包，同時(shí)禁止動(dòng)態(tài)分配。Ada 95安全擴(kuò)展功能集通常允許異常處理，并允許在啟動(dòng)時(shí)動(dòng)態(tài)分配，同時(shí)禁止釋放。

為任一安全功能集實(shí)現(xiàn)運(yùn)行時(shí)支持庫(kù)的挑戰(zhàn)在于，如何以有助于分析相關(guān)保證要求的方式提供允許的功能。滿足這一挑戰(zhàn)的實(shí)現(xiàn)的一個(gè)示例是AdaCore的Ravenscar-Cert庫(kù)，它支持安全基礎(chǔ)和安全擴(kuò)展功能集中允許的所有功能，并滿足DO-178B或DO-178C中的適用目標(biāo)。該庫(kù)實(shí)現(xiàn)了 Ravenscar 任務(wù)功能、異常傳播、最后機(jī)會(huì)處理程序和返回不受約束數(shù)組的函數(shù)的標(biāo)記/發(fā)布機(jī)制（不需要堆管理）。Ravenscar-Cert庫(kù)已經(jīng)為Wind River的VxWorks 653和Lynx Software Technologies的LynxOS-178 RTOSes實(shí)現(xiàn)。此庫(kù)中的 Ravenscar 任務(wù)支持小于 40 KB。

迎接挑戰(zhàn)

并發(fā)編程對(duì)于設(shè)計(jì)和實(shí)現(xiàn)實(shí)時(shí)嵌入式應(yīng)用程序，特別是FACE組件非常有用，但它帶來(lái)了重大的軟件工程挑戰(zhàn)：

?可移植性。Ravenscar 子集由 Ada 語(yǔ)言標(biāo)準(zhǔn)定義，其限制集可以幫助保證確定性行為。遵循Ravenscar子集的程序（以及對(duì)實(shí)現(xiàn)相關(guān)功能的其他限制）將跨不同的實(shí)現(xiàn)和平臺(tái)移植，這是FACE方法的主要目標(biāo)。Ada的Ravenscar任務(wù)子集可以幫助應(yīng)對(duì)這些挑戰(zhàn)。

?可靠性。對(duì)于實(shí)時(shí)程序，可靠性不僅意味著功能正確性（計(jì)算正確的結(jié)果），還意味著時(shí)間可預(yù)測(cè)性（滿足嚴(yán)格的截止日期）。Ravenscar 子集有助于以多種方式實(shí)現(xiàn)這些要求。禁止異步等復(fù)雜功能，允許的任務(wù)間通信的簡(jiǎn)單形式適用于靜態(tài)分析，隊(duì)列限制有助于計(jì)算最壞情況執(zhí)行時(shí)間。Ravenscar 限制指定的任務(wù)調(diào)度和對(duì)象鎖定策略同樣有助于調(diào)度分析，并產(chǎn)生比傳統(tǒng)循環(huán)執(zhí)行更簡(jiǎn)單、更易于維護(hù)的體系結(jié)構(gòu)。

?效率。由于沒(méi)有語(yǔ)義復(fù)雜性，因此可以實(shí)現(xiàn)“精益和平均”的運(yùn)行時(shí)實(shí)現(xiàn)。不需要支持任務(wù)終止、隊(duì)列管理和動(dòng)態(tài)優(yōu)先級(jí)等功能，并且正如 AdaCore 的 Ravenscar-Cert 庫(kù)等實(shí)現(xiàn)所證明的那樣，所需的功能可以有效地映射到底層實(shí)時(shí)操作系統(tǒng)提供的服務(wù)。

審核編輯：郭婷