--- res/PP-compiler.tex 2009/06/29 06:50:40 1.10 +++ 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 Andreas Krall and Jens Knoop}\\ -\{andi,knoop\}@complang.tuwien.ac.at +\author{{\sc Jens Knoop and Andreas Krall}\\ +\{knoop,andi\}@complang.tuwien.ac.at } \bibliographystyle{unsrt} @@ -30,9 +29,8 @@ PP leader: \emph{Jens Knoop and Andreas Krall (beide E185.1)} -Associated researchers: \emph{Anton Ertl (E185.1), Bernhard Gramlich (E185.2)} - - +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)} @@ -75,26 +73,32 @@ in the \emph{Handbook of Signal Processi famous instruction set simulator with modelling of energy consumption is \emph{Wattch} \cite{BrooksTiwariMartonosi00}. -\paragraph{JK} 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} projects, and more recently of +\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{PSS-tacas98,Ne-pldi00}, \emph{certifying compilation} +\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 ressources required by the compiled program is -still missing. - -\emph{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, +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 @@ -105,45 +109,53 @@ user-assistance and thus a \emph{trusted 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}. +%\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}. + + \subsubsection*{Previous achievements:} %\emph{Brief description of your own contributions to the related %scientific state-of-the art (5-10 lines)} 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}, the code-size sensitive -\emph{Sparse Code Motion} \cite{RKS-popl00}, and numerous other -program analyses and optimizations including -\emph{partial dead-code elimination}, \cite{KRS-pldi94}, \emph{partially redundant assignment elimination} \cite{KRS-pldi94}, and \emph{code-size sensitive -speculative code motion} \cite{scholz04}, many of which are now part of -state-of-the-art compilers. Recent research focuses on compiler -support for +\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. +\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 @@ -152,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):} @@ -180,11 +215,10 @@ 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: compilation and -simulation techniques for reliabiltiy, verified compilation and worst case -execution time analysis. +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} @@ -219,12 +253,13 @@ hardware/software and pure software tech \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. +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 @@ -240,9 +275,48 @@ translation validation for all kinds of frontend and backend optimizations \end{itemize} -\paragraph*{WP3 - Worst Case Ececution Time Analysis} +\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}. + +\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. + -WCET \begin{tabular}{llll} @@ -251,26 +325,34 @@ WCET {\bf Pos} & {\bf Type} & {\bf Description} & {\bf Duration} \\ NN1 & PhD & reliable compilation / simulation & 4 years \\ NN2 & PhD & verified compilation & 4 years \\ -NN3 & PhD & WCET & 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 @@ -281,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 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} @@ -296,9 +378,11 @@ Techniques for adjusting and decompiling %describe briefly the topic and nature of such a collaboration. (5-10 %lines)} \begin{itemize} -\item Sabine Glesner, TU Berlin, Berlin, Germany -\item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA +\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}