--- res/PP-compiler.tex	2009/06/26 07:34:20	1.4
+++ 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}
@@ -38,9 +38,9 @@ Associated researchers: \emph{}
 %\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)}
@@ -70,7 +70,19 @@ in the Handbook of Signal Processing sys
 instruction set simulator with modelling of energy consumtion is Wattch
 \cite{BrooksTiwariMartonosi00}.
 
-Compiler Verification \cite{Hoare,1328444,1314860}
+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{}
 
@@ -121,23 +133,76 @@ 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
+
+\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,
-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
+WCET
 
 
 \begin{tabular}{llll}
+\\
 \hline
 {\bf Pos} & {\bf Type} & {\bf Description}    & {\bf Duration} \\
 NN1 & PhD & reliable compilation / simulation & 4 years \\
-NN2 & PhD & compiler verificationi            & 4 years \\
+NN2 & PhD & verified compilation              & 4 years \\
 NN3 & PhD & WCET                              & 4 years \\
 \hline
 \end{tabular}