--- res/PP-compiler.tex 2009/06/09 09:59:25 1.1 +++ res/PP-compiler.tex 2009/06/28 16:26:25 1.8 @@ -19,8 +19,8 @@ \title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}} -\author{{\sc Ulrich Schmid}\\ -s@ecs.tuwien.ac.at +\author{{\sc Andreas Krall and Jens Knoop}\\ +\{andi,knoop\}@complang.tuwien.ac.at } \bibliographystyle{unsrt} @@ -28,9 +28,9 @@ s@ecs.tuwien.ac.at \begin{document} \maketitle -PP leader: \emph{Jens Knoop} +PP leader: \emph{Jens Knoop and Andreas Krall} -Associated researchers: \emph{Andreas Krall} +Associated researchers: \emph{} @@ -38,18 +38,51 @@ Associated researchers: \emph{Andreas Kr %\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 compilation, +simulation and specification methods are necessary to optimize for +performance, power, space, concurrency and reliability. \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 -Reliability \cite{LeeShrivastava09} - -ADL \cite{MishraDutt08} +Because of the exponential increase of the number of transistors and +the continuing decrease of the feature sizes of current processors +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 and 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 +processors specifications gives the book of Mishra and Dutt \cite{MishraDutt08}. +A good survey of current instruction set simulators gives our chapter +in the Handbook of Signal Processing systems \cite{BrHoKr09}. A famous +instruction set simulator with modelling of energy consumtion is Wattch +\cite{BrooksTiwariMartonosi00}. + +Compiler Verification + + \cite{Hoare03} + \cite{TristanLeroy09} + \cite{TristanLeroy08} + \cite{Kundu+09} + \cite{Necula00} + \cite{ZaksPnueli08} + \cite{Pnueli98a} + \cite{Pnueli98b} + \cite{GlesnerGoosZimmeermann04} + \cite{GoosZimmermann00} + \cite{BlechPoetzsch07} WCET \cite{} @@ -100,23 +133,77 @@ Techniques for reducing or eliminating t %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. + +\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, -ECC, lockstep etc) and compiler optimizations to exploit/balance reliabiliy features. -Connection with CESAR NN2 +\paragraph*{WP2 - Verified Compilation} -(3) translation verification, specification of semantics of IRs solving -subproblems. NN1 + NN2 +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 - Worst Case Ececution Time Analysis} + +WCET \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 & WCET & 4 years \\ \hline \end{tabular} @@ -161,7 +248,9 @@ Techniques for adjusting and decompiling %describe briefly the topic and nature of such a collaboration. (5-10 %lines)} -To be done. +Aviral Shrivastava, Arizona State University, Tempe, AZ, USA + +Wolf Zimmermann, Universit\"at Halle, Halle, Germany \begin{comment} %Bitte hier die Bibtex-Entries einfuellen, z.B.,