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

Diff for /res/PP-compiler.tex between versions 1.13 and 1.14

version 1.13, 2009/06/29 09:28:41 version 1.14, 2009/06/29 09:40:11
Line 82  Most notably are the pioneering approach Line 82  Most notably are the pioneering approach
 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{Pnueli98a,Pnueli98b,Ne-pldi00,\cite{ZaksPnueli08}},   \cite{Pnueli98a,Pnueli98b,Ne-pldi00,ZaksPnueli08}, 
 \emph{certifying compilation}   \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, which is optimizing and  However, an integratedly verified compiler, which is optimizing and
 ensures non-functional program properties such as on time and space  ensures non-functional program properties such as on time and space
 ressources required by the compiled program is still  resources required by the compiled program is still
 missing. Complementary to these approaches are approaches focusing on  missing. Complementary to these approaches are approaches focusing on
 frameworks for verifying compiler optimizations  frameworks for verifying compiler optimizations
 \cite{781156,1040335,Kundu+09} or the verification of specific  \cite{781156,1040335,Kundu+09} or the verification of specific
 compiler optizations, such as the \emph{Lazy Code Motion}  compiler optimizations, such as the \emph{Lazy Code Motion}
 \cite{TristanLeroy09} or instruction scheduling  \cite{TristanLeroy09} or instruction scheduling
 \cite{TristanLeroy08}. By far more ambitious and a grand challenge for  \cite{TristanLeroy08}. By far more ambitious and a grand challenge for
 computing research is Tony Hoare's vision of a \emph{verifying  computing research is Tony Hoare's vision of a \emph{verifying
 compiler} which proves properties of the translated program  compiler} which proves properties of the translated program
 \cite{Hoare03}.  \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,  \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 289  programmer during source code developmen Line 289  programmer during source code developmen
 providing hints on resource consumption and (2) the compiler to  providing hints on resource consumption and (2) the compiler to
 optimize for resource consumption. In our previous work we focused on  optimize for resource consumption. In our previous work we focused on
 compiler support for  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   \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 we will extend this research towards 
 other quantitive aspects of resource consumption, especially storage  other quantitive aspects of resource consumption, especially storage
 usage, towards these two global objectives, using the programming  usage, towards these two global objectives, using the programming
 environment used there as testbed for implementation  environment used there as testbed for implementation
Line 326  verification, implementation, and applic Line 326  verification, implementation, and applic
 {\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 & Resource analysis                 & 4 years \\  NN3 & PhD & resource analysis                 & 4 years \\
 \hline  \hline
 \end{tabular}  \end{tabular}
   
Line 364  safer and robust. Line 364  safer and robust.
       Links to specification and modeling of timing properties, to execution        Links to specification and modeling of timing properties, to execution
       models, hardware and software models.        models, hardware and software models.
 \item PP Composition and Predictability in RES Architectures  \item PP Composition and Predictability in RES Architectures
       [E182/Puschner]: Links to hard- and software models for time        [E182.1/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.2/Schmid]:
       Links to functional and non-functional system requirements,        Links to functional and non-functional system requirements,
       distribution, concurrency.        distribution, concurrency.
 \end{itemize}  \end{itemize}
Removed from v.1.13  
changed lines
  Added in v.1.14

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