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

描述

  作者:BENJAMIN BROSGOL,DR. DUDREY SMITH,DR. PATRICK ROGERS

  需要占用空间小或必须符合行业保证标准(如 DO-178B或 DO-178C)的机载系统对运行时支持库中的尺寸和复杂性成本很敏感。为了满足这些需求,未来机载能力环境(FACE?技术标准已将 Ada 编程语言任务功能的 Ravenscar 子集指定为必须满足安全和/或安全保证要求的软件组件的可接受并发方法之一。

  FACE方法是一种政府-行业软件标准和商业战略,旨在获得价格合理的软件系统,在全球国防项目中快速集成便携式功能,并吸引创新并快速且经济地部署。它通过通用参考体系结构上下文中定义良好的标准接口促进组件可移植性和重用性。参考体系结构包括一个操作系统段 (OSS),它提供应用程序可能需要的运行时服务。OSS 对 FACE 组件的支持的通用性取决于组件的配置文件,该配置文件是基于性能、安全和/或安全性要求的完整 FACE 功能的子集。FACE技术标准定义了几个配置文件:

  通用(根据需要保证,不保证确定性,可选时间分区,需要空间分区)

  安全性(安全/安保保证、确定性和时间/空间划分)

  安全(安全保证、确定性和时间/空间划分)——基础和扩展

  与这些配置文件对应的是 C、C++、Ada 和 Java 的语言子集(“功能集”)。功能集定义了允许哪些功能,禁止哪些功能:允许确保足够的表现力,禁止有助于根据相关保证要求简化分析/认证。运行时支持库必须实现允许的功能,并且可能提供更多功能,但(对于安全功能集)以确保确定性并促进保证分析的方式。

  FACE技术标准为Ada定义了几个功能集:

  Ada 95 安全 – Ada 95 安全基础和安保以及 Ada 95 安全扩展

  Ada 95 通用型

  Ada 2012 通用

  这些配置文件以两种方式支持并发:通过操作系统环境(POSIX 或 ARINC 653)中的线程 API,或通过语言构造(任务)。

  使用语言中定义的并发功能具有源代码可移植性的优势,因为每个 Ada 实现都需要支持 Ada 任务模型。Ada任务的高级性质也倾向于提高可靠性,因为程序员可以直接表达典型的通信范式,而不是通过信号量或条件变量等较低级别的结构。

  允许的任务功能在通用和安全功能集之间有所不同。对于通用集,几乎允许使用完整的 Ada 任务功能。但是,在需要安全或安全保证的情况下,运行时支持的复杂性将是有问题的,并且由于实现依赖性,完整模型还引入了应用程序非确定性。

  需要任务功能的确定性子集。该子集需要具有足够的表现力,以便对现实世界的航空电子应用程序进行编程,并且还需要足够简单以高效实施。它应该有助于静态分析,以验证关键属性,包括硬实时系统的可调度性(确保满足所有截止日期),并支持根据保证标准进行认证。Ravenscar任务子集是专门为满足这些目标而设计的,并且由FACE安全功能集允许;它是 Ada 95 任务功能的一个子集,是 Ada 2005 语言标准的一部分。

  艾达任务和乌鸦限制

  并发 Ada 程序由一组任务(控制线程)组成,这些任务通过称为会合的任务间通信设施直接相互通信,或通过共享数据间接通信。对于后一个目的,该语言提供了一种称为受保护对象的高级机制,用于基于状态/条件的互斥,同时避免竞争条件和死锁。其他形式的安全数据共享也由语言定义,例如依赖于硬件强制的访问原子性。

  Ada 任务模型包括用于终止任务的功能(例如,中止语句)、与时间相关的支持(例如相对和绝对延迟)和具有实时时钟操作的包,以及基于事件或超时的异步机制。为了防止数据损坏,某些代码节被定义为中止延迟,并且需要在异步终止之前执行到完成。

  任务和受保护对象可以全局定义,也可以在本地范围内定义;语义防止悬而未决的引用(例如,子程序在其所有本地任务终止之前不允许返回)。

  任务可以在多个处理器/内核上以实际并行方式执行,也可以在单个处理器/内核上的调度程序控制下多路复用。可以为任务分配优先级,无论是静态的还是动态的,并且根据任务调度策略,当多个任务有资格执行时,在程序执行期间的不同时间点考虑优先级。

  图 1 显示了一个 Ada 任务程序的简单示例,该程序具有两个任务(读取器和写入器),通过受保护的数据对象(资源)进行互斥通信。

  图1:Ada任务程序的示例,其中读取器和编写器通过资源进行通信。

  

操作系统

  完整的任务模型具有很强的表现力,但需要复杂的运行时实现。为了支持Ada中的高效,高完整性的并发应用程序,特别是那些具有硬实时要求的应用程序,1997年和1999年在英国Ravenscar举行的研讨会指定了一组限制,允许任务程序在其功能和时间属性方面进行静态分析。这个子集被称为Ravenscar Profile;为了避免与“轮廓”的FACE概念混淆,这里将其称为Ravenscar子集。

  遵循 Ravenscar 子集限制的程序具有以下几个属性:它包含固定数量的非终止任务,所有任务都是全局定义的;每个任务都有一个触发事件,要么基于时间,要么基于事件(从另一个任务或环境发出信号),触发事件的发生次数可能不受限制;唯一的任务交互是通过共享/受保护的数据对象。

  这些限制是通过标准 Ada 语言功能定义的,特别是实现强制执行的一系列编译指示。两个这样的编译指示任务调度和对象锁定策略:

  杂注Task_Dispatching_Policy (FIFO_Within_Priorities)

  杂注Locking_Policy (Ceiling_Locking)

  这些策略有助于调度性分析方法,如速率单调分析 [5],并有助于最小化优先级倒置,防止基于互斥的死锁,并保证任务始终满足其截止日期(有关进一步说明,请参阅侧栏)。

  Ravenscar的其他限制是对特定语言功能的限制。其中包括禁止相对延迟语句(因为它们不是必需的,也不能可靠地用于实现周期性)、中止语句、本地定义的任务或受保护的对象、任务集合、动态优先级、任务分配和异步控制转移。简化实现或促进可调度性分析的其他限制包括每个受保护对象最多一个队列(条目)的限制,在任何给定时间最多有一个调用方挂起,以及禁止任务终止。Ravenscar子集的完整定义出现在Ada 2012标准[6]中。

  虽然具有限制性,但 Ravenscar 子集也足够通用,可以表达一系列有用的任务习语,例如循环(周期性)任务;事件驱动(非定期或零星)任务、中断处理程序和共享资源(简单的受保护对象)。

  图 2 显示了图 1 中读取器/写入器示例变体中的 Ravenscar 子集,其中包含避免漂移的循环(周期性)任务。

  图2:图 1 中示例变体中的 Ravenscar 子集。

  

操作系统

  在 FACE 上下文中实现 Ravenscar 任务子集

  除了允许 Ravenscar 子集外,Ada 95 安全功能集还允许或禁止各种顺序语言功能。例如,安全基础功能集允许中断支持、具有单个默认处理程序的预定义异常以及来自 Ada 预定义环境的某些包,同时禁止动态分配。Ada 95安全扩展功能集通常允许异常处理,并允许在启动时动态分配,同时禁止释放。

  为任一安全功能集实现运行时支持库的挑战在于,如何以有助于分析相关保证要求的方式提供允许的功能。满足这一挑战的实现的一个示例是AdaCore的Ravenscar-Cert库,它支持安全基础和安全扩展功能集中允许的所有功能,并满足DO-178B或DO-178C中的适用目标。该库实现了 Ravenscar 任务功能、异常传播、最后机会处理程序和返回不受约束数组的函数的标记/发布机制(不需要堆管理)。Ravenscar-Cert库已经为Wind River的VxWorks 653和Lynx Software Technologies的LynxOS-178 RTOSes实现。此库中的 Ravenscar 任务支持小于 40 KB。

  迎接挑战

  并发编程对于设计和实现实时嵌入式应用程序,特别是FACE组件非常有用,但它带来了重大的软件工程挑战:

  •可移植性。Ravenscar 子集由 Ada 语言标准定义,其限制集可以帮助保证确定性行为。遵循Ravenscar子集的程序(以及对实现相关功能的其他限制)将跨不同的实现和平台移植,这是FACE方法的主要目标。Ada的Ravenscar任务子集可以帮助应对这些挑战。

  •可靠性。对于实时程序,可靠性不仅意味着功能正确性(计算正确的结果),还意味着时间可预测性(满足严格的截止日期)。Ravenscar 子集有助于以多种方式实现这些要求。禁止异步等复杂功能,允许的任务间通信的简单形式适用于静态分析,队列限制有助于计算最坏情况执行时间。Ravenscar 限制指定的任务调度和对象锁定策略同样有助于调度分析,并产生比传统循环执行更简单、更易于维护的体系结构。

  •效率。由于没有语义复杂性,因此可以实现“精益和平均”的运行时实现。不需要支持任务终止、队列管理和动态优先级等功能,并且正如 AdaCore 的 Ravenscar-Cert 库等实现所证明的那样,所需的功能可以有效地映射到底层实时操作系统提供的服务。

  审核编辑:郭婷

打开APP阅读更多精彩内容
声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉

全部0条评论

快来发表一下你的评论吧 !

×
20
完善资料,
赚取积分