|
version 1.12, 2009/06/29 08:36:40
|
version 1.13, 2009/06/29 09:28:41
|
|
Line 3
|
Line 3
|
| \usepackage{url} |
\usepackage{url} |
| %\usepackage{times} |
%\usepackage{times} |
| \usepackage{comment} |
\usepackage{comment} |
| |
|
| \pagestyle{plain} |
\pagestyle{plain} |
| \setlength{\textwidth}{16truecm} |
\setlength{\textwidth}{16truecm} |
| \setlength{\textheight}{24truecm} |
\setlength{\textheight}{24truecm} |
|
Line 19
|
Line 18
|
| |
|
| \title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}} |
\title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}} |
| |
|
| \author{{\sc Andreas Krall and Jens Knoop}\\ |
\author{{\sc Jens Knoop and Andreas Krall}\\ |
| \{andi,knoop\}@complang.tuwien.ac.at |
\{knoop,andi\}@complang.tuwien.ac.at |
| } |
} |
| |
|
| \bibliographystyle{unsrt} |
\bibliographystyle{unsrt} |
|
Line 75 in the \emph{Handbook of Signal Processi
|
Line 74 in the \emph{Handbook of Signal Processi
|
| famous instruction set simulator with modelling of energy consumption |
famous instruction set simulator with modelling of energy consumption |
| is \emph{Wattch} \cite{BrooksTiwariMartonosi00}. |
is \emph{Wattch} \cite{BrooksTiwariMartonosi00}. |
| |
|
| \paragraph{JK} |
|
| Methods for \emph{compiler verification} do exist |
Methods for \emph{compiler verification} do exist |
| \cite{Langmaack97a,Po-lncs124,MMO-lncs1283,Goos:99:verifix,Goos:00:ASM,1328444}. |
\cite{Langmaack97a,Po-lncs124,MMO-lncs1283,Goos:99:verifix,Goos:00:ASM,1328444}. |
| Most notably are the pioneering approaches of the |
Most notably are the pioneering approaches of the |
| \emph{ProCoS} \cite{Langmaack96a} and the \emph{Verifix} |
\emph{ProCoS} \cite{Langmaack96a} and the \emph{Verifix} |
| \cite{Goerigk-et-al:CC96} projects, and more recently of |
\cite{Goerigk-et-al:CC96,GlesnerGoosZimmeermann04,GoosZimmermann00} projects, and more recently of |
| the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There |
the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There |
| is also a rich body of work on the related approaches of |
is also a rich body of work on the related approaches of |
| \emph{translation validation} |
\emph{translation validation} |
| \cite{PSS-tacas98,Ne-pldi00}, \emph{certifying compilation} |
\cite{Pnueli98a,Pnueli98b,Ne-pldi00,\cite{ZaksPnueli08}}, |
| |
\emph{certifying compilation} |
| \cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and |
\cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and |
| \emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}. |
\emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}. |
| However, an integratedly verified compiler, |
However, an integratedly verified compiler, which is optimizing and |
| which is optimizing and ensures non-functional program properties such |
ensures non-functional program properties such as on time and space |
| as on time and space ressources required by the compiled program is |
ressources required by the compiled program is still |
| still missing. |
missing. Complementary to these approaches are approaches focusing on |
| |
frameworks for verifying compiler optimizations |
| \emph{Worst-case execution time analysis $($WCET$)$} for real-time systems, |
\cite{781156,1040335,Kundu+09} or the verification of specific |
| which are often safety-critical, is a vibrant field of research in |
compiler optizations, such as the \emph{Lazy Code Motion} |
| academia and industry and of fast growing economical relevance, |
\cite{TristanLeroy09} or instruction scheduling |
| |
\cite{TristanLeroy08}. By far more ambitious and a grand challenge for |
| |
computing research is Tony Hoare's vision of a \emph{verifying |
| |
compiler} which proves properties of the translated program |
| |
\cite{Hoare03}. |
| |
|
| |
\emph{Resource analysis}, especially 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 |
especially in the avionics and automotive industry. A survey on |
| state-of-the-art tools and methods for WCET analysis has recently been |
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 |
given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the |
|
Line 105 user-assistance and thus a \emph{trusted
|
Line 110 user-assistance and thus a \emph{trusted
|
| the WCET analysis \cite{Prantl:WCET2009}. |
the WCET analysis \cite{Prantl:WCET2009}. |
| |
|
| |
|
| \paragraph{AK} |
%\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 Verifix 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 |
| Pnueli et al.\ \cite{Pnueli98a,Pnueli98b} and Necula \cite{Necula00}. Until now |
%Pnueli et al.\ \cite{Pnueli98a,Pnueli98b} and Necula \cite{Necula00}. Until now |
| some optimizations have been verified, recently lazy code motion |
%some optimizations have been verified, recently lazy code motion |
| \cite{TristanLeroy09}, instruction scheduling \cite{TristanLeroy08}, or the whole |
%\cite{TristanLeroy09}, instruction scheduling \cite{TristanLeroy08}, or the whole |
| code generation phase \cite{BlechPoetzsch07}. Another research direction is the |
%code generation phase \cite{BlechPoetzsch07}. Another research direction is the |
| construction of general frameworks for validation \cite{ZaksPnueli08} or |
%construction of general frameworks for validation \cite{ZaksPnueli08} or |
| generalizations like parameterized equivalence checking \cite{Kundu+09}. |
%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's research focuses on proven correct and optimal program |
Jens Knoop's research focuses on proven correct and optimal program |
| analyses and optimizations \cite{Kn-lncs1428}. He is the co-inventor |
analyses and optimizations \cite{Kn-lncs1428}. He is the co-inventor |
| of the \emph{Lazy Code Motion} |
of the \emph{Lazy Code Motion} |
| \cite{KRS-pldi92,KRS-retrolcm04,XueK06}, the code-size sensitive |
\cite{KRS-pldi92,KRS-retrolcm04,XueK06}, and numerous other program |
| \emph{Sparse Code Motion} \cite{RKS-popl00}, and numerous other |
analyses and optimizations including |
| program analyses and optimizations including |
\emph{partial dead-code elimination} \cite{KRS-pldi94} and |
| \emph{partial dead-code elimination}, \cite{KRS-pldi94}, \emph{partially redundant assignment elimination} \cite{KRS-pldi94}, and \emph{code-size sensitive |
\emph{partially redundant assignment elimination} \cite{KRS-pldi94}, |
| speculative code motion} \cite{scholz04}, many of which are now part of |
which are now part of state-of-the-art compilers. Regarding the |
| state-of-the-art compilers. Recent research focuses on compiler |
present PP, particularly important are the achievements on |
| support for |
resource-aware program analyes and optimizations including the |
| |
code-size sensitive \emph{Sparse Code Motion} \cite{RKS-popl00}, and its |
| |
counterpart for \emph{Speculative Code Motion} \cite{scholz04}. |
| |
Recent research in the frame of the FWF project CoSTA and the EU FP7 |
| |
project ALL-TIMES focuses on compiler support for |
| \emph{worst-case execution time analysis} for safety-critical |
\emph{worst-case execution time analysis} for safety-critical |
| real-time embedded systems |
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+$ |
\cite{Prantl:WCET2009,SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}. |
| programme committees of international conferences including PLDI, CC, |
|
| TACAS, Formal Methods, and Supercomputing. He was the General Chair of |
% He served on $50+$ |
| PLDI'02 and ETAPS'06, and is Programme Committee Co-Chair of PACT'10. He is the |
%programme committees of international conferences including PLDI, CC, |
| iniator and co-founder of the annual workshop series on |
%TACAS, Formal Methods, and Supercomputing. He was the General Chair of |
| \emph{Compiler Optimization meets Compiler Verification} (since 2002), |
%PLDI'02 and ETAPS'06, and is Programme Committee Co-Chair of PACT'10. He is the |
| co-organizer of 4 Dagstuhl seminars, most recently on \emph{Verifying |
%iniator and co-founder of the annual workshop series on |
| Optimizing Compilation}, and a member of the European Network of |
%\emph{Compiler Optimization meets Compiler Verification} (since 2002), |
| Excellence HiPEAC. |
%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}. |
%, 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 |
|
Line 152 efficient instruction set simulators and
|
Line 165 efficient instruction set simulators and
|
| specification of a processor \cite{BrFeKrRi09,BrEbKr07,FaKrHo07, |
specification of a processor \cite{BrFeKrRi09,BrEbKr07,FaKrHo07, |
| FarKrStBrand06,Krall+04micro}. An important focus is on optimization |
FarKrStBrand06,Krall+04micro}. An important focus is on optimization |
| techniques for embedded processors |
techniques for embedded processors |
| \cite{EbBrSchKrWiKa08,MeKr07,PrKrHo06,HiKr03} as he lead the Christian |
\cite{EbBrSchKrWiKa08,MeKr07,PrKrHo06,HiKr03} as he leads the Christian |
| Doppler research laboratory {\em compilation techniques for embedded |
Doppler research laboratory {\em compilation techniques for embedded |
| processors} with partners from industry (Infineon, OnDemand |
processors} with partners from industry (Infineon, OnDemand |
| Microelectronics). |
Microelectronics). |
| |
|
| |
The PP is designed to exploit the synergies of the complementary |
| |
expertise of Jens Knoop on resource-aware program analyses and |
| |
optimizations and their verification and of Andreas Krall on |
| |
compilation techniques for embedded processors. Their complementary |
| |
expertise is essential for the PP. |
| |
|
| |
|
| \subsubsection*{Goals (first 4 years):} |
\subsubsection*{Goals (first 4 years):} |
| %\emph{Description of the research |
%\emph{Description of the research |
| %topics to be addressed during the first 4 years. Make sure to explicitly |
%topics to be addressed during the first 4 years. Make sure to explicitly |
| %stress what the significant additions to the scientific knowledge are, |
%stress what the significant additions to the scientific knowledge are, |
| %and why they are important. (30-40 lines)} |
%and why they are important. (30-40 lines)} |
| |
The goals of the first 4 years are as follows: |
| |
|
| New modeling and representation techniques of non-functional program |
\begin{itemize} |
| and system properties on the programming and intermediate language |
\item New modeling and representation techniques of non-functional |
| levels Definitions and measures of non-functional program and system |
program and system properties on the programming and |
| properties (performance, time, space/memory, power, concurrency). |
intermediate language levels |
| Modeling and representation of these properties alongside with the |
\item Definitions and measures of non-functional program and system |
| programming languages semantics Adapting and enhancing |
properties (performance, time, space/memory, power, |
| state-of-the-art compilation techniques towards non-functional |
concurrency). |
| property and platform awareness New functional and non-functional |
\item Modeling and representation of these properties alongside |
| property and platform-aware compilation techniques Analyses for |
with the programming languages semantics |
| non-functional program and system properties Functional and |
\item Adapting and enhancing state-of-the-art compilation techniques |
| non-functional property and platform-aware code generation techniques |
towards non-functional property and platform awareness |
| Enabling validation and verification throughout the compilation |
\item New functional and non-functional property and platform-aware |
| process Techniques for reducing or eliminating trusted code, |
compilation techniques |
| annotation, etc., bases |
\item Analyses for non-functional program and system properties |
| |
\item Functional and non-functional property and platform-aware |
| |
code generation techniques |
| |
\item Enabling validation and verification throughout the compilation |
| |
process |
| |
\item Techniques for reducing or eliminating trusted code, |
| |
annotation, etc., bases |
| |
\end{itemize} |
| |
These goals are essential for making the development and the |
| |
compilation of embedded systems software more reliable and |
| |
robust. Moreover, they are the basis for the second 4 years extension |
| |
of the project. |
| |
|
| |
|
| \subsubsection*{Work Plan (first 4 years):} |
\subsubsection*{Work Plan (first 4 years):} |
|
Line 185 annotation, etc., bases
|
Line 216 annotation, etc., bases
|
| %you intend to conduct the actual research during the first 4 years. Be sure |
%you intend to conduct the actual research during the first 4 years. Be sure |
| %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 |
Compilation techniques for robust embedded systems comprise different |
| areas. Therefore, the project is divided into three work packages: |
areas. Therefore, the project is divided into three work packages: |
| compilation and simulation techniques for reliabiltiy, verified |
\emph{compilation and simulation techniques for reliability}, \emph{verified |
| compilation and worst case execution time analysis. |
compilation} and \emph{resource analysis}. |
| |
|
| \paragraph*{WP1 - Compilation and Simulation Techniques for Reliability} |
\paragraph*{WP1 - Compilation and Simulation Techniques for Reliability} |
| |
|
|
Line 281 environment used there as testbed for im
|
Line 311 environment used there as testbed for im
|
| semi-automatic ones utilizing user-assistance on high-quality |
semi-automatic ones utilizing user-assistance on high-quality |
| resource bounds and the computational costs to compute them. |
resource bounds and the computational costs to compute them. |
| \item Research simulation and profiling methods to assess the |
\item Research simulation and profiling methods to assess the |
| quality of resource consumption analyses. |
quality of resource consumption analyses and to support |
| |
correctness and security checks at run-time. |
| \end{itemize} |
\end{itemize} |
| Overall, this WP will contribute to the design, foundations, |
Overall, this WP will contribute to the design, foundations, |
| verification, implementation, and application of resource analyses. |
verification, implementation, and application of resource analyses. |
![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to PP-compiler.tex CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [gforth] / res