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

Diff for /res/PP-compiler.tex between versions 1.4 and 1.9

version 1.4, 2009/06/26 07:34:20 version 1.9, 2009/06/28 16:53:25
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 38  Associated researchers: \emph{} Line 38  Associated researchers: \emph{}
 %\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 compilation,
 techniques are necessary to optimize for performance, power, space,  simulation and specification methods are necessary to optimize for
 concurrency and reliability.  performance, power, space, concurrency and reliability.
   
 \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)}
Line 70  in the Handbook of Signal Processing sys Line 70  in the Handbook of Signal Processing sys
 instruction set simulator with modelling of energy consumtion is Wattch  instruction set simulator with modelling of energy consumtion is Wattch
 \cite{BrooksTiwariMartonosi00}.  \cite{BrooksTiwariMartonosi00}.
   
 Compiler Verification \cite{Hoare,1328444,1314860}  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 Verfix 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}.
    
   
   
 WCET \cite{}  WCET \cite{}
   
Line 121  Techniques for reducing or eliminating t Line 134  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
   
   \end{itemize}
   
   \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.
   
   \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}
   
 (1) Specification and efficient simulation of reliable processors (partial redundancy,  WCET
 ECC, lockstep etc) and compiler optimizations to exploit/balance reliabiliy features.  
 Connection with CESAR NN1  
   
 (2) translation verification, specification of semantics of IRs solving  
 subproblems. NN1 + NN2  
   
 (3) WCET NN3  
   
   
 \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 & PhD & reliable compilation / simulation & 4 years \\  NN1 & PhD & reliable compilation / simulation & 4 years \\
 NN2 & PhD & compiler verificationi            & 4 years \\  NN2 & PhD & verified compilation              & 4 years \\
 NN3 & PhD & WCET                              & 4 years \\  NN3 & PhD & WCET                              & 4 years \\
 \hline  \hline
 \end{tabular}  \end{tabular}
Removed from v.1.4  
changed lines
  Added in v.1.9

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