Ignore:
Timestamp:
Mar 4, 2011, 5:38:45 PM (9 years ago)
Author:
amadio
Message:

wp2 revised

File:
1 edited

Legend:

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

    r626 r633  
    495495\institute{Universit\'e Paris Diderot}
    496496
    497 \title{CerCo Work Package 2: Untrusted Compiler Prototype (part 1)}
     497\title{$\cerco$ Work Package 2: Untrusted Compiler Prototype (part 1)}
    498498\date{March 11, 2011}
    499499
     
    530530
    531531\end{description}
    532 {\small This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The
     532{\small \Red{\NB} This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The
    533533second part will give more details on Task 2.2, discuss Task 2.3 (with demo),
    534534and  provide some perspectives on Task 2.4 and WP5.}
     
    539539\begin{frame}
    540540
    541 \frametitle{People involved at Paris site}
    542 
    543 
     541\frametitle{People involved at UPD site}
     542
     543
     544{\small
    544545\begin{tabular}{|c|c|c|}
    545546
    546547\hline
    547548{\bf Name}           &{\bf Status} &{\bf Rough Allocated Time} \\\hline
    548 Roberto Amadio &Professor &1 day/week \\
    549 Yann R\'egis-Gianas &Assistant Professor &1 day/week \\
    550 Nicolas Ayache      &Post-doc      &full time, 11 months \\
    551 Ronan Saillard      &Internship+PhD &full time, 8 months \\
    552 Kayvan Memarian     &Internship   &1.5 days/week, 4 months \\ \hline
    553 \end{tabular}
     549Roberto \textsc{Amadio} &Professor &1 day/week \\
     550Yann \textsc{R\'egis-Gianas} &Assistant Professor &1 day/week \\
     551Nicolas \textsc{Ayache}      &Post-doc      &full time, 11 months \\
     552Ronan \textsc{Saillard}      &Internship+PhD &full time, 8 months \\
     553Kayvan \textsc{Memarian}     &Internship   &1.5 days/week, 4 months \\ \hline
     554\end{tabular}}
     555
     556
     557~\\~\\
     558\Red{{\bf NB}} Internships are very important: dissemination, speed up development,
     559explore side paths, preliminary training towards research (PhD),$\ldots$
    554560
    555561\end{frame}
     
    589595\begin{frame}
    590596
    591 \frametitle{CerCo goals and approach}
     597\frametitle{$\cerco$ goals and approach}
    592598
    593599\begin{itemize}
     
    596602given  piece of code on a given processor with a given compiler.
    597603
    598 \item Target {\bf C programs}, and in particular the kind of C
     604\item Target {\bf $\C$ programs}, and in particular the kind of $\C$
    599605programs produced for embedded applications
    600 (such as those generated by the SCADE compiler).
     606(such as those generated by the $\scade$ compiler).
    601607
    602608\item {\bf Reflect the cost information} obtained at the machine level
    603 back into the C source code.
     609back into the $\C$ source code.
    604610
    605611\item {\bf Extract synthetic bounds} by reasoning on
    606 the annotated C  programs (for which several general purpose tools now exist).
     612the annotated $\C$  programs (for which several general purpose tools now exist).
    607613
    608614\end{itemize}
    609615
    610 \NB Technically, this can be seen as a refinement of ongoing work on {\bf compiler certification}   
    611 (see, e.g., CompCert project).
     616\Red{\NB} Technically, this can be seen as a refinement of ongoing work on {\bf compiler certification}   
     617(see, e.g., $\compcert$ project).
    612618
    613619\end{frame}
     
    624630but not formally checked with a proof assistant.
    625631\[
    626 \textsc{Lustre} \arrow \textsc{C} \arrow \textsc{binary~ code}
     632\lustre \arrow \C \arrow \textsc{binary~ code}
    627633\]
    628634\item Binary code must be {\bf annotated} with (uncertified)
     
    634640\end{itemize}
    635641
    636 \noindent{\bf Our challenge}
    637 Lift in a certified way whathever information we have on the execution
    638 cost of the binary code to an information on the C source code (a kind
     642\noindent \Red{{\bf Our challenge}}
     643Lift in a {\em certified way} whathever information we have on the execution
     644cost of the binary code to an information on the $\C$ source code (a kind
    639645of {\bf decompilation}).
    640646
     
    647653\frametitle{A potential connection}
    648654Could use this work as a {\bf platform} to experiment with
    649 `implicit complexity programming languages'.
     655\Blu{{\em implicit complexity programming languages}}.
    650656
    651657{\small
    652658\begin{enumerate}
    653659
    654 \item Write a program in your preferred implicit-complexity programming language.
    655 \item Compile it to C.
    656 \item CerCo compiles C to machine code and provides precise and certified information on execution time of C code.
     660\item Write a program in your preferred implicit complexity programming language.
     661\item Compile it to $\C$.
     662\item $\cerco$ compiles $\C$ to machine code and provides precise and certified information on execution time of $\C$ code.
    657663\item Use your implicit complexity analysis to produce automatically a synthetic bound on the resources used by the program.
    658 \item If you want to push this further, try to lift the assertions about the C code to assertions on your source program.
     664\item If you want to push this further, try to lift the assertions about the $\C$ code to assertions on your source program.
    659665\end{enumerate}}
    660666\end{frame}
     
    702708\item
    703709Starting from the annotated source program apply standard tools
    704 to reason about C programs in order to {\bf extract synthetic bounds}.
     710to reason about $\C$ programs in order to {\bf extract synthetic bounds}.
    705711
    706712\end{itemize}
     
    818824{\small
    819825\[
    820 \infer{(\w{An}_{i}(S),s[0/\w{cost}])\eval s'[c/\w{cost}]}
    821 {\begin{array}{c}
    822 (\w{An}_{i+1}(\cl{C}_{i,i+1}(S)),s[0/\w{cost}]) \eval s'[d/\w{cost}]  \\
    823 d \leq c
    824 \end{array}}
     826\begin{array}{lc}
     827\mbox{`Predicted' cost} &(\w{An}_{i}(S),s[0/\w{cost}])\eval s'[c/\w{cost}]\\\hline
     828\mbox{`Real' cost}       &(\w{An}_{i+1}(\cl{C}_{i,i+1}(S)),s[0/\w{cost}]) \eval s'[d/\w{cost}] \quad d \leq c
     829\end{array}
    825830\]}
    826831
     
    10031008\]}
    10041009
    1005 {\bf Simulation}
    1006 The simulation properties of the compilation functions are lifted to the labelled languages.
    1007 
    1008 With a proper design of the labelled languages this just means taking into account the rules that
    1009 generate labelled transitions. 
    1010 
    1011 Let $\lambda$ denote a sequence of labels. Then we have:
     1010\begin{description}
     1011
     1012\item[Simulation]
     1013The simulation properties of the compilation functions are {\em lifted} to the labelled languages.
     1014%With a proper design of the labelled languages this just means taking into account the rules that
     1015%generate labelled transitions. 
     1016Let $\lambda$ denote a sequence of labels. Then:% we have:
     1017\end{description}
    10121018\[
    10131019(S,s)\eval (s',\lambda)  \quad \Arrow \quad
     
    10451051\]}
    10461052
    1047 By {\bf diagram chasing} we get:
     1053\begin{description}
     1054
     1055\item[Numerical vs. Symbolic cost] By {\bf diagram chasing} we derive:
    10481056\[
    10491057\infer{(\w{An}(S),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]}
    1050 {(\cl{C}(\cl{L}(S)),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)}
     1058{(\cl{C'}(\cl{C}(\cl{L}(S))),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)}
    10511059\]
    1052 where $\delta$ is an `arbitrary additive cost'
    1053 of the sequence of labels $\lambda$.
     1060where $\delta$ is the numerical (additive) cost associated with $\lambda$.
     1061
     1062\end{description}
    10541063
    10551064\end{frame}
     
    10821091\]}
    10831092
    1084 Knowing that
     1093\begin{description}
     1094
     1095\item[When is the labelling $\cl{L}$ interesting?]
     1096I.e., knowing that
    10851097\[
    10861098\cl{C'}(\cl{C}(S)) = \w{er}_{\mips}(\cl{C'}(\cl{C}(\cl{L}(S)))
    10871099\]
    1088 {\bf under which conditions} can we conclude that $\lambda$, {\em i.e.}, $\delta$, is a sound and  possibly precise description of the real execution cost?
    1089 
     1100{\bf under which conditions} can we conclude that $\lambda$, {\em i.e.},
     1101$\delta$, is a sound and  possibly precise description of the real execution cost?
     1102\end{description}
    10901103\end{frame}
    10911104
     
    10941107
    10951108\frametitle{Labelling approach (7/7)}
     1109Conditions to be checked on the labelled binary code.
    10961110
    10971111{\small
     
    11461160\begin{frame}
    11471161
    1148 \frametitle{A larger experiment: a $C$ to $\mips$ compiler}
     1162\frametitle{A larger experiment: a $\C$ to $\mips$ compiler}
    11491163{\footnotesize
    11501164\[
     
    11631177
    11641178\item Roughly, we implement the labelling approach on top of a compiler quite
    1165 close to {\sc CompCert}.
     1179close to $\compcert$.
    11661180
    11671181\item Around 10K lines of $\ocaml$ code. No proofs, just code inspection and test. We used the software  in a master level compilation course.
     
    11821196\item The first situation never arises in the considered compilation chain.
    11831197
    1184 \item The second situation can be handled by some pre-processing of the C code
     1198\item The second situation can be handled by some pre-processing of the $\C$ code
    11851199(e.g., logical \bem{and} compiled as a conditional expression).
    11861200
     
    11951209\frametitle{What comes next}
    11961210This work was completed in the first 7 months of the project.
    1197 The following months have been spent:
    1198 
    1199 
    1200 \begin{itemize}
     1211The following 5 months have been spent:
     1212
     1213
     1214\begin{itemize}
     1215\item Enhancing and debugging the compiler.
    12011216
    12021217\item Extending the formal proofs on the toy compiler.
    12031218
    1204 \item Enhancing and debugging the compiler.
    1205 
    1206 \item Porting it to the 8051 processor.
    1207 
    1208 \item Integrating the {\sc Ocaml/Matita} description of 8051.
     1219\item Porting the compiler from $\mips$  to $\eighty$ (and teaching this).
     1220
     1221\item Integrating the {\sc Ocaml/Matita} description of $\eighty$.
    12091222
    12101223\end{itemize}
    12111224
    1212 This is discussed in the second part of the talk.
     1225This is covered in the second part of the talk.
    12131226
    12141227\end{frame}
Note: See TracChangeset for help on using the changeset viewer.