Ravenscar Ada任務和FACE安全配置文件

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

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

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

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

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

安全（安全保證、確定性和時間/空間劃分）——基礎和擴展

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

FACE技術標準為Ada定義了幾個功能集：

Ada 95 安全 – Ada 95 安全基礎和安保以及 Ada 95 安全擴展

Ada 95 通用型

Ada 2012 通用

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

使用語言中定義的并發(fā)功能具有源代碼可移植性的優(yōu)勢，因為每個 Ada 實現(xiàn)都需要支持 Ada 任務模型。Ada任務的高級性質(zhì)也傾向于提高可靠性，因為程序員可以直接表達典型的通信范式，而不是通過信號量或條件變量等較低級別的結(jié)構(gòu)。

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

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

艾達任務和烏鴉限制

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

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

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

任務可以在多個處理器/內(nèi)核上以實際并行方式執(zhí)行，也可以在單個處理器/內(nèi)核上的調(diào)度程序控制下多路復用?？梢詾槿蝿辗峙鋬?yōu)先級，無論是靜態(tài)的還是動態(tài)的，并且根據(jù)任務調(diào)度策略，當多個任務有資格執(zhí)行時，在程序執(zhí)行期間的不同時間點考慮優(yōu)先級。

圖 1 顯示了一個 Ada 任務程序的簡單示例，該程序具有兩個任務（讀取器和寫入器），通過受保護的數(shù)據(jù)對象（資源）進行互斥通信。

圖1：Ada任務程序的示例，其中讀取器和編寫器通過資源進行通信。

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

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

這些限制是通過標準 Ada 語言功能定義的，特別是實現(xiàn)強制執(zhí)行的一系列編譯指示。兩個這樣的編譯指示任務調(diào)度和對象鎖定策略：

雜注Task_Dispatching_Policy （FIFO_Within_Priorities）

雜注Locking_Policy （Ceiling_Locking）

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

Ravenscar的其他限制是對特定語言功能的限制。其中包括禁止相對延遲語句（因為它們不是必需的，也不能可靠地用于實現(xiàn)周期性）、中止語句、本地定義的任務或受保護的對象、任務集合、動態(tài)優(yōu)先級、任務分配和異步控制轉(zhuǎn)移。簡化實現(xiàn)或促進可調(diào)度性分析的其他限制包括每個受保護對象最多一個隊列（條目）的限制，在任何給定時間最多有一個調(diào)用方掛起，以及禁止任務終止。Ravenscar子集的完整定義出現(xiàn)在Ada 2012標準［6］中。

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

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

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

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

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

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

迎接挑戰(zhàn)

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

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

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

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

審核編輯：郭婷