[BACK]Return to PP-compiler.tex CVS log [TXT] [DIR] Up to [gforth] / res

Diff for /res/PP-compiler.tex between versions 1.1 and 1.10

version 1.1, 2009/06/09 09:59:25 version 1.10, 2009/06/29 06:50:40
Line 19 Line 19
   
 \title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}}  \title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}}
   
 \author{{\sc Ulrich Schmid}\\  \author{{\sc Andreas Krall and Jens Knoop}\\
 s@ecs.tuwien.ac.at  \{andi,knoop\}@complang.tuwien.ac.at
 }  }
   
 \bibliographystyle{unsrt}  \bibliographystyle{unsrt}
Line 28  s@ecs.tuwien.ac.at Line 28  s@ecs.tuwien.ac.at
 \begin{document}  \begin{document}
 \maketitle  \maketitle
   
 PP leader: \emph{Jens Knoop}  PP leader: \emph{Jens Knoop and Andreas Krall (beide E185.1)}
   
 Associated researchers: \emph{Andreas Krall}  Associated researchers: \emph{Anton Ertl (E185.1), Bernhard Gramlich (E185.2)}
   
   
   
Line 38  Associated researchers: \emph{Andreas Kr Line 38  Associated researchers: \emph{Andreas Kr
 %\emph{Informal description of the purpose of the PP (3-5 lines)}  %\emph{Informal description of the purpose of the PP (3-5 lines)}
 Every embedded system consists of software which is written in a high  Every embedded system consists of software which is written in a high
 level language, compiled to machine language and executed on a  level language, compiled to machine language and executed on a
 processor. For robust embedded systems new verified compilation  processor. For robust embedded systems new verified analysis and
 techniques are necessary to optimize for performance, power, space,  compilation, simulation, and specification methods are necessary to
 concurrency and reliability.  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:}   \subsubsection*{State of the art and related work:} 
 %\emph{Briefly describe the scientific state of the art (20-30 lines)}  %\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
 Reliability \cite{LeeShrivastava09}  the continuing decrease of the feature sizes of current processors
   \emph{soft errors} mainly caused by energetic particles are becoming an
 ADL \cite{MishraDutt08}  important design issue for robust embedded systems. Blome et
   al.~\cite{Blome+06} observed that a majority of faults that affect the
 WCET \cite{}  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}.
   
   \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 
   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{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,
   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}.
    
   
 \subsubsection*{Previous achievements:}   \subsubsection*{Previous achievements:} 
 %\emph{Brief description of your own contributions to the related  %\emph{Brief description of your own contributions to the related
 %scientific state-of-the art (5-10 lines)}  %scientific state-of-the art (5-10 lines)}
 Jens Knoop has a long history on work on program analysis with topics  Jens Knoop's research focuses on proven correct and optimal program
 like partial redundancy elimination or lazy code motion  analyses and optimizations \cite{Kn-lncs1428}. He is the co-inventor
 \cite{knoop:DSP:2008:1575,conf/cc/XueK06,scholz04}. Recently he  of the \emph{Lazy Code Motion}
 changed his research focus on worst case execution time analysis   \cite{KRS-pldi92,KRS-retrolcm04,XueK06}, the code-size sensitive
 \cite{SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,  \emph{Sparse Code Motion} \cite{RKS-popl00}, and numerous other
 kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}. He is involved  program analyses and optimizations including
 in the organization of many compiler conferences and since 2002 program  \emph{partial dead-code elimination}, \cite{KRS-pldi94}, \emph{partially redundant assignment elimination} \cite{KRS-pldi94}, and \emph{code-size sensitive 
 cochair of the yearly workshop on compiler optimization meets verification.  speculative code motion} \cite{scholz04}, many of which are now part of
   state-of-the-art compilers. Recent research 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  Andreas Krall does research in the area of architecture description
 languages and the automatic generation of highly optimizing compilers,  languages and the automatic generation of highly optimizing compilers,
Line 100  Techniques for reducing or eliminating t Line 181  Techniques for reducing or eliminating t
 %to also describe and (coarsely) quantify the resources (staff, cost of   %to also describe and (coarsely) quantify the resources (staff, cost of 
 %special equipment) required for this work in a table. (20-30 lines)}  %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.
   
   \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
   
 (1) WCET NN!  \end{itemize}
   
 (2) Specification and efficient simulation of reliable processors (partial redundancy,  \paragraph*{WP2 - Verified Compilation}
 ECC, lockstep etc) and compiler optimizations to exploit/balance reliabiliy features.  
 Connection with CESAR NN2  
   
 (3) translation verification, specification of semantics of IRs solving  Suitable semantics are necessary which support efficient translation
 subproblems. NN1 + NN2  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 - Worst Case Ececution Time Analysis}
   
   WCET
   
   
 \begin{tabular}{llll}  \begin{tabular}{llll}
   \\
 \hline  \hline
 {\bf Pos} & {\bf Type} & {\bf Description}        & {\bf Duration} \\  {\bf Pos} & {\bf Type} & {\bf Description}    & {\bf Duration} \\
 NN1 & PostDoc & WCET                              & 4 years \\  NN1 & PhD & reliable compilation / simulation & 4 years \\
 NN2 & PostDoc & reliable compilation / simulation & 4 years \\  NN2 & PhD & verified compilation              & 4 years \\
   NN3 & PhD & WCET                              & 4 years \\
 \hline  \hline
 \end{tabular}  \end{tabular}
   
Line 149  Techniques for adjusting and decompiling Line 284  Techniques for adjusting and decompiling
       [E182/Puschner]: Links to hard- and software models for time        [E182/Puschner]: Links to hard- and software models for time
       predictable systems, verification of timing behaviour.        predictable systems, verification of timing behaviour.
 \item PP Formal Verification for Robustness [E184/Veith]: Links to software  \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.        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/Schmid]:
       Links to functional and non-functional system requirements,        Links to functional and non-functional system requirements,
Line 160  Techniques for adjusting and decompiling Line 295  Techniques for adjusting and decompiling
 %\emph{List envisioned international  and national collaborations, and  %\emph{List envisioned international  and national collaborations, and
 %describe briefly the topic and nature  of such a collaboration. (5-10  %describe briefly the topic and nature  of such a collaboration. (5-10
 %lines)}  %lines)}
   \begin{itemize}
 To be done.  \item Sabine Glesner, TU Berlin, Berlin, Germany
   \item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA
   \item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany
   \end{itemize}
   
 \begin{comment}  \begin{comment}
 %Bitte hier die Bibtex-Entries  einfuellen, z.B.,  %Bitte hier die Bibtex-Entries  einfuellen, z.B.,
Removed from v.1.1  
changed lines
  Added in v.1.10

FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>