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} |