Retargeting a hardware compiler using protocol converters

We show how to retarget a compiler for occam-like programs from generating two-phase delay-insensitive circuits to generating four-phase speed independent circuits. The specifications of the two-phase circuit elements for our compiler are used to produce a set of equivalent specifications for four-phase circuit elements using a set of protocol converters. Automatic tools have been used in checking that our four-phase implementations satisfy their specifications.     

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.     

Correct compilation of specifications to deterministic asynchronous circuits

Powerful methods have been developed by A. martin and others wherby asynchronous circuits may be automatically constructed by starting from high-level specifications and incrementally transforming them into asynchronous circuits. In this paper we make the informal arguments for the correctness of this compilatin process mathematically rigorous. With rigorsouly justified transformations, specifications may be translated into circuits that provably meet their specification. A full proof of the correctness of the circuit compiler is given. Other results of independent interest include: the process model takes fairness of gates into account, hazard-freeness is formally defined, and all hazard-free circuits constructed solely of and, or, not gates and C elements are proven to behave deterministically to any outside observer. A novel notion of equivalence is used to justify the correctness of the compiler.     

Banner layout retargeting with hierarchical reinforcement learning and variational autoencoder

In many advertising areas, banners are often generated with different display sizes, so designers have to make huge efforts to retarget their designs to each size. Automating such retargeting process can greatly save time for designers and let them put creativity on new ads. This paper proposes a hierarchical reinforcement learning-based (HRL-based) method and a variational autoencoder-based (VAE-based) method by treating the automated banner retargeting problem as a layout retargeting task. The HRL and VAE models are trained separately to learn the scaling and positioning policy of the design elements from an original (base) layout. Hence, the proposed method can generate appropriate layouts for different target banner sizes. Meanwhile, evaluation metrics are proposed to assess the quality of generated layouts and are also reward conditions during the training process. To evaluate performances of the two models, SOTA methods such as Non-linear Inverse Optimization (NIO), Triangle Interpolation (TI), and Layout GAN (LGAN) are implemented and compared. Experimental results show that both HRL- and VAE-based methods retarget design layouts effectively, and the VAE model achieves better performance than the HRL model.

     

The mechanical generation of fault trees for reactive systems via retrenchment II: clocked and feedback circuits

The retrenchment approach to the mechanical construction of fault trees, introduced in the first paper for combinational logic circuits, is extended to handle clocked circuits and then feedback circuits. The temporal behaviour of clocked circuits is captured using their causal relations, and the potentially unbounded behaviour of cyclic circuits is decomposed into an iteration over their acyclic counterparts. The repercussions of all this for the theory of retrenchment are elaborated. For clocked circuits, the techniques we present allow glitches and other transient errors to be properly described. For feedback circuits, the plethora of behaviours that can occur, give rise to infinitary fault trees of an appropriate kind. All this paves the way for automated fault tree generation for reactive systems.     

非规则三维建筑模型的保结构变形

为了快速生成大量与输入风格一致的三维建筑模型,提出一种针对非规则三维建筑模型的保结构交互式变形技术.该技术以一般的三维网格模型作为输入,经过若干预处理操作形成带标记的包围盒层次结构,以此作为变形操作的分析基础.变形算法的核心思想是将原始的复杂结构分解为一组一维的结构序列,然后逐条对一维结构序列施加变形操作.在对一维结构序列的变形过程中尽可能以可重复的元素来填充变形空间,实现对输入结构特点的保持.实验结果表明,该技术可用于各种不同风格的建筑模型.     

针对嵌入架构的Open64编译器重定向

基于开源高性能编译器Open64,以PowerPC嵌入式处理器为例,开展重定向关键问题研究和代码实现,自主开发完成一款具有工业产品水准的高性能开源编译器后端。gcc-c.torture和SPEC2000实测结果表明,在正确性和性能方面,该编译器均接近或达到和GCC编译器相当的水平,为进一步研究和应用提供良好的编译工具支持以及实现参考,同时为后续自动重定向等工作奠定基础。     

Formal Proofs About Rewriting Using ACL2

We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization and representation aspects of our work using the first-order, quantifier-free logic of ACL2 and we sketch some of the main points of the proof effort. First, we present a formalization of abstract reduction systems and then we show how this abstraction can be instantiated to establish results about term rewriting. The main theorems we mechanically proved are Newman's lemma (for abstract reductions) and Knuth–Bendix critical pair theorem (for term rewriting).     

Specification,Verification and Prototyping of an Optimized Compiler

This paper generalizes an algebraic method for the design of a correct compiler to tackle specification and verification of an optimized compiler. The main optimization issues of concern here include the use of existing contents of registers where possible and the identification of common expressions. A register table is introduced in the compiling specification predicates to map each register to an expression whose value is held by it. We define different kinds of predicates to specify compilation of programs, expressions and Boolean tests. A set of theorems relating to these predicates, acting as a correct compiling specification, are presented and an example proof within the refinement algebra of the programming language is given. Based on these theorems, a prototype compiler in Prolog is produced.     

Ultimate periodicity of orbits for min-max systems

The ultimate periodicity theorem is an important result in min-max systems theory. It was first proved by Olsder and Perennes in their unpublished work. In this paper, we present a new proof. This proof is also based on two important theorems: the existence of cycle time for any min-max function and the Nussbaum-Sine theorem. However, two different techniques, pure min-max function and conditional redundancy, are used to obtain two important intermediate results. The purpose of this paper is to provide a simple alternate proof to the ultimate periodicity theorem.     

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

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

A Formally Verified Compiler Back-end

This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its soundness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.     

基于时空约束的运动编辑和运动重定向

近年来兴起的运动捕获已成为人体动画中最有应用前景的技术之一，目前运动捕获手段很多，但是通常成本高，而且捕获到的运动类型比较单一，为了提高运动捕获数据的重用性，生成与复杂场景协调的多样的动画，必须对捕获的运动数据进行编辑和重定向处理，介绍了一种基于时空约束的运动编辑和运动重定向方法，通过规定一组时空约束条件，建立相应的目标函数，采用逆向运动学和数值优化方法求解出满足约束条件的运动姿势，实验结果表明，该方法可以生成多种满足不同场景婪泊逼真运动，提出了数据的重用性。     

面向关节坐标运动数据重定向的通用双向循环自编码器

针对面向关节坐标表示的骨骼运动数据重定向网络缺乏通用性的问题,提出一种能够实现源骨骼到多种骨骼运动重定向的通用双向循环自编码器.该自编码器由基于关节坐标表示的运动数据以重建误差为损失函数训练得到.在完成训练后,首先用自编码器计算源运动数据对应的隐变量和重建运动,然后对重建运动施加骨骼长度约束、足迹约束、根关节位置约束以及骨骼角度约束,并将损失反向传播至隐变量空间中优化隐变量,通过多次迭代得到重定向后运动.在CMU运动数据库上的实验结果表明,提出的自编码器及4种约束能够实现基于关节坐标表示的运动数据的重定向,并且得到的重定向运动在骨骼长度误差、骨骼角度误差、末端效应器轨迹以及平滑性上具有更好的效果.     

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

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

A Certifying Code Generation Phase

Guaranteeing correctness of compilation is a vital precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof one can be sure that the compiler produced correct code. This paper reports on the construction of a certifying code generation phase for a compiler. It is part of a larger project aimed at guaranteeing the correctness of a complete compiler. We emphasize on demonstrating the feasibility of the certifying compilation approach to code generation and focus on the implementation and practical issues. It turns out that the checking of the certificates is the actual bottleneck of certifying compilation. We present a proof schema to overcome this bottleneck. Hence we show the applicability of the certifying compilation approach for small sized programs processed by a compiler's code generation phase.     

Optimizing Nested Loops Using Local CPS Conversion

Local CPS conversion is a compiler transformation for improving the code generated for nested loops by a direct-style compiler that uses recursive functions to represent loops. The transformation selectively applies CPS conversion at non-tail call sites, which allows the compiler to use a single machine procedure and stack frame for both the caller and callee. In this paper, we describe LCPS conversion, as well as a supporting analysis. We have implemented Local CPS conversion in the MOBY compiler and describe our implementation. In addition to improving the performance of loops, Local CPS conversion is also used to aid the optimization of non-local control flow by the MOBY compiler. We present results from preliminary experiments with our compiler that show significant reductions in loop overhead as a result of Local CPS conversion.