[BACK]Return to PP-compiler.tex CVS log [TXT] [DIR] Up to [gforth] / res

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

version 1.10, 2009/06/29 06:50:40 version 1.12, 2009/06/29 08:36:40
Line 164  Microelectronics). Line 164  Microelectronics).
 %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):}
Line 181  Techniques for reducing or eliminating t Line 186  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.  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}
   
Line 219  hardware/software and pure software tech Line 224  hardware/software and pure software tech
 \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
Line 240  translation validation for all kinds of Line 246  translation validation for all kinds of
       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}
Line 251  WCET Line 295  WCET
 {\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}
   
   
 \subsubsection*{Goals (last 4 years):}  \subsubsection*{Goals (last 4 years):}
 %\emph{Brief description of the   %\emph{Brief description of the 
 %eesearch topics to be addressed during the last 4 years. Make sure to   %research topics to be addressed during the last 4 years. Make sure to 
 %explicitly stress what the significant additions to the scientific   %explicitly stress what the significant additions to the scientific 
 %knowledge are, and why they are important. (20-30 lines)}  %knowledge are, and why they are important. (20-30 lines)}
   
 New programming languages and compilers for RESs  In the last 4 years we will extend the research of the first years into
 Non-functional properties and requirements as first-class language and compiler citizens  some additional directions like
 New compilation techniques enabling a uniform and integrated approach  
 for ensuring functional and non-functional program and system requirements  \begin{itemize}
 Replacing trust by proof  \item New programming languages and compilers for RESs
 Certifying compilation, proof-carrying code, translation validation  \item Non-functional properties and requirements as first-class language and
 Verified compilers, verifying compilation for RESs        compiler citizens
 Making legacy applications fit to and available on RESs  \item New compilation techniques enabling a uniform and integrated approach
 Techniques for adjusting and decompiling legacy applications        for ensuring functional and non-functional program and system requirements
   \item Verified compilers, proof-carrying code, verifying compilation for RESs
   \item Making legacy applications fit to and available on RESs
   \item Techniques for adjusting and decompiling legacy applications
   \end{itemize}
   
   Application of the results of this research reduces the cost of the
   development of reliable and correct embedded systems and makes them
   safer and robust.
   
 \subsubsection*{Collaboration with other PPs:}  \subsubsection*{Collaboration with other PPs:}
 %\emph{List the PPs you are expecting to collaborate with, and describe briefly  %\emph{List the PPs you are expecting to collaborate with, and describe briefly
Line 296  Techniques for adjusting and decompiling Line 348  Techniques for adjusting and decompiling
 %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 Sabine Glesner, TU Berlin, Berlin, Germany  \item Walter Binder, University of Lugano, Switzerland (resource analysis)
 \item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA  \item Sabine Glesner, TU Berlin, Berlin, Germany (verified compilation)
   \item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA (reliable compilation)
 \item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany  \item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany
         (verified compilation)
 \end{itemize}  \end{itemize}
   
 \begin{comment}  \begin{comment}
Removed from v.1.10  
changed lines
  Added in v.1.12

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