version 1.1, 2009/06/09 09:59:25
|
version 1.10, 2009/06/29 06:50:40
|
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 28 s@ecs.tuwien.ac.at
|
Line 28 s@ecs.tuwien.ac.at
|
\begin{document} |
\begin{document} |
\maketitle |
\maketitle |
|
|
PP leader: \emph{Jens Knoop} |
PP leader: \emph{Jens Knoop and Andreas Krall (beide E185.1)} |
|
|
Associated researchers: \emph{Andreas Krall} |
Associated researchers: \emph{Anton Ertl (E185.1), Bernhard Gramlich (E185.2)} |
|
|
|
|
|
|
Line 38 Associated researchers: \emph{Andreas Kr
|
Line 38 Associated researchers: \emph{Andreas Kr
|
%\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 analysis and |
techniques are necessary to optimize for performance, power, space, |
compilation, simulation, and specification methods are necessary to |
concurrency and reliability. |
support the programmer during application development and maintenance |
|
and to optimize for performance, power, space, concurrency and |
|
reliability during compilation. |
|
%for short, new programming and |
|
%compilation techniques for robust embedded systems development and |
|
%deployment. |
|
|
\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)} |
|
|
Compiler Verification \cite{Hoare,1328444,1314860} |
%Compilation Techniques for Reliability |
|
Because of the exponential increase of the number of transistors and |
Reliability \cite{LeeShrivastava09} |
the continuing decrease of the feature sizes of current processors |
|
\emph{soft errors} mainly caused by energetic particles are becoming an |
ADL \cite{MishraDutt08} |
important design issue for robust embedded systems. Blome et |
|
al.~\cite{Blome+06} observed that a majority of faults that affect the |
WCET \cite{} |
architectural state of a processor come from the register file. Lee |
|
and Shrivastava \cite{LeeShrivastava09a,LeeShrivastava09c} proposed |
|
different solutions to cope with this problem. The first assigns |
|
variables depending on their lifetime to either the ECC protected or |
|
the unprotected part of a register file to balance energy consumption |
|
and reliability \cite{LeeShrivastava09a}. The second spills registers |
|
to ECC protected memory if the register contents are not used for a |
|
long period \cite{LeeShrivastava09c}. There exist complete software |
|
solutions which use different forms of code duplications |
|
\cite{Oh+02a,Reis+05}, which do failure virtualization |
|
\cite{WapplerMueller08} or which use techniques like control flow |
|
checking \cite{Oh+02b}. A complete overview of processor description |
|
languages and generation of compilers and simulators from processor |
|
specifications gives the book of Mishra and Dutt \cite{MishraDutt08}. |
|
A good survey of current instruction set simulators gives our chapter |
|
in the \emph{Handbook of Signal Processing systems} \cite{BrHoKr09}. A |
|
famous instruction set simulator with modelling of energy consumption |
|
is \emph{Wattch} \cite{BrooksTiwariMartonosi00}. |
|
|
|
\paragraph{JK} |
|
Methods for \emph{compiler verification} do exist |
|
\cite{Langmaack97a,Po-lncs124,MMO-lncs1283,Goos:99:verifix,Goos:00:ASM,1328444}. |
|
Most notably are the pioneering approaches of the |
|
\emph{ProCoS} \cite{Langmaack96a} and the \emph{Verifix} |
|
\cite{Goerigk-et-al:CC96} projects, and more recently of |
|
the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There |
|
is also a rich body of work on the related approaches of |
|
\emph{translation validation} |
|
\cite{PSS-tacas98,Ne-pldi00}, \emph{certifying compilation} |
|
\cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and |
|
\emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}. |
|
However, an integratedly verified compiler, |
|
which is optimizing and ensures non-functional program properties such |
|
as on time and space ressources required by the compiled program is |
|
still missing. |
|
|
|
\emph{Worst-case execution time analysis $($WCET$)$} for real-time systems, |
|
which are often safety-critical, is a vibrant field of research in |
|
academia and industry and of fast growing economical relevance, |
|
especially in the avionics and automotive industry. A survey on |
|
state-of-the-art tools and methods for WCET analysis has recently been |
|
given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the |
|
WCET Tool Challenges \cite{Gus:ISoLA2006,Holsti:WCET2008}, however, |
|
demonstrate that all these tools have their own strengths and |
|
limitations. In particular, they all rely to some extent on |
|
user-assistance and thus a \emph{trusted information basis} guiding |
|
the WCET analysis \cite{Prantl:WCET2009}. |
|
|
|
|
|
\paragraph{AK} |
|
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 Verifix 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}. |
|
|
|
|
\subsubsection*{Previous achievements:} |
\subsubsection*{Previous achievements:} |
%\emph{Brief description of your own contributions to the related |
%\emph{Brief description of your own contributions to the related |
%scientific state-of-the art (5-10 lines)} |
%scientific state-of-the art (5-10 lines)} |
Jens Knoop has a long history on work on program analysis with topics |
Jens Knoop's research focuses on proven correct and optimal program |
like partial redundancy elimination or lazy code motion |
analyses and optimizations \cite{Kn-lncs1428}. He is the co-inventor |
\cite{knoop:DSP:2008:1575,conf/cc/XueK06,scholz04}. Recently he |
of the \emph{Lazy Code Motion} |
changed his research focus on worst case execution time analysis |
\cite{KRS-pldi92,KRS-retrolcm04,XueK06}, the code-size sensitive |
\cite{SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661, |
\emph{Sparse Code Motion} \cite{RKS-popl00}, and numerous other |
kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}. He is involved |
program analyses and optimizations including |
in the organization of many compiler conferences and since 2002 program |
\emph{partial dead-code elimination}, \cite{KRS-pldi94}, \emph{partially redundant assignment elimination} \cite{KRS-pldi94}, and \emph{code-size sensitive |
cochair of the yearly workshop on compiler optimization meets verification. |
speculative code motion} \cite{scholz04}, many of which are now part of |
|
state-of-the-art compilers. Recent research focuses on compiler |
|
support for |
|
\emph{worst-case execution time analysis} for safety-critical |
|
real-time embedded systems |
|
\cite{Prantl:WCET2009,SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}. He served on $50+$ |
|
programme committees of international conferences including PLDI, CC, |
|
TACAS, Formal Methods, and Supercomputing. He was the General Chair of |
|
PLDI'02 and ETAPS'06, and is Programme Committee Co-Chair of PACT'10. He is the |
|
iniator and co-founder of the annual workshop series on |
|
\emph{Compiler Optimization meets Compiler Verification} (since 2002), |
|
co-organizer of 4 Dagstuhl seminars, most recently on \emph{Verifying |
|
Optimizing Compilation}, and a member of the European Network of |
|
Excellence HiPEAC. |
|
%, and the IFIP WG 2.4 \emph{Software Implementation Technology}. |
|
|
Andreas Krall does research in the area of architecture description |
Andreas Krall does research in the area of architecture description |
languages and the automatic generation of highly optimizing compilers, |
languages and the automatic generation of highly optimizing compilers, |
Line 100 Techniques for reducing or eliminating t
|
Line 181 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 |
|
|
(1) WCET NN! |
\end{itemize} |
|
|
(2) Specification and efficient simulation of reliable processors (partial redundancy, |
\paragraph*{WP2 - Verified Compilation} |
ECC, lockstep etc) and compiler optimizations to exploit/balance reliabiliy features. |
|
Connection with CESAR NN2 |
|
|
|
(3) translation verification, specification of semantics of IRs solving |
Suitable semantics are necessary which support efficient translation |
subproblems. NN1 + NN2 |
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} |
|
|
|
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 & PostDoc & WCET & 4 years \\ |
NN1 & PhD & reliable compilation / simulation & 4 years \\ |
NN2 & PostDoc & reliable compilation / simulation & 4 years \\ |
NN2 & PhD & verified compilation & 4 years \\ |
|
NN3 & PhD & WCET & 4 years \\ |
\hline |
\hline |
\end{tabular} |
\end{tabular} |
|
|
Line 149 Techniques for adjusting and decompiling
|
Line 284 Techniques for adjusting and decompiling
|
[E182/Puschner]: Links to hard- and software models for time |
[E182/Puschner]: Links to hard- and software models for time |
predictable systems, verification of timing behaviour. |
predictable systems, verification of timing behaviour. |
\item PP Formal Verification for Robustness [E184/Veith]: Links to software |
\item PP Formal Verification for Robustness [E184/Veith]: Links to software |
model checking and testing of code (on source code and intermediate |
model-checking and testing of code (on source code and intermediate |
code levels), support for program analysis and transformation. |
code levels), support for program analysis and transformation. |
\item PP Modeling \& Analysis of Robust Distributed Systems [E182/Schmid]: |
\item PP Modeling \& Analysis of Robust Distributed Systems [E182/Schmid]: |
Links to functional and non-functional system requirements, |
Links to functional and non-functional system requirements, |
Line 160 Techniques for adjusting and decompiling
|
Line 295 Techniques for adjusting and decompiling
|
%\emph{List envisioned international and national collaborations, and |
%\emph{List envisioned international and national collaborations, and |
%describe briefly the topic and nature of such a collaboration. (5-10 |
%describe briefly the topic and nature of such a collaboration. (5-10 |
%lines)} |
%lines)} |
|
\begin{itemize} |
To be done. |
\item Sabine Glesner, TU Berlin, Berlin, Germany |
|
\item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA |
|
\item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany |
|
\end{itemize} |
|
|
\begin{comment} |
\begin{comment} |
%Bitte hier die Bibtex-Entries einfuellen, z.B., |
%Bitte hier die Bibtex-Entries einfuellen, z.B., |