What Level of Mathematical Reasoning can Computer Science Demand of a Software Implementer?: Auf Deutsch: Welche Art mathematischer Argumentation darf die Informatikwissenschaft einem Softwareimplementierer auf jeden Fall zumuten?

The article starts out from the observation that software engineering splits in two large activity areas: Software specification with its verification and software implementation with its verification. To find answers to the question in the title the article studies a practical systems software engineering area where theory is better developed than compared to other areas: Compiler construction. Our answer is a conclusion from work in the DFG-project Verifix, U.Karlsruhe, U.Kiel, U.Ulm, 1995-2003. One very complex cooperational task has been construction of a so called initial correct compiler for a realistic high level programming (and compiler writing) language correctly implemented and executed on a real life host processor. The interface between compiling specification and compiler implementation is given by algebraic-style, conditional formula transformation or program term rewriting rules which the specifier figures out and must prove correct w. r. t. source program and target processor semantics and data and states representations.Intensive cooperation of compiling specifiers and compiler implementers has revealed that the implementer's mathematical reasoning is algebraic reasoning of moderate depth. The specifier overtakes semantical issues and does induction proofs, a field of much more intricate mathematical reasoning.     

Verified compilation of communicating processes into clocked circuits

We have previously developed a verified algorithm for compiling programs written in an occam-like language into delay-insensitive circuits. In this paper we show how to retarget our compiler for clocked circuits. Since verifying a hardware compiler is a huge effort, it is significant that we are able to retarget our compiler proof without recreating that effort.The chief contribution of this paper is the methodology used for retargeting our compiler which is based upon a new model for systems with both synchronous and asynchronous behaviour. The retargeting proof utilizes both theorems proved algebraically by hand and theorems proved automatically by state exploration. The technique of protocol conversion is used extensively in modularizing the proof of the clocked implementation.     

RETE网络中的优化编译模式及其PVS形式验证

In the compilation of rule program to the intermediate code-RETE network,optimizing compilation is an important compiler schema,and is a necessary step in the compiler verification.In this paper,we discuss optimization schemas in rule program compilation,and prove the semantic equivalence theorems of these schemas.Firstly,the structure of RETE network and its PVS specification are represented.Secondly,three kinds of optimization schemas are listed.Then algorithms evaluating semantics of target RETE network are given.Finally,we prove the semantic equivalence theorems with theorem prover PVS (Prototype Verification System).     

The compiler as a validation and evaluation tool

Like a processor executes flawlessly at different frequencies, a compiler should produce correct results at any optimization level. The Intel^® Itanium^® processor family with its new features, like the register stack engine and control- and data speculation, provides new and unique challenges for ported software and compiler technology. This paper describes validation and evaluation techniques that can be employed in compilation tools and can help to get a cleaner port of an application, a more robust compilation system and even insights into performance tuning opportunities. Using Itanium as a specific example, the paper explains why the register stack engine (RSE), the large register file, or control- and data speculation can potentially expose bugs in poorly written or compiled software. It then demonstrates validation and evaluation techniques to find or expose these bugs. An evaluation team can employ them to find, eliminate and evaluate software bugs. A compiler team can use them to make the compiler more stable and robust. A performance analysis team can use them to uncover performance opportunities in an application. We demonstrate our validation and evaluation techniques on code examples and provide run-time data to indicate the cost of some of our methods.     

Deriving a compiler from an operational semantics written in VDL

This paper addresses the issue of compiler correctness. The approach taken is to systematically construct a correct compiler for a language from a formal semantic definition of the language. For this purpose, an operational semantics of a language is chosen as the basis for the approach. That is, the compiler for a language is derived from an interpreter of the language. The derivation process uses the notion of mixed computation proposed by Ershov. Briefly stated, one begins interpreting and when a primitive state changing instruction is about to be executed, the instruction is emitted as code instead. The correctness of all compilers produced by the method is guaranteed by proving the derivation rules correct. This proof is a one-time task for each specification language. The specification language studied in this paper is the Vienna Definition Language (VDL). The object code generated by the compiler is in an intermediate language close to an assembly language. Therefore, the translation from the intermediate language into the assembly language should be straightforward.     

A demonstrably correct compiler

As critical applications grow in size and complexity, high level languages, rather than better-trusted assembly languages, will be used in their development. This adds potential for extra errors to creep in, especially in the now necessary compiler. To avoid these new errors, it is necessary to have a formal specification of the high level language, and a formal development of its compiler. We outline what we believe is a practical route for achieving a demonstrably correct compiler, and describe a prototype compiler we have built by this route for a small, but non-trivial, language.     

Temporal logic programming for assembly sequence planning

A temporal-constraint logic programming framework for the specification and automatic verification and synthesis of assembly sequences is developed. The implemented tool is based on the formulated and derived precedence properties for a general mechanical assembly. This tool, called the Mechanical Assembly Sequence Satisfiability Checker (MASS-C), supports the use of a subset of temporal logic for assembly constraint specification. MASS-C provides the logic programming framework by which the designer can be relieved of the tedium of finding the assembly sequences, and the assembly sequence planning process manifests itself in the implicit modelling of assembly sequences by acquiring and formulating the set of correct and complete assembly constraints as a logic program. MASS-C implements a class of temporal expressions as predicates for logic programming of assembly constraints. It provides facilities to either verify an assembly sequence or synthesise all assembly sequences that satisfy the specified constraints composed as a logic program. Two examples illustrate the use of MASS-C for such verification and synthesis.     

The multiflow trace scheduling compiler

The Multiflow compiler uses the trace scheduling algorithm to find and exploit instruction-level parallelism beyond basic blocks. The compiler generates code for VLIW computers that issue up to 28 operations each cycle and maintain more than 50 operations in flight. At Multiflow the compiler generated code for eight different target machine architectures and compiled over 50 million lines of Fortran and C applications and systems code. The requirement of finding large amounts of parallelism in ordinary programs, the trace scheduling algorithm, and the many unique features of the Multiflow hardware placed novel demands on the compiler. New techniques in instruction scheduling, register allocation, memory-bank management, and intermediate-code optimizations were developed, as were refinements to reduce the overhead of trace scheduling. This article describes the Multiflow compiler and reports on the Multiflow practice and experience with compiling for instruction-level parallelism beyond basic blocks.     

Towards Acceptability of Optimizations: An Extended View of Compiler Correctness

The theory of relative program correctness and its preservation allows for elaborate and practically adequate definitions of correct implementation notions as they are established by transformations implemented in a compiler. It generalizes Hoare's and Floyd's partial and total program correctness and correctness preservation by classifying finite and infinite errors to be either acceptable (unavoidable) or unacceptable (chaotic, to be avoided). We will define correct implementation by particular compositional diagram commutativities, and we will further extend this theory also to express correctness of compiling specifications and of compiler programs and their implementations in the same uniform relational setting. Unacceptable error outcomes can semantically model pre-conditions such as well-formedness conditions for compilers or optimization pre-conditions for user programs. Our theory allows to distinguish between different correct implementation requirements, for instance (horizontally) for user programs or (vertically) for the compiler implementation, just as if we would switch on and off compiler options and tune one compiler to appropriately preserve correctness in different application domains.     

显式并行资源计算结构及其编译优化

提出并分析了一种新的基于超长指令字(VLIW)思想的微处理器模型,该模型提供了体系结构可见的处理器内部结果寄存器和数据通路,允许优化编译器进行直接的控制和调度,并依赖编译器保证操作之间的依赖关系,以简化硬件设计并获得更高的时钟频率.基于该目标模型,构造了一个完整的优化编译和模拟环境,提出、分析并实现了相应的软件旁路优化以及集成式的资源分配与指令调度算法.     

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.     

BWDSP104X多条件谓词编译优化

目前BWDSP104X编译器对程序中条件分支的处理是采用传统的谓词优化方法,及每条指令和一个谓词相关,只有当谓词为真时指令才被执行,但它存在的局限性是当涉及到多条件谓词时,并不能消除跳转分支,且多条件谓词之间可能存在控制依赖关系,不利于指令并行和指令流水. 因此在现有编译器框架下,针对传统谓词优化方法的不足之处,本文提出一种基于BWDSP104X体系结构下多条件谓词编译优化方法. 实验结果表明,与传统谓词优化方法相比,该优化算法在BWDSP104X编译器上能够取得平均5.62的加速比.     

Specification and correctness proof of a WAM extension with abstract type constraints

We provide a mathematical specification of an extension of Warren's Abstract Machine (WAM) for executing Prolog to type-constraint logic programming and prove its correctness. Our aim is to provide a full specification and correctness proof of a concrete system, the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L.In this paper, while leaving the details of the PAM's type constraint representation and solving facilities to a sequel to this work, we keep the notion of types and dynamic type constraints abstract to allow applications to different constraint formalisms like Prolog III or CLP(R). This generality permits us to introduce modular extensions of Börger's and Rosenzweig's formal derivation of the WAM. Since the type constraint handling is orthogonal to the compilation of predicates and clauses, we start from type-constraint Prolog algebras with compiled AND/OR structure that are derived from Börger's and Rosenzweig's corresponding compiled standard Prolog algebras. The specification of the type-constraint WAM extension is then given by a sequence of evolving algebras, each representing a refinement level, and for each refinement step a correctness proof is given. Thus, we obtain the theorem that for every such abstract type-constraint logic programming system L, every compiler to the WAM extension with an abstract notion of types which satisfies the specified conditions, is correct.The first author was partially funded by the German Ministry for Research and Technology (BMFT) in the framework of the WISPRO Project (Grant 01 IW 206). He would also like to thank the Scientific Center of IBM Germany where the work reported here was started.     

One-pass transformations of attributed program trees

Summary The classical attribute grammar framework can be extended by allowing the specification of tree transformation rules. A tree transformation rule consists of an input template, an output template, enabling conditions which are predicates on attribute instances of the input template, and re-evaluation rules which define the values of attribute instances of the output template. A tree transformation may invalidate attribute instances which are needed for additional transformations.In this paper we investigate whether consecutive tree transformations and attribute re-evaluations are safely possible during a single pass over the derivation tree. This check is made at compiler generation time rather than at compilation time.A graph theoretic characterization of attribute dependencies is given, showing in which cases the recomputation of attribute instances can be done in parallel with tree transformations.Part of this work was done while the author was visiting Tartan Laboratories Inc., Pittsburgh, PA, USA     

An evaluation of throw-away compiling

The performance of a throw-away compiler for Pascal is compared with an interpreter, a threaded code compiler and a traditional compiler. In addition an evaluation is given of the performance of various strategies for dynamic and throw-away compiling in a small workspace.     

An investigation into concurrent semantic analysis

Concurrency is an attractive method for reducing the execution time of compilers. By dividing source programs into segments which can be compiled concurrently, the task of compiling programs can be accelerated. Many of the difficult problems which arise when constructing a concurrent compiler occur in the implementation of the semantic analyser. This paper investigates the problems involved in designing the semantic analyser for a concurrent compiler for a modern, block-structured language. Several approaches to solving the problems which arise are presented. These solutions are then implemented as part of a concurrent Modula-2 + compiler, running on a shared memory multiprocessor. A performance evaluation of these semantic analysers is presented.     

可信编译理论及其核心实现技术:研究综述

编译器是重要的系统软件之一,高级语言编写的软件都必须经过编译器的编译才能成为可执行程序。编译器的可信性对于整个计算机系统而言具有非常关键的意义,如果编译器不可信,则很难保证系统所运行软件的可信性。可信编译是指编译器在保证编译正确的同时提供相应的机制保证编译对象的可信性,对可信编译理论和技术的研究具有重要理论意义和实用前景。阐述了可信编译器的概念,介绍了编译过程正确性的形式化定义,对可信编译的主要研究进行了概括。在全面分析可信编译研究现状的基础上,从编译器自身可信性和确保编译对象可信性两个方面,对可信编译器设计和实现的相关理论和方法进行了分类和总结。最后,讨论了可信编译有待解决的问题和未来的研究方向。     

Power-Aware Compilation for Register File Energy Reduction

Most power reduction techniques have focused on gating the clock to unused functional units to minimize static power consumption, while system level optimizations have been used to deal with dynamic power consumption. Once these techniques are applied, register file power consumption becomes a dominant factor in the processor. This paper proposes a power-aware reconfiguration mechanism in the register file driven by a compiler. Optimal usage of the register file in terms of size is achieved and unused registers are put into a low-power state. Total energy consumption in the register file is reduced by 65% with no appreciable performance penalty for MiBench benchmarks on an embedded processor. The effect of reconfiguration granularity on energy savings is also analyzed, and the compiler approach to optimize energy results is presented.     

一种寄存器分配的优化策略

寄存器作为机器硬件结构中有限的宝贵资源，使得寄存器分配技术成为编译器最为关键的优化技术之一。寄存器分配效率提高的关键在于如何最大限度地减少溢出带来的开销，论文针对这一问题，提出了在传统RISC芯片存储结构的基础上加一级缓冲寄存器来处理溢出的设想，并以作者为一种新型的RISC体系结构微处理器研制的编译系统为背景，提出了基于该缓冲寄存器的寄存器分配优化策略。实验表明，优化效果明显。