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

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

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

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

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

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

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

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

可信编译器L2C的核心翻译步骤及其设计与实现

同步数据流语言（如Lustre）近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好”误编译”问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证取得了很大的成功,如CompCert C编译器.L2C是基于这种方法开发的可信编译器,它以扩展的Lustre语言为源语言,以Clight （CompCert中的C语言子集）为目标语言.就我们所知,L2C是同类工作中唯一面向实际工业应用的同步数据流语言编译器.本文重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.     

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

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

PCC中数组边界检查的优化和生成

PCC的数组边界检查存在着由于无法确定数组下标表达式符号值的范围，而造成拒绝执行一些安全的移动代码等问题。本文给出的一种数组边界检查的优化及生成算法，不仅能够比较好地解决了这一问题，同时还生成了循环不变式注解中的条件谓词。我们设计的编译器——认证编译器——已经实现了这些算法，并完成了从用C编程语言的类型安全子集编写的源程序到携带注解的Intelx86／linux汇编语言程序的编译过程。由于基于语言安全策略系统的证明是建立在携带注解的代码基础之上的，因此该认证编译器中实现的算法在移动代码安全检查中非常有用。     

基于区域图数据流分析的通信优化算法

减少通信开销对于并行化编译器生成高效的分布代码是非常重要的.首先提出了一个冗余并行执行模型(RPEM)作为通信优化算法生成的目标程序的执行模型,之后给出了区域图的概念和区域最大化算法,在最大化区域图的基础上进行数据流分析可以增大数据流分析粒度,提高分析的效率,同时也有助于通信的提前与合并.最后提出了一种基于区域图数据流分析的通信优化算法.该算法能够进行跨循环、跨过程的数据流分析,提高分析的精度,改善通信优化效果.实验结果表明,该算法对于通信量较大的程序能够有效地减少通信的次数和通信量,具有良好的可扩展性.     

出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

面向同步规范的并行代码自动生成

随着对安全攸关实时系统功能与非功能要求的日益增加,使用多核技术将成为发展趋势.如何在多核平台条件下保证系统运行的可信任性及可靠性是学术上和应用上的关键问题.目前基于形式化方法的系统设计、验证以及自动代码生成已经在单核平台上形成很多研究成果,但在多核平台上的研究仍面临许多科学问题.同步语言SIGNAL是一种被广泛应用于安全攸关实时系统功能设计的形式化方法,适用于对系统确定性并发行为的描述.SIGNAL编译器也支持将同步规范SynchronousSpecification）生成仿真代码,以对其进行验证与分析.然而现有研究较少关注从SIGNAL同步规范到支持跨平台并行代码的生成方法.本文研究面向SIGNAL同步规范的并行自动代码生成方法.提出了方程依赖图EDG的概念,将SIGNAL规范转换为EDG以分析其全局数据依赖关系;研究了对EDG进行任务划分获取规范中可以并行执行部分的算法;最后,以跨平台并行编程API-OpenMP作为对象,结合程序中信号的时钟关系,将并行任务映射到OpenMP并行代码,并进行了实例验证.     

Towards a verified compiler prototype for the synchronous language SIGNAL

SIGNAL belongs to the synchronous languages family which are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL compiler, we propose a new intermediate representation (named S-CGA, a variant of clocked guarded actions), to integrate more synchronous programs into our compiler prototype in the future. The front-end of the compiler, i.e., the translation from SIGNAL to S-CGA, is presented. As well, the proof of semantics preservation is mechanized in the theorem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multithreaded code generation with time-predictable properties. With the rising importance of multi-core processors in safetycritical embedded systems or cyber-physical systems (CPS), there is a growing need for model-driven generation of multithreaded code and thus mapping on multi-core. We propose a time-predictable multi-core architecture model in architecture analysis and design language (AADL), and map the multi-threaded code to this model.     

一种改进数据流图的子字并行程序表示方法

论文致力于对图像处理算法的串行C程序进行子字并行分析,并重定向到带有多媒体扩展的通用处理器和多媒体专用嵌入式微处理器。图像处理算法的特点决定其是内在可并行的,这种并行粒度介于数据并行(DLP)和指令级并行(ILP)之间,称之为子字并行。但是,当前的编译技术很难充分挖掘和定位程序基本块内的子字并行,对此设计了一种基于流图程序表示的编译方法,能够从串行程序中显式地定位子字并行。扩展了编译器的功能,增加了特定的模式库,基于模式识别的控制流和数据流分析后,产生特定的子字并行流图(SWFG,Sub-WordFlowGraph),并将该图作为中间表示,提供给子字并行指令选择,进而实现有效的子字并行代码产生。     

基于子字并行的串行图像处理算法表示方法

多媒体应用程序的一个最突出的特点就是其内在的并行性,要求同时对多个数据单元进行相同的规则操作,这种并行性被称为子字并行。如何让编译器产生有效的并行代码,如何从普通的串行C程序中识别出子字并行指令,是一个前沿性的研究课题。提出了一种用于实现对串行源代码进行显式表示的方法,该方法对数字信号处理领域常用的同步数据流图方法进行改进,结合模式匹配技术,着眼于内层循环,通过扩展规范的模式库,对带模式识别的数据流、控制流进行分析,能够从串行应用程序中自动地提取其固有的子字并行,得到显式的并行化中间表示,基于这种数据流图表示,采用改进的树模式匹配实现子字并行指令选择和代码生成。实验测试表明了该方法的有效性。     

CPCC抽象语法树的三地址码生成

为了便于代码优化及指令生成,在并行C语言编译器CPCC（Concordia Parallel C Compiler）将源程序的抽象语法树（Abstract Syntax Tree, AST）转换成目标机PAAG（Parallel Array Architecture GPU）处理器的汇编代码时,采用了三地址码作为中间表示形式。基于CPCC AST的结构特点,将AST到三地址码的转换分为三类,即一般表达式的翻译、布尔表达式的翻译以及语句的翻译,并给出了其详细设计思路及是实现方法。实验结果表明,该方案实现了从源码的抽象语法树到三地址码的转换。     

Formal verification of synchronous data-flow program transformations toward certified compilers

Translation validation was invented in the 90’s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation validation is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its transformed counterpart as first-order formulas which are called clock models and synchronous dependence graphs (SDGs), respectively. We then introduce clock refinement and dependence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock models and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.     

一种面向向量化的动态指针别名分析框架

指针别名分析是数据流分析中的关键性技术,其分析结果是编译优化和程序变换的基础.在向量化方法和动态指针别名分析相关研究的基础上,设计了一种面向向量化的动态指针别名分析框架.该框架通过动态插桩和试运行提取指针别名信息,并反馈到向量化阶段指导向量化代码生成.从提取候选别名分析集、插桩及试运行和反馈优化3个方面对整体框架进行分析和研究.该框架基于Open64实现,并以通用测试集GCC-VECT和典型应用进行了实验评估,结果表明,该框架相比静态指针别名分析具有更精确的别名分析结果,该结果能够有效改进向量化程序的加速比.     

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.     

Run-Time Validation of Speculative Optimizations using CVC.

Translation validation is an approach for validating the output of optimizing compilers. Rather than verifying the compiler itself, translation validation mandates that every run of the compiler generate a formal proof that the produced target code is a correct implementation of the source code. Speculative loop optimizations are aggressive optimizations which are only correct under certain conditions which cannot be validated at compile time. We propose using an automatic theorem prover together with the translation validation framework to automatically generate run-time tests for such speculative optimizations. This run-time validation approach must not only detect the conditions under which an optimization generates incorrect code, but also provide a way to recover from the optimization without aborting the program or producing an incorrect result. In this paper, we apply the run-time validation technique to a class of speculative reordering transformations and give some initial results of run-time tests generated by the theorem prover CVC.