--- res/PP-compiler.tex 2009/06/29 06:50:40 1.10 +++ res/PP-compiler.tex 2009/06/29 08:07:59 1.11 @@ -164,15 +164,20 @@ Microelectronics). %stress what the significant additions to the scientific knowledge are, %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 -Definitions and measures of non-functional program and system properties (performance, time, space/memory, power, concurrency). -Modeling and representation of these properties alongside with the programming languages semantics -Adapting and enhancing state-of-the-art compilation techniques towards non-functional property and platform awareness -New functional and non-functional 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 +New modeling and representation techniques of non-functional program +and system properties on the programming and intermediate language +levels Definitions and measures of non-functional program and system +properties (performance, time, space/memory, power, concurrency). +Modeling and representation of these properties alongside with the +programming languages semantics Adapting and enhancing +state-of-the-art compilation techniques towards non-functional +property and platform awareness New functional and non-functional +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):} @@ -181,10 +186,10 @@ Techniques for reducing or eliminating t %to also describe and (coarsely) quantify the resources (staff, cost of %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. +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} @@ -219,12 +224,13 @@ hardware/software and pure software tech \paragraph*{WP2 - Verified Compilation} Suitable semantics are necessary which support efficient translation -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. +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 @@ -240,9 +246,47 @@ translation validation for all kinds of frontend and backend optimizations \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} @@ -251,7 +295,7 @@ WCET {\bf Pos} & {\bf Type} & {\bf Description} & {\bf Duration} \\ NN1 & PhD & reliable compilation / simulation & 4 years \\ NN2 & PhD & verified compilation & 4 years \\ -NN3 & PhD & WCET & 4 years \\ +NN3 & PhD & Resource analysis & 4 years \\ \hline \end{tabular} @@ -296,6 +340,7 @@ Techniques for adjusting and decompiling %describe briefly the topic and nature of such a collaboration. (5-10 %lines)} \begin{itemize} +\item Walter Binder, University of Lugano, Switzerland \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