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

WP-roberto update

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.1/Presentations/WP2-roberto.tex

    r656 r666  
    512512Implement a {\bf proof-of-concept prototype} of the cost annotating compiler.
    513513
     514{\small
    514515\begin{description}
    515516
     
    529530\item[D2.2] Untrusted cost-annotating $\ocaml$ compiler (T0+12).
    530531
    531 \end{description}
     532\end{description}}
     533
    532534{\small \Red{\NB} This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The
    533535second part will give more details on Task 2.2, discuss Task 2.3 (with demo),
     
    535537
    536538\end{frame}
     539
     540
     541
    537542
    538543
     
    562567
    563568
    564 
    565 
    566 
    567 
    568 
    569 
    570 
    571 
    572 
    573 
    574 
    575 
    576 \begin{frame}
    577 
    578 \frametitle{Motivation}
    579 Resource analysis of programming models should, if we are serious about it,
    580 eventually have an impact on programming practice. Limiting factors include:
    581 
    582 \begin{itemize}
    583 
    584 \item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable.
    585 
    586 \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.
    587 
    588 \item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with.
    589 
    590 \end{itemize}
    591 
    592 \end{frame}
    593 
    594 
    595 \begin{frame}
    596 
    597 \frametitle{$\cerco$ goals and approach}
     569\begin{frame}
     570
     571\frametitle{$\cerco$ goals and approach (again)}
    598572
    599573\begin{itemize}
     
    621595
    622596
    623 \begin{frame}
    624 
    625 \frametitle{Current technology and our challenge}
    626 \begin{itemize}
    627 
    628 
    629 \item Compilation phases are heavily {\bf inspected and tested}
    630 but not formally checked with a proof assistant.
    631 \[
    632 \lustre \arrow \C \arrow \textsc{binary~ code}
    633 \]
    634 \item Binary code must be {\bf annotated} with (uncertified)
    635 information on the number of iterations of loops.
    636 
    637 \item Tools such as \textsc{AbsInt} perform WCET analysis of
    638 {\bf sequences of instructions of binary code}.
     597
     598\begin{frame}
     599
     600\frametitle{More motivation}
     601Resource analysis of programming models should, if we are serious about it,
     602eventually have an impact on programming practice. Limiting factors include:
     603
     604\begin{itemize}
     605
     606\item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable.
     607
     608\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.
     609
     610\item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with.
    639611
    640612\end{itemize}
    641 
    642 \noindent \Red{{\bf Our challenge}}
    643 Lift in a {\em certified way} whathever information we have on the execution
    644 cost of the binary code to an information on the $\C$ source code (a kind
    645 of {\bf decompilation}).
    646613
    647614\end{frame}
     
    669636
    670637
     638\begin{frame}
     639
     640\frametitle{Current technology and our challenge (again)}
     641\begin{itemize}
     642
     643
     644\item Compilation phases are heavily {\bf inspected and tested}
     645but not formally checked with a proof assistant.
     646\[
     647\lustre \arrow \C \arrow \textsc{binary~ code}
     648\]
     649\item Binary code must be {\bf annotated} with (uncertified)
     650information on the number of iterations of loops.
     651
     652\item Tools such as \textsc{AbsInt} perform WCET analysis of
     653{\bf sequences of instructions of binary code}.
     654
     655\end{itemize}
     656
     657\noindent \Red{{\bf Our challenge}}
     658Lift in a {\em certified way} whathever information we have on the execution
     659cost of the binary code to an information on the $\C$ source code (a kind
     660of {\bf decompilation}).
     661
     662\end{frame}
     663
     664
     665
     666
    671667
    672668\begin{frame}
Note: See TracChangeset for help on using the changeset viewer.