Changeset 633

Show
Ignore:
Timestamp:
03/04/11 17:38:45 (2 years ago)
Message:

wp2 revised

Files:
1 modified

Unmodified
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}