Diff for /res/PP-compiler.tex between versions 1.3 and 1.7

version 1.3, 2009/06/24 14:31:51 version 1.7, 2009/06/28 15:01:57
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 59  either the ECC protected or the unprotec Line 59  either the ECC protected or the unprotec
 balance energy consumption and reliability \cite{LeeShrivastava09a}.  balance energy consumption and reliability \cite{LeeShrivastava09a}.
 The second spills registers to ECC protected memory if the register  The second spills registers to ECC protected memory if the register
 contents are not used for a long period \cite{LeeShrivastava09c}.  contents are not used for a long period \cite{LeeShrivastava09c}.
 There exist complete software solutions which use different forms  There exist complete software solutions which use different forms of
 of code duplications \cite{Reis+05}, which do failure virutalization  code duplications \cite{Oh+02a,Reis+05}, which do failure
 \cite{WapplerMueller08} or which use techniques like control flow  virtualization \cite{WapplerMueller08} or which use techniques like
 checking \cite{}  control flow checking \cite{Oh+02b}. A complete overview of processor
   description languages and generation of compilers and simulators from
 %ADL and Instruction Set Simulators \cite{MishraDutt08}  processors specifications gives the book of Mishra and Dutt \cite{MishraDutt08}.
   A good survey of current instruction set simulators gives our chapter
 Compiler Verification \cite{Hoare,1328444,1314860}  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{}  WCET \cite{}
   
Line 117  Techniques for reducing or eliminating t Line 133  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}
   
 (1) Specification and efficient simulation of reliable processors (partial redundancy,  translation verification, specification of semantics of IRs solving
 ECC, lockstep etc) and compiler optimizations to exploit/balance reliabiliy features.  subproblems.
 Connection with CESAR NN1  
   
 (2) translation verification, specification of semantics of IRs solving  \paragraph*{WP3 - Worst Case Ececution Time Analysis}
 subproblems. NN1 + NN2  
   
 (3) WCET NN3  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 & 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.3  
changed lines
  Added in v.1.7


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