# Changeset 666 for Deliverables

Ignore:
Timestamp:
Mar 10, 2011, 1:20:47 PM (10 years ago)
Message:

WP-roberto update

File:
1 edited

### Legend:

Unmodified
 r656 Implement a {\bf proof-of-concept prototype} of the cost annotating compiler. {\small \begin{description} \item[D2.2] Untrusted cost-annotating $\ocaml$ compiler (T0+12). \end{description} \end{description}} {\small \Red{\NB} This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The second part will give more details on Task 2.2, discuss Task 2.3 (with demo), \end{frame} \begin{frame} \frametitle{Motivation} Resource analysis of programming models should, if we are serious about it, eventually have an impact on programming practice. Limiting factors include: \begin{itemize} \item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable. \item Should focus on software applications that {\bf do care about resource bounds}. E.g., focus on embedded programs rather than on pure functional programs. \item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with. \end{itemize} \end{frame} \begin{frame} \frametitle{$\cerco$ goals and approach} \begin{frame} \frametitle{$\cerco$ goals and approach (again)} \begin{itemize} \begin{frame} \frametitle{Current technology and our challenge} \begin{itemize} \item Compilation phases are heavily {\bf inspected and tested} but not formally checked with a proof assistant. $\lustre \arrow \C \arrow \textsc{binary~ code}$ \item Binary code must be {\bf annotated} with (uncertified) information on the number of iterations of loops. \item Tools such as \textsc{AbsInt} perform WCET analysis of {\bf sequences of instructions of binary code}. \begin{frame} \frametitle{More motivation} Resource analysis of programming models should, if we are serious about it, eventually have an impact on programming practice. Limiting factors include: \begin{itemize} \item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable. \item Should focus on software applications that {\bf do care about resource bounds}. E.g., focus on embedded programs rather than on pure functional programs. \item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with. \end{itemize} \noindent \Red{{\bf Our challenge}} Lift in a {\em certified way} whathever information we have on the execution cost of the binary code to an information on the $\C$ source code (a kind of {\bf decompilation}). \end{frame} \begin{frame} \frametitle{Current technology and our challenge (again)} \begin{itemize} \item Compilation phases are heavily {\bf inspected and tested} but not formally checked with a proof assistant. $\lustre \arrow \C \arrow \textsc{binary~ code}$ \item Binary code must be {\bf annotated} with (uncertified) information on the number of iterations of loops. \item Tools such as \textsc{AbsInt} perform WCET analysis of {\bf sequences of instructions of binary code}. \end{itemize} \noindent \Red{{\bf Our challenge}} Lift in a {\em certified way} whathever information we have on the execution cost of the binary code to an information on the $\C$ source code (a kind of {\bf decompilation}). \end{frame} \begin{frame}