![[Replace this image]](Replace_this_image_male.png) |
Roland Lezuo
Institute of Computer Languages E185/1
Argentinierstraße 8 / 185
e-Mail: rlezuo@complang.tuwien.ac.at |
For my master's thesis I developed code generators for the CACAO project. Since October 2010 I am a research assistant.
This research projects aims at implementing a verifing compiler for processors described by a formal specification.
I am (among other things) interested in compilation and optimization techniques, virtual machines and verification.
Today embedded computer systems are often used in safety-critical applications.
A malfunction in such a system (e.g. X-by-wire) often has severe effects, even life-threatening consequences.
Lots of effort is put into certification to assure the correct and safe behavior of safety-critical applications.
Due to the high complexity of modern technical systems, a high-level programming language like C is commonly used to implement their software.
This makes the compiler a critical component in the certification of safety-critical systems.
Even if the source code is fully certified and error-free an erroneous compiler could introduce unintended behavior and hence the certification would be in vain.
This is one motivation of research in compiler correctness, a discipline which develops methods to show that the compiler behaves correctly.
One approach, namely translation validation, formally proves that a single, specific run of the compiler was error-free.
This thesis contributes a framework which allows to apply translation validation from the source code down to its binary representation.
The CASM language, based on the formal method of Abstract State Machines (ASM), has been developed as part of this thesis to specify the semantics of the source language and machine code.
Using the novel technique of direct symbolic execution a first-order logic representation is created as the foundation for the formal proofs.
To exploit the common structure found in problems originating from translation validation problems a specialized prover called vanHelsing has been implemented as part of this thesis.
Its visual proof debugger enables non-domain experts to analyze failing proofs and pinpoint the causing, erroneous translation.
The detailed evaluation shows that CASM is by far the best performing ASM implementation.
It is efficient enough to synthesize ISS and CS tools.
The vanHelsing prover performs much better than other state of the art provers on problems stemming from translation validation.
These efficient tools and the high degree of parallelism in our translation validation framework enable fast validations.
The implemented prototypes for instruction selection, register allocation and VLIW scheduling demonstrate that validation of real-world applications like bzip2 is possible within a few dozen minutes.
Roland Lezuo, ©2014
In this paper we present CASM, a language based on Abstract State Machines (ASM), and its optimizing compiler.
ASM is a well-defined (formal) method based on algebraic concepts.
A distinct feature of ASM is its combination of parallel and sequential execution semantics.
This makes it an excellent choice to formally specify and verify micro-architectures.
We present a compilation scheme and an implementation of a runtime system supporting efficient execution of ASM.
After introducing novel analysis techniques we present optimizations allowing us to eliminate many costly operations.
Benchmark results show that our baseline compiler is 2-3 magnitudes faster than other ASM implementations.
The optimizations further increase the performance of the compiled programs up to 264%.
The achieved performance allows our ASM implementation to be used with industry-size applications.
LCTES'14, ACM New York, NY, USA ©2014
In this paper we present CASM, a general purpose programming language based on abstract state machines (ASMs). We describe the implementation of an interpreter and a compiler for the language. The demand for efficient execution forced us to modify the definition of ASM and we discuss the impact of those changes. A novel feature for ASM based languages is symbolic execution, which we briefly describe. CASM is used for instruction set simulator generation and for semantic description in a compiler verification project. We report on the experience of using the language in those two projects. Finally we position ASM based programming languages as an elegant combination of imperative and functional programming paradigms which may liberate us from the von Neumann style as demanded by John Backus.
ATPS'13, Gesellschaft für Informatik, Bonn ©2013
We present the CASM language, an abstract state machine (ASM) based modeling language originally designed for verifying compiler backends. We demonstrate the expressiveness by describing an instruction set simulator (ISS) for MIPS in approximately 700 lines of code. Further we present a refinement of the models to cycle-accurately describe two implementations of the classic 5-stage MIPS pipeline. Utilizing symbolic execution allows us to prove semantic equivalence of the pipeline implementations and the instruction set description. Finally we compile the models to C++ and provide a small runtime to create a system simulator achieving a performance of approx. 1 MHz in MiBench and SPECInt2000 benchmarks.
Best Poster Award 3rd place in HiPEAC student poster [pdf]
RAPIDO'13, ACM New York, NY, USA ©2013
For safety critical embedded systems the correctness of the processor, toolchain and compiler is an important issue. Translation validation is one approach for compiler verification. A common semantic framework to represent source and target language is needed and Abstract State Machines (ASMs) are a well suited and established method. In this paper we present a method to show correctness of instruction selection by performing fully automated simulation proofs over symbolic execution traces of state transformations using an automated first-order theorem prover. We applied this approach to an industrial-strength compiler and created the ASM models in such a way that we are able to reuse them to create a cycle-accurate simulator. To achieve fast simulation we compile the ASM models to C++ and present the compilation scheme in this paper. Finally we present our preliminary results which indicate that a unified ASM model is sufficient for proving correct instruction selection and generating efficient cycle-accurate simulators.
ABZ'12, Springer-Verlag Berlin, Heidelberg ©2012
The documents listed above are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder. ACM, Springer-Verlag, and IEEE published documents have other restrictions given here, here, and here.