--- res/PP-compiler.tex 2009/06/29 08:07:59 1.11 +++ 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,32 +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):} @@ -185,11 +215,10 @@ annotation, etc., bases %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. +\emph{compilation and simulation techniques for reliability}, \emph{verified +compilation} and \emph{resource analysis}. \paragraph*{WP1 - Compilation and Simulation Techniques for Reliability} @@ -259,7 +288,7 @@ programmer during source code developmen 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 and expertise we will extend this research towards +\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 @@ -281,7 +310,8 @@ environment used there as testbed for im 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. + 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. @@ -295,26 +325,34 @@ verification, implementation, and applic {\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 \\ +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 @@ -325,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} @@ -340,10 +378,11 @@ Techniques for adjusting and decompiling %describe briefly the topic and nature of such a collaboration. (5-10 %lines)} \begin{itemize} -\item Walter Binder, University of Lugano, Switzerland -\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}