| %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)} |
| |
|
| New modeling and representation techniques of non-functional program and system properties on the programming and intermediate language levels |
New modeling and representation techniques of non-functional program |
| Definitions and measures of non-functional program and system properties (performance, time, space/memory, power, concurrency). |
and system properties on the programming and intermediate language |
| Modeling and representation of these properties alongside with the programming languages semantics |
levels Definitions and measures of non-functional program and system |
| Adapting and enhancing state-of-the-art compilation techniques towards non-functional property and platform awareness |
properties (performance, time, space/memory, power, concurrency). |
| New functional and non-functional property and platform-aware compilation techniques |
Modeling and representation of these properties alongside with the |
| Analyses for non-functional program and system properties |
programming languages semantics Adapting and enhancing |
| Functional and non-functional property and platform-aware code generation techniques |
state-of-the-art compilation techniques towards non-functional |
| Enabling validation and verification throughout the compilation process |
property and platform awareness New functional and non-functional |
| Techniques for reducing or eliminating trusted code, annotation, etc., bases |
property and platform-aware compilation techniques Analyses for |
| |
non-functional program and system properties Functional and |
| |
non-functional property and platform-aware code generation techniques |
| |
Enabling validation and verification throughout the compilation |
| |
process Techniques for reducing or eliminating trusted code, |
| |
annotation, etc., bases |
| |
|
| |
|
| \subsubsection*{Work Plan (first 4 years):} |
\subsubsection*{Work Plan (first 4 years):} |
| %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. |
Compilation techniques for robust embedded systems comprise different |
| Therefore, the project is divided into three work packages: compilation and |
areas. Therefore, the project is divided into three work packages: |
| simulation techniques for reliabiltiy, verified compilation and worst case |
compilation and simulation techniques for reliabiltiy, verified |
| execution time analysis. |
compilation and worst case execution time analysis. |
| |
|
| \paragraph*{WP1 - Compilation and Simulation Techniques for Reliability} |
\paragraph*{WP1 - Compilation and Simulation Techniques for Reliability} |
| |
|
| \paragraph*{WP2 - Verified Compilation} |
\paragraph*{WP2 - Verified Compilation} |
| |
|
| Suitable semantics are necessary which support efficient translation |
Suitable semantics are necessary which support efficient translation |
| validation or support easy verification of a compiler. We will research |
validation or support easy verification of a compiler. We will |
| into different semantics and into mappings between the semantics of our |
research into different semantics and into mappings between the |
| processor description language \cite{BrEbKr07} and a compiler backend |
semantics of our processor description language \cite{BrEbKr07} and a |
| semantics, intermediate representation semantics (compatible to LLVM) and |
compiler backend semantics, intermediate representation semantics |
| source language semantics. The main research will be on verification and |
(compatible to LLVM) and source language semantics. The main research |
| translation validation for all kinds of compiler optimizations. |
will be on verification and translation validation for all kinds of |
| |
compiler optimizations. |
| |
|
| \begin{itemize} |
\begin{itemize} |
| \item Evaluate different semantics regarding suitability for compiler |
\item Evaluate different semantics regarding suitability for compiler |
| frontend and backend optimizations |
frontend and backend optimizations |
| \end{itemize} |
\end{itemize} |
| |
|
| \paragraph*{WP3 - Worst Case Ececution Time Analysis} |
\paragraph*{WP3 - Resource Analysis} |
| |
For safety-critical real-time embedded sytems resource consumption |
| |
measured in terms of a quantitative aspect of a program execution such |
| |
as execution time, storage use, and power consumption belongs rather |
| |
to the functional properties of an application rather its |
| |
non-functional ones. Formal guarantees on resource consumption are |
| |
thus essential and mandatory to ensure the robustness of such |
| |
systems. This requires new and usually more complex but more |
| |
expressive program analyses and transformations to support the (1) |
| |
programmer during source code development by early and automatically |
| |
providing hints on resource consumption and (2) the compiler to |
| |
optimize for resource consumption. In our previous work we focused on |
| |
compiler support for |
| |
\emph{worst-case execution time analysis $($WCET$)$} \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. Based on this work and expertise we will extend this research towards |
| |
other quantitive aspects of resource consumption, especially storage |
| |
usage, towards these two global objectives, using the programming |
| |
environment used there as testbed for implementation |
| |
\cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. |
| |
|
| |
\begin{itemize} |
| |
\item Research into new program analyses for providing high-quality |
| |
bounds on resourse consumption which are useful for both the |
| |
application programmer and the compiler. |
| |
\item Research new program analyses and static optimizations |
| |
to optimize for resource consumption and to help complying to |
| |
possibly given limits. |
| |
\item Research suitable abstraction levels of interfaces and modes |
| |
of interaction between fully automatic program analysis and |
| |
verification methods and semi-automatic ones relying on |
| |
user-assistance because of undecidability issues |
| |
\item Research the synergies and the trade-off between fully |
| |
automatic program analysis and verification methods and |
| |
semi-automatic ones utilizing user-assistance on high-quality |
| |
resource bounds and the computational costs to compute them. |
| |
\item Research simulation and profiling methods to assess the |
| |
quality of resource consumption analyses. |
| |
\end{itemize} |
| |
Overall, this WP will contribute to the design, foundations, |
| |
verification, implementation, and application of resource analyses. |
| |
|
| |
|
| WCET |
|
| |
|
| |
|
| \begin{tabular}{llll} |
\begin{tabular}{llll} |
| {\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 & verified compilation & 4 years \\ |
NN2 & PhD & verified compilation & 4 years \\ |
| NN3 & PhD & WCET & 4 years \\ |
NN3 & PhD & Resource analysis & 4 years \\ |
| \hline |
\hline |
| \end{tabular} |
\end{tabular} |
| |
|
| %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} |
\begin{itemize} |
| |
\item Walter Binder, University of Lugano, Switzerland |
| \item Sabine Glesner, TU Berlin, Berlin, Germany |
\item Sabine Glesner, TU Berlin, Berlin, Germany |
| \item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA |
\item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA |
| \item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany |
\item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany |
