# Changeset 633 for Deliverables

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

wp2 revised

File:
1 edited

### Legend:

Unmodified
 r626 \institute{Universit\'e Paris Diderot} \title{CerCo Work Package 2: Untrusted Compiler Prototype (part 1)} \title{$\cerco$ Work Package 2: Untrusted Compiler Prototype (part 1)} \date{March 11, 2011} \end{description} {\small This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The {\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), and  provide some perspectives on Task 2.4 and WP5.} \begin{frame} \frametitle{People involved at Paris site} \frametitle{People involved at UPD site} {\small \begin{tabular}{|c|c|c|} \hline {\bf Name}           &{\bf Status} &{\bf Rough Allocated Time} \\\hline Roberto Amadio &Professor &1 day/week \\ Yann R\'egis-Gianas &Assistant Professor &1 day/week \\ Nicolas Ayache      &Post-doc      &full time, 11 months \\ Ronan Saillard      &Internship+PhD &full time, 8 months \\ Kayvan Memarian     &Internship   &1.5 days/week, 4 months \\ \hline \end{tabular} Roberto \textsc{Amadio} &Professor &1 day/week \\ Yann \textsc{R\'egis-Gianas} &Assistant Professor &1 day/week \\ Nicolas \textsc{Ayache}      &Post-doc      &full time, 11 months \\ Ronan \textsc{Saillard}      &Internship+PhD &full time, 8 months \\ Kayvan \textsc{Memarian}     &Internship   &1.5 days/week, 4 months \\ \hline \end{tabular}} ~\\~\\ \Red{{\bf NB}} Internships are very important: dissemination, speed up development, explore side paths, preliminary training towards research (PhD),$\ldots$ \end{frame} \begin{frame} \frametitle{CerCo goals and approach} \frametitle{$\cerco$ goals and approach} \begin{itemize} given  piece of code on a given processor with a given compiler. \item Target {\bf C programs}, and in particular the kind of C \item Target {\bf $\C$ programs}, and in particular the kind of $\C$ programs produced for embedded applications (such as those generated by the SCADE compiler). (such as those generated by the $\scade$ compiler). \item {\bf Reflect the cost information} obtained at the machine level back into the C source code. back into the $\C$ source code. \item {\bf Extract synthetic bounds} by reasoning on the annotated C  programs (for which several general purpose tools now exist). the annotated $\C$  programs (for which several general purpose tools now exist). \end{itemize} \NB Technically, this can be seen as a refinement of ongoing work on {\bf compiler certification} (see, e.g., CompCert project). \Red{\NB} Technically, this can be seen as a refinement of ongoing work on {\bf compiler certification} (see, e.g., $\compcert$ project). \end{frame} but not formally checked with a proof assistant. $\textsc{Lustre} \arrow \textsc{C} \arrow \textsc{binary~ code} \lustre \arrow \C \arrow \textsc{binary~ code}$ \item Binary code must be {\bf annotated} with (uncertified) \end{itemize} \noindent{\bf Our challenge} Lift in a certified way whathever information we have on the execution cost of the binary code to an information on the C source code (a kind \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}). \frametitle{A potential connection} Could use this work as a {\bf platform} to experiment with implicit complexity programming languages'. \Blu{{\em implicit complexity programming languages}}. {\small \begin{enumerate} \item Write a program in your preferred implicit-complexity programming language. \item Compile it to C. \item CerCo compiles C to machine code and provides precise and certified information on execution time of C code. \item Write a program in your preferred implicit complexity programming language. \item Compile it to $\C$. \item $\cerco$ compiles $\C$ to machine code and provides precise and certified information on execution time of $\C$ code. \item Use your implicit complexity analysis to produce automatically a synthetic bound on the resources used by the program. \item If you want to push this further, try to lift the assertions about the C code to assertions on your source program. \item If you want to push this further, try to lift the assertions about the $\C$ code to assertions on your source program. \end{enumerate}} \end{frame} \item Starting from the annotated source program apply standard tools to reason about C programs in order to {\bf extract synthetic bounds}. to reason about $\C$ programs in order to {\bf extract synthetic bounds}. \end{itemize} {\small $\infer{(\w{An}_{i}(S),s[0/\w{cost}])\eval s'[c/\w{cost}]} {\begin{array}{c} (\w{An}_{i+1}(\cl{C}_{i,i+1}(S)),s[0/\w{cost}]) \eval s'[d/\w{cost}] \\ d \leq c \end{array}} \begin{array}{lc} \mbox{Predicted' cost} &(\w{An}_{i}(S),s[0/\w{cost}])\eval s'[c/\w{cost}]\\\hline \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 \end{array}$} \]} {\bf Simulation} The simulation properties of the compilation functions are lifted to the labelled languages. With a proper design of the labelled languages this just means taking into account the rules that generate labelled transitions. Let $\lambda$ denote a sequence of labels. Then we have: \begin{description} \item[Simulation] The simulation properties of the compilation functions are {\em lifted} to the labelled languages. %With a proper design of the labelled languages this just means taking into account the rules that %generate labelled transitions. Let $\lambda$ denote a sequence of labels. Then:% we have: \end{description} $(S,s)\eval (s',\lambda) \quad \Arrow \quad$} By {\bf diagram chasing} we get: \begin{description} \item[Numerical vs. Symbolic cost] By {\bf diagram chasing} we derive: $\infer{(\w{An}(S),s[c/\w{cost}]) \eval s'[c+\delta/\w{cost}]} {(\cl{C}(\cl{L}(S)),s[c/\w{cost}]) \eval (s'[c/\w{cost}],\lambda)} {(\cl{C'}(\cl{C}(\cl{L}(S))),s[c/\w{cost}]) \eval (s'[c/\w{cost}],\lambda)}$ where $\delta$ is an arbitrary additive cost' of the sequence of labels $\lambda$. where $\delta$ is the numerical (additive) cost associated with $\lambda$. \end{description} \end{frame} \]} Knowing that \begin{description} \item[When is the labelling $\cl{L}$ interesting?] I.e., knowing that $\cl{C'}(\cl{C}(S)) = \w{er}_{\mips}(\cl{C'}(\cl{C}(\cl{L}(S)))$ {\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? {\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? \end{description} \end{frame} \frametitle{Labelling approach (7/7)} Conditions to be checked on the labelled binary code. {\small \begin{frame} \frametitle{A larger experiment: a $C$ to $\mips$ compiler} \frametitle{A larger experiment: a $\C$ to $\mips$ compiler} {\footnotesize \[ \item Roughly, we implement the labelling approach on top of a compiler quite close to {\sc CompCert}. close to $\compcert$. \item Around 10K lines of $\ocaml$ code. No proofs, just code inspection and test. We used the software  in a master level compilation course. \item The first situation never arises in the considered compilation chain. \item The second situation can be handled by some pre-processing of the C code \item The second situation can be handled by some pre-processing of the $\C$ code (e.g., logical \bem{and} compiled as a conditional expression). \frametitle{What comes next} This work was completed in the first 7 months of the project. The following months have been spent: \begin{itemize} The following 5 months have been spent: \begin{itemize} \item Enhancing and debugging the compiler. \item Extending the formal proofs on the toy compiler. \item Enhancing and debugging the compiler. \item Porting it to the 8051 processor. \item Integrating the {\sc Ocaml/Matita} description of 8051. \item Porting the compiler from $\mips$  to $\eighty$ (and teaching this). \item Integrating the {\sc Ocaml/Matita} description of $\eighty$. \end{itemize} This is discussed in the second part of the talk. This is covered in the second part of the talk. \end{frame}