### Diff for /res/PP-compiler.tex between versions 1.9 and 1.10

version 1.9, 2009/06/28 16:53:25 version 1.10, 2009/06/29 06:50:40
Line 28 Line 28
\begin{document}  \begin{document}
\maketitle  \maketitle

PP leader: \emph{Jens Knoop and Andreas Krall}  PP leader: \emph{Jens Knoop and Andreas Krall (beide E185.1)}

Associated researchers: \emph{}  Associated researchers: \emph{Anton Ertl (E185.1), Bernhard Gramlich (E185.2)}

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 analysis and
simulation and specification methods are necessary to optimize for  compilation, simulation, and specification methods are necessary to
performance, power, space, 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)}

%Compilation Techniques for Reliability  %Compilation Techniques for Reliability

Because of the exponential increase of the number of transistors and  Because of the exponential increase of the number of transistors and
the continuing decrease of the feature sizes of current processors  the continuing decrease of the feature sizes of current processors
soft errors mainly caused by energetic particles are becoming an  \emph{soft errors} mainly caused by energetic particles are becoming an
important design issue for robust embedded systems. Blome et  important design issue for robust embedded systems. Blome et
al.~\cite{Blome+06} observed that a majority of faults that affect the  al.~\cite{Blome+06} observed that a majority of faults that affect the
architectural state of a processor come from the register file. Lee  architectural state of a processor come from the register file. Lee
and Shrivastava and proposed different solutions to cope with this  and Shrivastava \cite{LeeShrivastava09a,LeeShrivastava09c} proposed
problem. The first assigns variables depending on their lifetime to  different solutions to cope with this problem. The first assigns
either the ECC protected or the unprotected part of a register file to  variables depending on their lifetime to either the ECC protected or
balance energy consumption and reliability \cite{LeeShrivastava09a}.  the unprotected part of a register file to balance energy consumption
The second spills registers to ECC protected memory if the register  and reliability \cite{LeeShrivastava09a}.  The second spills registers
contents are not used for a long period \cite{LeeShrivastava09c}.  to ECC protected memory if the register contents are not used for a
There exist complete software solutions which use different forms of  long period \cite{LeeShrivastava09c}.  There exist complete software
code duplications \cite{Oh+02a,Reis+05}, which do failure  solutions which use different forms of code duplications
virtualization \cite{WapplerMueller08} or which use techniques like  \cite{Oh+02a,Reis+05}, which do failure virtualization
control flow checking \cite{Oh+02b}. A complete overview of processor  \cite{WapplerMueller08} or which use techniques like control flow
description languages and generation of compilers and simulators from  checking \cite{Oh+02b}. A complete overview of processor description
processors specifications gives the book of Mishra and Dutt \cite{MishraDutt08}.  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  A good survey of current instruction set simulators gives our chapter
in the Handbook of Signal Processing systems \cite{BrHoKr09}. A famous  in the \emph{Handbook of Signal Processing systems} \cite{BrHoKr09}. A
instruction set simulator with modelling of energy consumtion is Wattch  famous instruction set simulator with modelling of energy consumption
\cite{BrooksTiwariMartonosi00}.  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  Three aspects of program and compiler correctness exist. The verifying
compiler proves properties of the translated program and is a grand challenge  compiler proves properties of the translated program and is a grand challenge
for computing research \cite{Hoare03}. A certified compiler like Verfix is  for computing research \cite{Hoare03}. A certified compiler like Verifix is
proven once to do semantically equivalent optimizations and translations  proven once to do semantically equivalent optimizations and translations
\cite{GlesnerGoosZimmeermann04,GoosZimmermann00}. Translation validation proves  \cite{GlesnerGoosZimmeermann04,GoosZimmermann00}. Translation validation proves
at every compiler run that the translation is correct and was introduced by  at every compiler run that the translation is correct and was introduced by
Line 84  construction of general frameworks for v Line 120  construction of general frameworks for v
generalizations like parameterized equivalence checking \cite{Kundu+09}.  generalizations like parameterized equivalence checking \cite{Kundu+09}.

WCET \cite{}

\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 237  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 248  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}
Aviral Shrivastava, Arizona State University, Tempe, AZ, USA  \item Sabine Glesner, TU Berlin, Berlin, Germany
\item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA
Wolf Zimmermann, Universit\"at Halle, Halle, Germany  \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.,

 Removed from v.1.9 changed lines Added in v.1.10

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