Coinductive Verification of Program Optimizations Using Similarity Relations

Formal verification methods have gained increased importance due to their ability to guarantee system correctness and improve reliability. Nevertheless, the question how proofs are to be formalized in theorem provers is far from being trivial, yet very important as one needs to spend much more time on verification if the formalization was not cleverly chosen. In this paper, we develop and compare two different possibilities to express coinductive proofs in the theorem prover Isabelle/HOL. Coinduction is a proof method that allows for the verification of properties of also non-terminating state-transition systems. Since coinduction is not as widely used as other proof techniques as e.g. induction, there are much fewer “recipes” available how to formalize corresponding proofs and there are also fewer proof strategies implemented in theorem provers for coinduction. In this paper, we investigate formalizations for coinductive proofs of properties on state transition sequences. In particular, we compare two different possibilities for their formalization and show their equivalence. The first of these two formalizations captures the mathematical intuition, while the second can be used more easily in a theorem prover. We have formally verified the equivalence of these criteria in Isabelle/HOL, thus establishing a coalgebraic verification framework. To demonstrate that our verification framework is suitable for the verification of compiler optimizations, we have introduced three different, rather simple transformations that capture typical problems in the verification of optimizing compilers, even for non-terminating source programs.     

Compiler-driven approach for automating nonblocking synchronization in concurrent data abstractions

This paper presents an extended version of our previous work on using compiler technology to automatically convert sequential C++ data abstractions, for example, queues, stacks, maps, and trees, to concurrent lock-free implementations. A key difference between our work and existing research in software transactional memory (STM) is that our compiler-based approach automatically selects the best state-of-the-practice nonblocking synchronization method for the underlying sequential implementation of the data structure. The extended material includes a broader collection of the state-of-the-practice lock-free synchronization techniques, additional formal correctness proofs of the overall integration of the different synchronizations in our system, and a more comprehensive experimental study of the integrated techniques. We evaluate our compiler-generated nonblocking data structures both by using a collection of micro-benchmarks, including the Synchrobench suite, and by using a multi-threaded application Dedup from PARSEC. Our automatically synchronized code attains performance competitive to that of concurrent data structures manually-written by experts and much better performance than heavier-weight support by STM.     

Handling Global Constraints in Compiler Strategy

To achieve high-performance on processors featuring ILP, most compilers apply locally a set of heuristics. This leads to a potentially high-performance on separate code fragments. Unfortunately, most optimizations also increase code size, which may lead to a global net performance loss. In this paper, we propose a Global Constraints-Driven Strategy (GCDS) for guiding code optimization. When using GCDS, the final code optimization decision is taken according to global criteria rather than local criteria. For instance, such criteria might be performance, code size, instruction cache behavior, etc. The performance/code size trade-off is a particularly important problem for embedded systems. We show how GCDS can be used to master code size while optimizing performance.     

The hierarchical task graph as a universal intermediate representation

This paper presents an intermediate program representation called the Hierarchical Task Graph (HTG), and argues that it is not only suitable as the basis for program optimization and code generation, but it fully encapsulates program parallelism at all levels of granularity. As such, the HTG can be used as the basis for a variety of restructuring and optimization techniques, and hence as the target for front-end compilers as well as the input to source and code generators. Our implementation and testing of the HTG in the Parafrase-2 compiler has demonstrated its suitability and versatility as a potentially universal intermediate representation. In addition to encapsulating semantic information, data and control dependences, the HTG provides more information vital to efficient code generation and optimizations related to parallel code generation. In particular, we introduce the notion of precedence between nodes of the structure whose grain size can range from atomic operations to entire subprograms. This work was supported in part by the National Science Foundation under Grant No. NSF-CCR-89-57310, the U. S. Department of Energy under Grant No. DOE-DE-FG02-85ER25001, and a grant from Texas Instruments Inc.     

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF

Software that can produce independently checkable evidence for the correctness of its output has received recent attention for use in certifying compilers and proof-carrying code. CVC (Cooperating Validity Checker) is a proof-producing validity checker for a decidable fragment of first-order logic enriched with background theories. This paper describes how proofs of valid formulas are produced from the decision procedure for linear real arithmetic implemented in CVC. It is shown how extensions to LF which support proof rules schematic in an arity (“elliptical” rules) are very convenient for this purpose.     

Formal proof of integer adders using all-prefix-sums operation

Addition of two binary numbers is a fundamental operation in electronic circuits.Several integer adder architectures have been proposed.Their formal properties are well known,but the proofs are either incomplete or difficult to find.In this paper,we present a formal proof for the correctness of prefix adders.Both sequential and parallel algorithms are formalized and proved.In contrast to previous proofs using higher order functions and rewriting systems,our work is based on first order recursive equations,which are familiar to the computer arithmetic community and are therefore understandable by people working on VLSI circuit design.This study sets up a basis for further work on formal proofs of computer arithmetic algorithms.     

Goto elimination in program algebra

This paper shows that program algebra (PGA) [J.A. Bergstra, M.E. Loots, Program algebra for sequential code, J. Logic Algebraic Programm. 51 (2002) 125–156] offers a mathematical and systematic framework for reasoning about correctness and equivalence of algorithms and transformation rules for goto removal. We study correctness and equivalence for the algorithm proposed by Cooper for goto elimination with additional boolean variables. To remove goto statements without the use of additional variables, we propose a technique to get rid of head-to-head crossings and subsequently employ the results of Peterson et al. and Ramshaw. Finally, we provide formal correctness proofs in the setting of PGA for industrial transformation rules given recently by Veerman for restructuring Cobol programs in real-life applications. We hereby show that PGA can explain goto elimination with mathematical rigor to a larger public.     

The VLISP verified PreScheme compiler

This paper describes a verified compiler for PreScheme, the implementation language for thevlisp run-time system. The compiler and proof were divided into three parts: A transformational front end that translates source text into a core language, a syntax-directed compiler that translates the core language into a combinator-based tree-manipulation language, and a linearizer that translates combinator code into code for an abstract stored-program machine with linear memory for both data and code. This factorization enabled different proof techniques to be used for the different phases of the compiler, and also allowed the generation of good code. Finally, the whole process was made possible by carefully defining the semantics ofvlisp PreScheme rather than just adopting Scheme's. We believe that the architecture of the compiler and its correctness proof can easily be applied to compilers for languages other than PreScheme.This work was supported by Rome Laboratory of the United States Air Force, contract No. F19628-89-C-0001, through the MITRE Corporation, and by NSF and DARPA under NSF grants CCR-9002253 and CCR-9014603. Author's current address: Department of Computer Science and Engineering, Oregon Graduate Institute, P.O. Box 91000, Portland, OR 97291-1000.The work reported here was supported by Rome Laboratory of the United States Air Force, contract No. F19628-89-C-0001. Preparation of this paper was generously supported by The MITRE Corporation.This work was supported by Rome Laboratory of the United States Air Force, contract No. F19628-89-C-0001, through the MITRE Corporation, and by NSF and DARPA under NSF grants CCR-9002253 and CCR-9014603.     

Deriving correctness properties of compiled code

When developing safety-critical software, it is the correctness of the object code that is paramount. However, it is desirable to perform formal verification on the source program. To ensure that correctness results proved about the source program do apply to the object code, the compiler used can be formally verified. However, care must be taken to ensure that the compiler correctness theorem proved is suitable. We have combined a derived programming logic with a verified compiler for a generic subset of the Vista structured assembly language. We show how correctness properties of object code can be formally derived from corresponding correctness properties of the source program which have been proved using the programming logic. Thus we can be sure the results do apply to the object code. The work described has been performed using the HOL system and so is machine-checked.     

基于目标代码大小的指令选择

在传统编译器中,指令选择往往采用动态规划的方法,其目的是优化目标代码性能（减小程序运行时间）。在嵌入式系统中,受到成本的约束,一般只有很有限的存储空间,因此要求目标代码仅可能地小。本文针对具有可变长指令的处理器,以优化代码大小为目的,采用动态规划的方法进行指令选择;相对于优化性能的目标代码,可缩小代码大小的15%
到20%。     

A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract)

We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler implementations, and we point out that much can be done without binders or alpha-conversion. We propose specific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutions in both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.     

Certifying compilers using higher-order theorem provers as certificate checkers

Correct software requires compilers to work correctly. Especially code generation can be an error prone task, since it potentially uses sophisticated algorithms to produce efficient code.     

Improving on Linear Scan Register Allocation

Register allocation is a major step for all compilers. Various register allocation algorithms have been developed over the decades. This work describes a new class of rapid register allocation algorithms and presents experimental data on their behavior. Our research encourages the avoidance of graphing and graph-coloring based on the fact that precise graph-coloring is nondeterministic polynomial time-complete (NP-complete), which is not suitable for real-time tasks. In addition, practical graph-coloring algorithms tend to use polynomial-time heuristics. In dynamic compilation environments, their super linear complexity makes them unsuitable for register allocation and code generation. Existing tools for code generation and register allocation do not completely fulfill the require- ments of fast compilation. Existing approaches either do not allow for the optimization of register allocation to be achieved compre- hensively with a sufficient degree of performance or they require an unjustifiable amount of time and/or resources. Therefore, we pro- pose a new class of register allocation and code generation algorithms that can be performed in linear time. These algorithms are based on the mathematical foundations of abstract interpretation and the computation of the level of abstraction. They have been implemen- ted in a specialized library for just-in-time compilation. The specialization of this library involves the execution of common intermedi- ate language (CIL) and low level virtual machine (LLVM) with a focus on embedded systems.     

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

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

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

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

SPARE: a development environment for program analysis algorithms

A tool that bridges the gap between the theory and practice of program analysis specifications is described. The tool supports a high-level specification language that enables clear and concise expression of analysis algorithms. The denotational nature of the specifications eases the derivation of formal proofs of correctness for the analysis algorithm. SPARE (structured program analysis refinement environment) is based on a hybrid approach that combines the positive aspects of both the operational and the semantics-driven approach. An extended denotational framework is used to provide specifications in a modular fashion. Several extensions to the traditional denotational specification language have been designed to allow analysis algorithms to be expressed in a clear and concise fashion. This extended framework eases the design of analysis algorithms as well as the derivation of correctness proofs. The tool provides automatic implementation for testing purposes     

Trace-based leakage energy optimisations at link time

Energy-aware compilers are becoming increasingly important for embedded systems due to the need to meet a variety of design constraints on time, code size and power consumption. This paper introduces for the first time a trace-based, link-time compiler framework on binaries for embedded systems and evaluates its potential benefits in supporting energy optimisations, especially those that exploit the interaction between compilers and architecture. We present two algorithms for reducing leakage energy in functional units and data caches, respectively. Both algorithms work uniformly at the granularity of optimisation regions that are formed by the hot traces of a program. Our experimental results using Mediabench benchmarks show that good leakage energy savings can be achieved at the cost of some small performance and code size penalties. Furthermore, by varying the granularity of optimisation regions, which is a tunable parameter, embedded application programmers can make the tradeoffs between energy savings and these associated costs.     

Quick compilers using peephole optimization

Abstract machine modelling is a popular technique for developing portable compilers. A compiler can be quickly realized by translating the abstract machine operations to target machine operations. The problem with these compilers is that they trade execution efficiency for portability. Typically, the code emitted by these compilers runs two to three times slower than the code generated by compilers that employ sophisticated code generators. This paper describes a C compiler that uses abstract machine modelling to achieve portability. The emitted target machine code is improved by a simple, classical rule-directed peephole optimizer. Our experiments with this compiler on four machines show that a small number of very general handwritten patterns (under 40) yields code that is comparable to the code from compilers that use more sophisticated code generators. As an added bonus, compilation time on some machines is reduced by 10 to 20 per cent.     

Building certified libraries for PCC: dynamic storage allocation

Proof-carrying code (PCC) allows a code producer to provide to a host a program along with its formal safety proof. The proof attests to a certain safety policy enforced by the code, and can be mechanically checked by the host. While this language-based approach to code certification is very general in principle, existing PCC systems have only focused on programs whose safety proofs can be automatically generated. As a result, many low-level system libraries (e.g., memory management) have not yet been handled. In this paper, we explore a complementary approach in which general properties and program correctness are semi-automatically certified. In particular, we introduce a low-level language, CAP, for building certified programs and present a certified library for dynamic storage allocation.