--- res/PP-compiler.tex 2009/06/29 08:36:40 1.12 +++ res/PP-compiler.tex 2009/06/29 09:28:41 1.13 @@ -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} @@ -75,26 +74,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,\cite{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 +ressources 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 optizations, 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 +110,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 analyes 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 +165,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 exploit the synergies of the complementary +expertise of Jens Knoop on resource-aware program analyses and +optimizations and their verification 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 +216,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} @@ -281,7 +311,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.