| |
|
| \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} |
| %\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)} |
| 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{} |
| |
|
| %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} |
