面向安全关键系统的时间可预测多核代码生成方法研究

Multi-core processors will be widely used in safety-critical systems. Unfortunately, the introduction of performance-enhancing architectural elements, such as pipelines, out-of-order execution, dynamic branch prediction, multithreading, and caches, etc., as well as inter-cores resource-sharing, make the WCET (Worst-Case Execution Time) analysis of a system become more difficult. Thus, time-predictable system design is concerned with the challenge of building systems for which WCET can be statically and easily analyzed. At the software level, we propose a time-predictable multi-threaded code generation based on synchronous-model development. At the platform level, we propose a time-predictable multi-core architecture model in AADL (Architecture Analysis and Design Language), and then we map the multi-threaded code to this model. Real-time specifications propagate down in the system hierarchy. Therefore, our method integrates time predictability across several design layers, and finally reduces the complexity of WCET analysis. The research outcomes will also provide theoretical and technical supports for building time-predictable embedded system in avionics and space system industry.

能够提供更强计算能力的多核处理器将在安全关键系统中得到广泛应用。但是，由于现代处理器所使用的流水线、乱序执行、动态分支预测、多硬件线程、Cache等性能提高机制以及多核之间的资源共享，使得系统的最坏执行时间分析变得非常困难。为此，国际学术界提出设计时间可预测系统的思想，以降低系统的最坏执行时间分析难度。已有研究主要关注硬件层次及其编译方法的调整和优化，而较少关注软件层次，即时间可预测多线程代码的构造方法以及到多核硬件平台的映射。课题提出一种基于同步语言模型驱动的时间可预测多线程代码生成方法，并对代码生成器的语义保持进行证明；提出一种基于AADL的时间可预测多核体系结构模型，作为本课题研究的目标平台；最后，研究多线程代码到多核体系结构模型的映射方法，并给出系统性质的分析框架。课题研究结果可为航空航天工业界构造时间可预测嵌入式系统提供理论基础和方法支持。

安全关键系统广泛应用于航空航天等关键信息领域。能够提供更强计算能力的多核处理器将在安全关键系统中得到广泛应用。但是，由于现代处理器所使用的流水线、乱序执行、动态分支预测、多硬件线程、Cache等性能提高机制以及多核之间的资源共享，使得系统的最坏执行时间分析变得非常困难。为此，国际学术界提出时间可预测系统设计的思想，以降低系统的最坏执行时间分析难度。已有研究主要关注硬件层次及其编译方法的调整和优化，而较少关注软件层次，即时间可预测多线程代码的构造方法以及到多核硬件平台的映射。. 课题提出了一种基于同步语言（SIGNAL）模型驱动的时间可预测多线程代码生成方法，并基于定理证明器Coq对代码生成器的语义保持进行证明；提出了一种时间可预测多核体系结构模型，作为目标平台，研究多线程代码到多核体系结构的映射，并给出系统性质的分析框架；最后，将课题实现的同步语言验证编译器应用集成到课题组研制的安全关键软件形式化设计与验证平台MACAerospace中，实现AADL (Architecture Analysis and Design Language)架构和同步语言功能行为建模的无缝集成和代码自动生成，并与航天研究所合作，在航天控制子系统中进行了应用验证。. 本课题研究的面向多核处理器的时间可预测多线程代码生成方法以及同步语言和体系架构描述语言AADL混合建模及其代码自动生成方法，可为安全关键领域构造实际的时间可预测嵌入式系统提供理论基础和方法支持。