--- res/PP-compiler.tex 2009/06/09 09:59:25 1.1 +++ res/PP-compiler.tex 2009/06/29 18:13:13 1.16 @@ -3,7 +3,6 @@ \usepackage{url} %\usepackage{times} \usepackage{comment} - \pagestyle{plain} \setlength{\textwidth}{16truecm} \setlength{\textheight}{24truecm} @@ -19,8 +18,8 @@ \title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}} -\author{{\sc Ulrich Schmid}\\ -s@ecs.tuwien.ac.at +\author{{\sc Jens Knoop and Andreas Krall}\\ +\{knoop,andi\}@complang.tuwien.ac.at } \bibliographystyle{unsrt} @@ -28,42 +27,136 @@ s@ecs.tuwien.ac.at \begin{document} \maketitle -PP leader: \emph{Jens Knoop} - -Associated researchers: \emph{Andreas Krall} - +PP leader: \emph{Jens Knoop and Andreas Krall (beide E185.1)} +Associated researchers: \emph{Anton Ertl (E185.1), Bernhard Gramlich (E185.2),}\\ +\phantom{Associated researchers: } \ \ \ \ \emph{Franz Puntigam (E185.1)} \subsubsection*{Motivation:} %\emph{Informal description of the purpose of the PP (3-5 lines)} Every embedded system consists of software which is written in a high level language, compiled to machine language and executed on a -processor. For robust embedded systems new verified compilation -techniques are necessary to optimize for performance, power, space, -concurrency and reliability. +processor. For robust embedded systems new verified analysis and +compilation, simulation, and specification methods are necessary to +support the programmer during application development and maintenance +and to optimize for performance, power, space, concurrency and +reliability during compilation. +%for short, new programming and +%compilation techniques for robust embedded systems development and +%deployment. \subsubsection*{State of the art and related work:} %\emph{Briefly describe the scientific state of the art (20-30 lines)} -Compiler Verification \cite{Hoare,1328444,1314860} +%Compilation Techniques for Reliability +Because of the exponential increase of the number of transistors and +the continuing decrease of the feature sizes of current processors +\emph{soft errors} mainly caused by energetic particles are becoming an +important design issue for robust embedded systems. Blome et +al.~\cite{Blome+06} observed that a majority of faults that affect the +architectural state of a processor come from the register file. Lee +and Shrivastava \cite{LeeShrivastava09a,LeeShrivastava09c} proposed +different solutions to cope with this problem. The first assigns +variables depending on their lifetime to either the ECC protected or +the unprotected part of a register file to balance energy consumption +and reliability \cite{LeeShrivastava09a}. The second spills registers +to ECC protected memory if the register contents are not used for a +long period \cite{LeeShrivastava09c}. There exist complete software +solutions which use different forms of code duplications +\cite{Oh+02a,Reis+05}, which do failure virtualization +\cite{WapplerMueller08} or which use techniques like control flow +checking \cite{Oh+02b}. A complete overview of processor description +languages and generation of compilers and simulators from processor +specifications gives the book of Mishra and Dutt \cite{MishraDutt08}. +A good survey of current instruction set simulators gives our chapter +in the \emph{Handbook of Signal Processing systems} \cite{BrHoKr09}. A +famous instruction set simulator with modelling of energy consumption +is \emph{Wattch} \cite{BrooksTiwariMartonosi00}. + +Methods for \emph{compiler verification} do exist +\cite{Langmaack97a,Po-lncs124,MMO-lncs1283,Goos:99:verifix,Goos:00:ASM,1328444}. +Most notably are the pioneering approaches of the +\emph{ProCoS} \cite{Langmaack96a} and the \emph{Verifix} +\cite{Goerigk-et-al:CC96,GlesnerGoosZimmeermann04,GoosZimmermann00} projects, and more recently of +the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There +is also a rich body of work on the related approaches of +\emph{translation validation} +\cite{Pnueli98a,Pnueli98b,Ne-pldi00,ZaksPnueli08}, +\emph{certifying compilation} +\cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and +\emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}. +However, an integratedly verified compiler, which is optimizing and +ensures non-functional program properties such as on time and space +resources required by the compiled program is still +missing. Complementary to these approaches are approaches focusing on +frameworks for verifying compiler optimizations +\cite{781156,1040335,Kundu+09} or the verification of specific +compiler optimizations, such as the \emph{Lazy Code Motion} +\cite{TristanLeroy09} or instruction scheduling +\cite{TristanLeroy08}. By far more ambitious and a grand challenge for +computing research is Tony Hoare's vision of a \emph{verifying +compiler} which proves properties of the translated program +\cite{Hoare03}. + +\emph{Resource analysis}, especially worst-case execution time analysis $($WCET$)$ for real-time systems, which are often safety-critical, is a vibrant field of research in academia and industry and of fast growing economical relevance, +especially in the avionics and automotive industry. A survey on +state-of-the-art tools and methods for WCET analysis has recently been +given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the +WCET Tool Challenges \cite{Gus:ISoLA2006,Holsti:WCET2008}, however, +demonstrate that all these tools have their own strengths and +limitations. In particular, they all rely to some extent on +user-assistance and thus a \emph{trusted information basis} guiding +the WCET analysis \cite{Prantl:WCET2009}. + + +%\paragraph{AK} +%Three aspects of program and compiler correctness exist. The verifying +%compiler proves properties of the translated program and is a grand challenge +%for computing research \cite{Hoare03}. A certified compiler like Verifix is +%proven once to do semantically equivalent optimizations and translations +%\cite{GlesnerGoosZimmeermann04,GoosZimmermann00}. Translation validation proves +%at every compiler run that the translation is correct and was introduced by +%Pnueli et al.\ \cite{Pnueli98a,Pnueli98b} and Necula \cite{Necula00}. Until now +%some optimizations have been verified, recently lazy code motion +%\cite{TristanLeroy09}, instruction scheduling \cite{TristanLeroy08}, or the whole +%code generation phase \cite{BlechPoetzsch07}. Another research direction is the +%construction of general frameworks for validation \cite{ZaksPnueli08} or +%generalizations like parameterized equivalence checking \cite{Kundu+09}. + -Reliability \cite{LeeShrivastava09} -ADL \cite{MishraDutt08} - -WCET \cite{} \subsubsection*{Previous achievements:} %\emph{Brief description of your own contributions to the related %scientific state-of-the art (5-10 lines)} -Jens Knoop has a long history on work on program analysis with topics -like partial redundancy elimination or lazy code motion -\cite{knoop:DSP:2008:1575,conf/cc/XueK06,scholz04}. Recently he -changed his research focus on worst case execution time analysis -\cite{SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661, -kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}. He is involved -in the organization of many compiler conferences and since 2002 program -cochair of the yearly workshop on compiler optimization meets verification. +Jens Knoop's research focuses on proven correct and optimal program +analyses and optimizations \cite{Kn-lncs1428}. He is the co-inventor +of the \emph{Lazy Code Motion} +\cite{KRS-pldi92,KRS-retrolcm04,XueK06}, and numerous other program +analyses and optimizations including +\emph{partial dead-code elimination} \cite{KRS-pldi94} and +\emph{partially redundant assignment elimination} \cite{KRS-pldi94}, +which are now part of state-of-the-art compilers. Regarding the +present PP, particularly important are the achievements on +resource-aware program analyses and optimizations including the +code-size sensitive \emph{Sparse Code Motion} \cite{RKS-popl00}, and its +counterpart for \emph{Speculative Code Motion} \cite{scholz04}. +Recent research in the frame of the FWF project CoSTA and the EU FP7 +project ALL-TIMES focuses on compiler support for +\emph{worst-case execution time analysis} for safety-critical +real-time embedded systems +\cite{Prantl:WCET2009,SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}. + +% He served on $50+$ +%programme committees of international conferences including PLDI, CC, +%TACAS, Formal Methods, and Supercomputing. He was the General Chair of +%PLDI'02 and ETAPS'06, and is Programme Committee Co-Chair of PACT'10. He is the +%iniator and co-founder of the annual workshop series on +%\emph{Compiler Optimization meets Compiler Verification} (since 2002), +%co-organizer of 4 Dagstuhl seminars, most recently on \emph{Verifying +%Optimizing Compilation}, and a member of the European Network of +%Excellence HiPEAC. +%, and the IFIP WG 2.4 \emph{Software Implementation Technology}. Andreas Krall does research in the area of architecture description languages and the automatic generation of highly optimizing compilers, @@ -71,27 +164,50 @@ efficient instruction set simulators and specification of a processor \cite{BrFeKrRi09,BrEbKr07,FaKrHo07, FarKrStBrand06,Krall+04micro}. An important focus is on optimization techniques for embedded processors -\cite{EbBrSchKrWiKa08,MeKr07,PrKrHo06,HiKr03} as he lead the Christian +\cite{EbBrSchKrWiKa08,MeKr07,PrKrHo06,HiKr03} as he leads the Christian Doppler research laboratory {\em compilation techniques for embedded processors} with partners from industry (Infineon, OnDemand Microelectronics). +The PP is designed to synergetically combine the complementary +expertises of Jens Knoop on verified resource-aware program analyses +and optimizations and of Andreas Krall on compilation techniques for +embedded processors. Their complementary expertise is essential for +the PP. + \subsubsection*{Goals (first 4 years):} %\emph{Description of the research %topics to be addressed during the first 4 years. Make sure to explicitly %stress what the significant additions to the scientific knowledge are, %and why they are important. (30-40 lines)} +The goals of the first 4 years are as follows: -New modeling and representation techniques of non-functional program and system properties on the programming and intermediate language levels -Definitions and measures of non-functional program and system properties (performance, time, space/memory, power, concurrency). -Modeling and representation of these properties alongside with the programming languages semantics -Adapting and enhancing state-of-the-art compilation techniques towards non-functional property and platform awareness -New functional and non-functional property and platform-aware compilation techniques -Analyses for non-functional program and system properties -Functional and non-functional property and platform-aware code generation techniques -Enabling validation and verification throughout the compilation process -Techniques for reducing or eliminating trusted code, annotation, etc., bases +\begin{itemize} +\item New modeling and representation techniques of non-functional + program and system properties on the programming and + intermediate language levels +\item Definitions and measures of non-functional program and system + properties (performance, time, space/memory, power, + concurrency). +\item Modeling and representation of these properties alongside + with the programming languages semantics +\item Adapting and enhancing state-of-the-art compilation techniques + towards non-functional property and platform awareness +\item New functional and non-functional property and platform-aware + compilation techniques +\item Analyses for non-functional program and system properties +\item Functional and non-functional property and platform-aware + code generation techniques +\item Enabling validation and verification throughout the compilation + process +\item Techniques for reducing or eliminating trusted code, + annotation, etc., bases +\end{itemize} +These goals are essential for making the development and the +compilation of embedded systems software more reliable and +robust. Moreover, they are the basis for the second 4 years extension +of the project. \subsubsection*{Work Plan (first 4 years):} @@ -99,43 +215,144 @@ Techniques for reducing or eliminating t %you intend to conduct the actual research during the first 4 years. Be sure %to also describe and (coarsely) quantify the resources (staff, cost of %special equipment) required for this work in a table. (20-30 lines)} +Compilation techniques for robust embedded systems comprise different +areas. Therefore, the project is divided into three work packages: +\emph{compilation and simulation techniques for reliability}, \emph{verified +compilation} and \emph{resource analysis}. + +\paragraph*{WP1 - Compilation and Simulation Techniques for Reliability} + +In previous work we have developed a processor description language +with a very concise semantics from where we automatically generate +optimized compilers \cite{BrEbKr07} and high efficient instruction set +simulators \cite{BrFeKrRi09}. This environment we use as testbed for +our compiler optimizations for embedded processors +\cite{EbBrSchKrWiKa08,PrKrHo06,MeKr07}. We will extend this +environment to do research on compilation and simulation techniques to +enhance the reliability of processor/memory systems by mixed +hardware/software and pure software techniques. + +\begin{itemize} +\item Specification method to specify an energy consumption model in + a processor specification. +\item Specification method for redundancy and error correction in the + processor specification +\item Specification method for fault injection and fault checking in + the processor specification +\item Generation of optimized instruction set simulators from the + extended processor specification +\item Generation of optimizing compilers from the extended processor + specification +\item Research into new compiler optimizations to increase reliability by + pure software solutions, mixed hardware/software solutions and + balancing performance, code space, reliability and energy consumption +\item Research of correctness proofs and validation of the new optimizations + +\end{itemize} + +\paragraph*{WP2 - Verified Compilation} +Suitable semantics are necessary which support efficient translation +validation or support easy verification of a compiler. We will +research into different semantics and into mappings between the +semantics of our processor description language \cite{BrEbKr07} and a +compiler backend semantics, intermediate representation semantics +(compatible to LLVM) and source language semantics. The main research +will be on verification and translation validation for all kinds of +compiler optimizations. +\begin{itemize} +\item Evaluate different semantics regarding suitability for compiler + verification and translation validation, eventually develop new + semantics +\item Develop a translator for an automatic mapping from our processor + description language into verification semantics +\item Develop a validation system from the intermediate representation + (LLVM) to the processor semantics +\item Develop a validation system from the source language (C) to the + intermediate representation (LLVM) +\item Research into verification and translation validation for different + frontend and backend optimizations +\end{itemize} + +\paragraph*{WP3 - Resource Analysis} +For safety-critical real-time embedded sytems resource consumption +measured in terms of a quantitative aspect of a program execution such +as execution time, storage use, and power consumption belongs rather +to the functional properties of an application rather its +non-functional ones. Formal guarantees on resource consumption are +thus essential and mandatory to ensure the robustness of such +systems. This requires new and usually more complex but more +expressive program analyses and transformations to support the (1) +programmer during source code development by early and automatically +providing hints on resource consumption and (2) the compiler to +optimize for resource consumption. In our previous work we focused on +compiler support for +\emph{worst-case execution time analysis $($WCET$)$} \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. Based on this work we will extend this research towards +other quantitive aspects of resource consumption, especially storage +usage, towards these two global objectives, using the programming +environment used there as testbed for implementation +\cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. -(1) WCET NN! +\begin{itemize} +\item Research into new program analyses for providing high-quality + bounds on resourse consumption which are useful for both the + application programmer and the compiler. +\item Research new program analyses and static optimizations + to optimize for resource consumption and to help complying to + possibly given limits. +\item Research suitable abstraction levels of interfaces and modes + of interaction between fully automatic program analysis and + verification methods and semi-automatic ones relying on + user-assistance because of undecidability issues +\item Research the synergies and the trade-off between fully + automatic program analysis and verification methods and + semi-automatic ones utilizing user-assistance on high-quality + resource bounds and the computational costs to compute them. +\item Research simulation and profiling methods to assess the + quality of resource consumption analyses and to support + correctness and security checks at run-time. +\end{itemize} +Overall, this WP will contribute to the design, foundations, +verification, implementation, and application of resource analyses. -(2) Specification and efficient simulation of reliable processors (partial redundancy, -ECC, lockstep etc) and compiler optimizations to exploit/balance reliabiliy features. -Connection with CESAR NN2 -(3) translation verification, specification of semantics of IRs solving -subproblems. NN1 + NN2 \begin{tabular}{llll} +\\ \hline -{\bf Pos} & {\bf Type} & {\bf Description} & {\bf Duration} \\ -NN1 & PostDoc & WCET & 4 years \\ -NN2 & PostDoc & reliable compilation / simulation & 4 years \\ +{\bf Pos} & {\bf Type} & {\bf Description} & {\bf Duration} \\ +NN1 & PhD & reliable compilation / simulation & 4 years \\ +NN2 & PhD & verified compilation & 4 years \\ +NN3 & PhD & resource analysis & 4 years \\ \hline \end{tabular} \subsubsection*{Goals (last 4 years):} %\emph{Brief description of the -%eesearch topics to be addressed during the last 4 years. Make sure to +%research topics to be addressed during the last 4 years. Make sure to %explicitly stress what the significant additions to the scientific %knowledge are, and why they are important. (20-30 lines)} -New programming languages and compilers for RESs -Non-functional properties and requirements as first-class language and compiler citizens -New compilation techniques enabling a uniform and integrated approach -for ensuring functional and non-functional program and system requirements -Replacing trust by proof -Certifying compilation, proof-carrying code, translation validation -Verified compilers, verifying compilation for RESs -Making legacy applications fit to and available on RESs -Techniques for adjusting and decompiling legacy applications +In the last 4 years we will extend the research of the first years into +some additional directions like + +\begin{itemize} +\item New programming languages and compilers for RESs +\item Non-functional properties and requirements as first-class language and + compiler citizens +\item New compilation techniques enabling a uniform and integrated approach + for ensuring functional and non-functional program and system requirements +\item Verified compilers, proof-carrying code, verifying compilation for RESs +\item Making legacy applications fit to and available on RESs +\item Techniques for adjusting and decompiling legacy applications +\end{itemize} + +Application of the results of this research reduces the cost of the +development of reliable and correct embedded systems and makes them +safer and robust. \subsubsection*{Collaboration with other PPs:} %\emph{List the PPs you are expecting to collaborate with, and describe briefly @@ -146,12 +363,12 @@ Techniques for adjusting and decompiling Links to specification and modeling of timing properties, to execution models, hardware and software models. \item PP Composition and Predictability in RES Architectures - [E182/Puschner]: Links to hard- and software models for time + [E182.1/Puschner]: Links to hard- and software models for time predictable systems, verification of timing behaviour. \item PP Formal Verification for Robustness [E184/Veith]: Links to software - model checking and testing of code (on source code and intermediate + model-checking and testing of code (on source code and intermediate code levels), support for program analysis and transformation. -\item PP Modeling \& Analysis of Robust Distributed Systems [E182/Schmid]: +\item PP Modeling \& Analysis of Robust Distributed Systems [E182.2/Schmid]: Links to functional and non-functional system requirements, distribution, concurrency. \end{itemize} @@ -160,8 +377,13 @@ Techniques for adjusting and decompiling %\emph{List envisioned international and national collaborations, and %describe briefly the topic and nature of such a collaboration. (5-10 %lines)} - -To be done. +\begin{itemize} +\item Walter Binder, University of Lugano, Switzerland (resource analysis) +\item Sabine Glesner, TU Berlin, Berlin, Germany (verified compilation) +\item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA (reliable compilation) +\item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany + (verified compilation) +\end{itemize} \begin{comment} %Bitte hier die Bibtex-Entries einfuellen, z.B.,