同步语言多线程代码生成的语义保持证明方法  

A Semantic Preservation Proving Method of Multi-Threaded Code Generation for Synchronous Language

作　　者：袁胜浩 杨志斌[1,2] 张博林 周勇 薛垒[3] BODELEIX Jean-Paul FILALI Mamoun YUAN Sheng-Hao;YANG Zhi-Bin;ZHANG Bo-Lin;ZHOU Yong;XUE Lei;BODEVEIX Jean-Paul;FILALI Mamoun(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106;Key Laboratory of Safety-Critical Software,Ministry of Industry and Information Technology,Nanjing 211106;Shanghai Aerospace Electronic Technology Institute,Shanghai 201109;IRIT-University of Toulouse,Toulouse 31062,France)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]高安全系统的软件开发与验证技术工信部重点实验室,南京211106 [3]上海航天电子技术研究所,上海201109 [4]IRIT-University of Toulouse,Toulouse 31062France

出　　处：《计算机学报》2020年第11期2216-2226,共11页Chinese Journal of Computers

基　　金：国家自然科学基金(61502231);航空科学基金(201919052002);GF基础科研重点项目(JCKY2016203B011);中央高校基本科研业务费专项资金资助(NP2017205);南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20181603)资助.

摘　　要：同步语言具有确定性并行和精确时间语义等特性,因此被广泛用于设计和验证安全关键软件.随着安全关键领域应用多核处理器逐渐成为趋势,同步语言的多线程代码生成及其语义保持证明研究成为研究热点.目前,已有同步语言代码生成方法还较少考虑多线程代码生成的语义保持证明.因此,本文提出一种同步语言SIGNAL多线程代码生成的语义保持证明方法:首先形式化定义编译过程中源、目标、中间语言的结构化操作语义;其次形式化定义多线程代码生成过程;最后基于互模拟等价思想证明编译前后的语义一致性.Safety-critical software is widely used in the fields of avionics,space systems,and nuclear power plants:Malfunctions of safety-critical software can lead to accidents that can potentially put people,environment,property,and mission in serious risks such as environmental catastrophes and loss of lives.Synchronous Languages are adopted for the design and the verification of safety-critical software,due to their characteristic features,for instance the description of deterministic concurrency behaviors and precise timing semantics.Recently,safety-critical domains have evolved to use high computation performance provided by multicore platforms to implement more complex functionality.Therefore the multi-threaded code generation approach for synchronous languages and related semantic preservation proof have been research hotspots.However,the existing studies on synchronous languages mainly concern the semantic preservation of sequential code generation from synchronous languages.Such as the verified synchronous language Lustre compiler Vélus supports sequential C code generation,the verified Lustre compiler L2C translates Lustre models to Clight programs which can be considered as the input of the CompCert compiler and the translation validation approach is used to verify the transformation steps from the synchronous language SIGNAL to sequential C code.They pay a little attention to the semantic preservation of multi-threaded code generation.As multi-core processors gradually become widely used in safety-critical systems,it is necessary to consider the semantic preservation of multi-threaded code generation approach for synchronous languages.Therefore,this paper presents a verified multi-threaded code generation method for the synchronous language SIGNAL.Firstly,a common SIGNAL subset which is compatible with two existing SIGNAL compilers Polychrony and MiniSIGNAL,is selected as the start point to consider the proof of semantic preservation of the multi-threaded code generation process and its formal syntax and stru

关 键 词：同步语言 安全关键软件 多任务代码生成 语义保持证明 COQ 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]