Changeset 633

Timestamp:

03/04/11 17:38:45 (2 years ago)

Author:

amadio

Message:

wp2 revised

Files:

• Deliverables/D1.1/Presentations/WP2-roberto.tex (modified) (18 diffs)

Deliverables/D1.1/Presentations/WP2-roberto.tex

@@ -495 +495 @@
 \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}
 
@@ -530 +530 @@
 
 \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.}
@@ -539 +539 @@
 \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}
@@ -589 +595 @@
 \begin{frame}
 
-\frametitle{CerCo goals and approach}
+\frametitle{$\cerco$ goals and approach}
 
 \begin{itemize}
@@ -596 +602 @@
 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}
@@ -624 +630 @@
 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) 
@@ -634 +640 @@
 \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}).
 
@@ -647 +653 @@
 \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}
@@ -702 +708 @@
 \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}
@@ -818 +824 @@
 {\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}
 \]}
 
@@ -1003 +1008 @@
 \]}
 
-{\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 
@@ -1045 +1051 @@
 \]}
 
-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}
@@ -1082 +1091 @@
 \]}
 
-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}
 
@@ -1094 +1107 @@
 
 \frametitle{Labelling approach (7/7)}
+Conditions to be checked on the labelled binary code.
 
 {\small
@@ -1146 +1160 @@
 \begin{frame}
 
-\frametitle{A larger experiment: a $C$ to $\mips$ compiler}
+\frametitle{A larger experiment: a $\C$ to $\mips$ compiler}
 {\footnotesize
 \[
@@ -1163 +1177 @@
 
 \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.
@@ -1182 +1196 @@
 \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).
 
@@ -1195 +1209 @@
 \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}