面向安全關鍵系統的時間可預測多核代碼生成方法研究

《面向安全關鍵系統的時間可預測多核代碼生成方法研究》是依託南京航空航天大學，由楊志斌擔任項目負責人的青年科學基金項目。

基本介紹

• 中文名：面向安全關鍵系統的時間可預測多核代碼生成方法研究
• 項目類別：青年科學基金項目
• 項目負責人：楊志斌
• 依託單位：南京航空航天大學

項目摘要

能夠提供更強計算能力的多核處理器將在安全關鍵系統中得到廣泛套用。但是，由於現代處理器所使用的流水線、亂序執行、動態分支預測、多硬體執行緒、Cache等性能提高機制以及多核之間的資源共享，使得系統的最壞執行時間分析變得非常困難。為此，國際學術界提出設計時間可預測系統的思想，以降低系統的最壞執行時間分析難度。已有研究主要關注硬體層次及其編譯方法的調整和最佳化，而較少關注軟體層次，即時間可預測多執行緒代碼的構造方法以及到多核硬體平台的映射。課題提出一種基於同步語言模型驅動的時間可預測多執行緒代碼生成方法，並對代碼生成器的語義保持進行證明；提出一種基於AADL的時間可預測多核體系結構模型，作為本課題研究的目標平台；最後，研究多執行緒代碼到多核體系結構模型的映射方法，並給出系統性質的分析框架。課題研究結果可為航空航天工業界構造時間可預測嵌入式系統提供理論基礎和方法支持。

結題摘要

安全關鍵系統廣泛套用於航空航天等關鍵信息領域。能夠提供更強計算能力的多核處理器將在安全關鍵系統中得到廣泛套用。但是，由於現代處理器所使用的流水線、亂序執行、動態分支預測、多硬體執行緒、Cache等性能提高機制以及多核之間的資源共享，使得系統的最壞執行時間分析變得非常困難。為此，國際學術界提出時間可預測系統設計的思想，以降低系統的最壞執行時間分析難度。已有研究主要關注硬體層次及其編譯方法的調整和最佳化，而較少關注軟體層次，即時間可預測多執行緒代碼的構造方法以及到多核硬體平台的映射。 課題提出了一種基於同步語言（SIGNAL）模型驅動的時間可預測多執行緒代碼生成方法，並基於定理證明器Coq對代碼生成器的語義保持進行證明；提出了一種時間可預測多核體系結構模型，作為目標平台，研究多執行緒代碼到多核體系結構的映射，並給出系統性質的分析框架；最後，將課題實現的同步語言驗證編譯器套用集成到課題組研製的安全關鍵軟體形式化設計與驗證平台MACAerospace中，實現AADL (Architecture Analysis and Design Language)架構和同步語言功能行為建模的無縫集成和代碼自動生成，並與航天研究所合作，在航天控制子系統中進行了套用驗證。 本課題研究的面向多核處理器的時間可預測多執行緒代碼生成方法以及同步語言和體系架構描述語言AADL混合建模及其代碼自動生成方法，可為安全關鍵領域構造實際的時間可預測嵌入式系統提供理論基礎和方法支持。