同步数据流语言可信编译器Vélus与L2C的比较

同步数据流语言（如Lustre、Signal）在航空、高铁、核电等安全关键领域得到广泛应用.例如,适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言.这类语言相关开发工具,特别是编译器的安全性问题也自然受到高度关注.近年来,基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一,也取得了瞩目的成果,如CompCert项目实现了产品级的可信C编译器.同样,人们也采用这种方法开展了同步数据流语言可信编译器的研发工作.主要关注从事这一工作的两个长线项目,二者均研发面向基于Lustre的同步数据流语言编译器,分别以Vélus和L2C代称.对Vélus和L2C从多个重要的角度进行较为深入的分析与比较.     

同步数据流语言高阶运算消去的可信翻译

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.     

同步数据流语言可信编译器的构造

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.     

一个C语言安全子集的可信编译器

以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器.然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估.之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器.最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率.     

同步数据流程序的可信排序

Lustre是一种广泛应用于核电、航空等高可信领域的同步数据流语言。用形式化验证的方法来实现Lustre到C的翻译并证明其过程能有效提高编译器的安全性。因为Lustre程序是并发执行的,需要对其进行因果分析和串行化。利用Coq工具,形式化定义拓扑排序的性质和相应层次的Lustre的语义;对Lustre程序进行因果分析和排序;证明排序后的程序满足拓扑排序的性质;证明任意两个满足拓扑排序性质的程序语义执行等价。从而实现了一种针对Lustre程序的可信排序过程。     

同步数据流语言输入结构体的可信翻译

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.     

同步语言Lustre的编译前端的设计与实现

同步语言Lustre所描述的反应系统通常应用在航空航天、国防建设等领域,对系统的正确性和安全性都要求很高。如果系统在运行时出现了正确性问题,很可能会导致系统崩溃,产生非常严重的后果。系统中的任何一个词法错误或者语法错误都应该受到重视,而且应该被及时纠正。因此,对Lustre语言进行正确的编译是十分重要的。传统的Lustre语言的编译器都采用OCaml语言描述,无法保证所有人员都能够很容易地理解和使用,而且,需要耗费开发人员大量的时间和精力。基于上述问题,提出了一种新型的Lustre语言编译器。新型的Lustre语言编译器前端主要采用C++语言进行描述,并对生成的抽象语法树的结构进行重新定义,简化了编译的过程。该编译前端会对一个经典的Lustre语言模型进行检测,通过对检测的结果进行分析,验证了该编译前端的可行性。     

DSP分块内存和多AGU的编译指示优化

分块内存和多地址生成器(AGU)是DSP普遍采用的体系结构.传统的C语言编译器没有针对分块内存和多AGU结构进行代码优化,导致生成代码无法满足性能需求,影响了C语言编译器在数字信号处理领域的应用.为了解决这个问题,提出基于编译指示,与分块内存和多AGU结构相关的编译优化算法.该算法利用定义引用链和引用定义链中的数据流信息,为地址计算指令和访存指令分配AGU,从而提高生成代码的指令级并行度.实验结果表明此算法能够达到较好的优化效果.     

试论C语言编译器的设计与实现

编译程序被认为是现代计算机系统的基本构成,本文重点分析了C语言编译器设计与实现的相关问题,文章先阐述了C语言编译器总体设计的相关内容,包括词法、语义分析等;再介绍了C语言编译器的实现路径,希望能对相关人员工作有所帮助.     

基于程序转化的SCADE模型检测

SCADE同步语言是一种常用的嵌入式系统程序设计语言.在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统.SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语言结构来精简代码.目前,相比Lustre语言,SCADE程序模型检测的学术研究相对落后.为此,文中提出了一种对SCADE程序进行模型检测的方法并实现了一款SCADE模型检测工具,该方法的核心思想是基于程序转化,即把SCADE程序经过词法分析、语法分析、抽象语法树生成与化简等操作最终转化为等价的Lustre程序,然后用JKind与SMT求解器完成模型检测.此外,通过理论推导和大量实验证明了工具的模型检测的正确性.实验结果表明,功能相同的两个SCADE和Lustre测试用例模型的检测结果相同,但SCADE程序的模型检测效率相对较低.     

Flush: an example of development by refinements in SCADE/Lustre

In the domain of safety-critical control systems, the Lustre/SCADE development environment has proved its value, with notable achievements such as the Hong Kong subway signaling system and Airbus A380 flight controls. The interest of the approach comes from the synchronous data-flow style of the Lustre language which makes it well-adapted to the culture of control engineers. Moreover Lustre is endowed with simple formal semantics which makes it amenable to formal development. The currently running Flush project consists in building a formal system development tool on top of Lustre, by taking advantage of the language formal properties. To this end, a refinement calculus is defined, encompassing both functional and temporal aspects. Refinement proof obligations are generated, and several proof approaches can be used to discharge them: model-checking, abstract interpretation, and theorem proving through repeated induction and, finally translation to PVS proof obligations. The resulting methodology is illustrated on the island example used by J.R. Abrial for presenting the B system method.     

Using Verified Data-Flow Analysis-based Optimizations in Attribute Grammars

Building verified compilers is difficult, especially when complex analyses such as type checking or data-flow analysis must be performed. Both the type checking and program optimization communities have developed methods for proving the correctness of these processes and developed tools for using, respectively, verified type systems and verified optimizations. However, it is difficult to use both of these analyses in a single declarative framework since these processes work on different program representations: type checking on abstract syntax trees and data-flow analysis-based optimization on control flow or program dependency graphs.We present an attribute grammar specification language that has been extended with constructs for specifying attribute-labelled control flow graphs and both CTL and LTL-FV formulas that specify data-flow analyses. These formulas are model-checked on these graphs to perform the specified analyses. Thus, verified type rules and verified data-flow analyses (verified either by hand or with automated proof tools) can both be transcribed into a single declarative framework based on attribute grammars to build a high-confidence language implementations. Also, the attribute grammar specification language is extensible so that it is relatively straight-forward to add new constructs for different temporal logics so that alternative logics and model checkers can be used to specify data-flow analyses in this framework.     

Optimizing compiler for the procedural subset of the algebraic programming language of the APS system

Conclusion An L2B-L2C optimizing compiler has been developed for compiling the procedural subset of the interpreted untyped language APLAN of the algebraic programming system APS into C. Controlled automatic compiling of procedures is regarded as a technological step toward efficient solution of problems in an algebraic programming environment. A distinctive feature of the compiler is that optimization is initiated by the user and relies on hierarchical algebraic specifications. If no specifications are present, the system guarantees compilation consistent with common APLAN semantics. The compiler is formally described on two levels. On the architectural level, we describe the general structure of the compiling process. The main data structures used for optimization are dictionaires of algebraic program components and expression type arrays. The semantic level of multialternative compiling of language constructs is represented in the language of relationships with selection of an appropriate translation alternative. The implementation of the proposed compiler requires a flexible support environment, which allows nonhomogeneous processing of an extended source language, in particular construction of static and dynamic information environments, compilation of the procedural part, and also analysis of the compiling environment, definition of the set of translations of procedural constructs, and selection of the best translation alternative for each particular case. An implementation of the proposed compiler is described in [13]. Translated from Kibernetika i Sistemnyi Analiz, No. 6, pp. 3–16, November–December, 1995.     

Type-based Initialization Analysis of a Synchronous Data-flow Language

One of the appreciated features of the synchronous data-flow approach is that a program defines a perfectly deterministic behavior. But the use of the delay primitive leads to undefined values at the first cycle; thus a data-flow program is really deterministic only if it can be shown that such undefined values do not affect the behavior of the system.This paper presents an initialization analysis that guarantees the deterministic behavior of programs. This property being undecidable in general, the paper proposes a safe approximation of the property, precise enough for most data-flow programs. This analysis is a one-bit analysis — expressions are either initialized or uninitialized — and is defined as an inference type system with sub-typing constraints. This analysis has been implemented in the Lucid Synchrone compiler and in a new Scade-Lustre prototype compiler. It gives very good results in practice.     

An Extended ANSI C for Processors with a Multimedia Extension

This paper presents the Multimedia C language, which is designed for the multimedia extensions included in all modern microprocessors. The paper discusses the language syntax, the implementation of its compiler and its use in developing multimedia applications. The goal was to provide programmers with the most natural way of using multimedia processing facilities in the C language. The MMC language has been used to develop some of the most frequently used multimedia kernels. The presented experiments on these scientific and multimedia applications have yielded good performance improvements.     

Compilation of functional languages using flow graph analysis

A system based on the notion of a flow graph is used to specify formally and to implement a compiler for a lazy functional language. The compiler takes a simple functional language as input and generates C. The generated C program can then be compiled, and loaded with an extensive run-time system to provide the facility to experiment with different analysis techniques. The compiler provides a single, unified, efficient, formal framework for all the analysis and synthesis phases, including the generation of C. Many of the standard techniques, such as strictness and boxing analyses, have been included.