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

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

同步语言具有确定性并行和精确时间语义等特性,因此被广泛用于设计和验证安全关键软件.随着安全关键领域应用多核处理器逐渐成为趋势,同步语言的多线程代码生成及其语义保持证明研究成为研究热点.目前,已有同步语言代码生成方法还较少考虑多线程代码生成的语义保持证明.因此,本文提出一种同步语言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 structural operational semantics(based on transition systems)is proposed;Secondly,the clock calculus procedure is formally defined to generate clockedSIGNAL programs from source SIGNAL models,the procedure consists of the formal definition of the extraction function of clock relations and construction function of clause sets,the formal description of solving clock equations system and the definition of the clock dependency graph,the operational semantics of clockedSIGNAL structure is also constructed according to the transition systems of source SIGNAL models and the result of the clock calculus procedure;Thirdly,an abstract C-like subset structure is considered as the target language and its formal definition as well as the operational semantics are proposed,the transformation step from clockedSIGNAL programs to target C-like subset code contains two important functions:the computation function and the memory update function.The semantics consistency of the transformation step(named clockedSIGNAL2C)includes the proof of two directions:from clockedSIGNAL to C-like and from C-like to clockedSIGNAL which correspond to two lemmas.Considering the proof processes of two lemmas are similar,this paper mainly introduces the first lemma,i.e.clockedSIGNAL2C satisfies the unidirectional bisimulation equivalent relation.Finally,a theorem about the semantics consistency of the transformation step is proved to guarantee the semantic consistency between the SIGNAL program after clock calculus and the target C program after translation based on the bisimulation equivalent relation.