source: Deliverables/D1.1/Presentations/WP2-yann.tex @ 3534

\documentclass[10pt]{beamer}
\usetheme{Frankfurt}
\logo{\includegraphics[height=1.0cm]{fetopen.png}}
\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath, amssymb, amsfonts}
\usepackage{stmaryrd}
\usepackage{graphicx}
\usepackage{array}
\usepackage{fancybox}


\newcommand{\N}{\mathbb{N}}
\newcommand{\sem}[1]{\llbracket #1 \rrbracket}
\newcommand{\Comp}{\mathcal{C}}
\newcommand{\semequiv}{\equiv}
\newcommand{\Annot}{\mathit{An}}
\newcommand{\semleads}{\Downarrow}
\newcommand{\Lab}{\mathcal{L}}
\newcommand{\LabLang}[1]{$\text{#1}^\Lab$}
\newcommand{\medquad}{\quad\quad}
\newcommand{\bigquad}{\quad\quad\quad}
\newcommand{\PSet}[1]{\mathcal{P}(#1)}

\definecolor{transblack}{RGB}{217,217,217}
\definecolor{transred}{RGB}{255,215,215}
\definecolor{transgreen}{RGB}{215,255,215}
\definecolor{transblue}{RGB}{215,215,255}
\definecolor{transorange}{RGB}{255,235,215}
\definecolor{transmagenta}{RGB}{255,215,235}

\definecolor{darkred}{RGB}{102,0,0}
\definecolor{transdarkred}{RGB}{230,215,215}
\definecolor{darkgreen}{RGB}{0,102,0}
\definecolor{transdarkgreen}{RGB}{215,230,215}

\definecolor{violet}{RGB}{160,0,160}
\definecolor{lightviolet}{RGB}{255,204,204}

\newcommand{\checked}{\textcolor{darkgreen}{$\surd$}}
\newcommand{\unchecked}{\textcolor{red}{X}}
\newcommand{\plus}{\textcolor{darkgreen}{+}}
\newcommand{\minus}{\textcolor{red}{-}}

\newcommand{\notitle}{\frametitle{\textcolor{white}{A}}}
\newcommand{\moveup}{\includegraphics[height=10cm]{figs/nothing.mps}}

\newcommand{\Clang}{\textsc{C}}
\newcommand{\Clight}{\textsc{Clight}}
\newcommand{\Cminor}{\textsc{Cminor}}
\newcommand{\RTLabs}{\textsc{RTL}_{\textsc{abs}}}
\newcommand{\RTL}{\textsc{RTL}}
\newcommand{\ERTL}{\textsc{ERTL}}
\newcommand{\LTL}{\textsc{LTL}}
\newcommand{\LIN}{\textsc{LIN}}
\newcommand{\MIPS}{\textsc{MIPS}}
\newcommand{\Imp}{\textsc{Imp}}
\newcommand{\VM}{\textsc{VM}}
\newcommand{\ASM}{\textsc{ASM}}
\newcommand{\Labelled}[1]{#1^\mathcal{L}}

\newcommand{\lbl}{\ell}

\newlength\codewidth
\newenvironment{code}[1][\codewidth]{
\begin{center}
\Sbox
\hspace{0.3cm}\minipage{#1}
}{
\endminipage
\endSbox\fbox{\TheSbox}
\end{center}
}


%\input{mybeamer}
\newcommand{\BlueLabelled}[1]{#1^{\textcolor{blockTColor}{\mathcal{L}}}}

\setbeamersize{text margin left=5mm, text margin right=5mm}
\parskip=3mm
\setbeamercovered{invisible}

\title{
CerCo Work Package 2 : \\
The Untrusted Compiler Prototype \\
{\small (part 2)}}
\author{Yann Régis-Gianas}
\institute{}
\date{March $11$, 2011}


\begin{document}

\begin{frame}
\titlepage
\end{frame}

\begin{frame}
  \frametitle{Architecture of the Compiler}

  \centering

  \includegraphics[width=\linewidth]{figs/diagram3.mps}

  \bigskip
  \bigskip

  \begin{tabular}{cc}
    \textcolor{blue}{Labelling} \quad & \quad \textcolor{darkgreen}{Erasure}\\
    \\
    \textcolor{red}{Compilation} \quad &
    \quad \textcolor{darkred}{Labelled compilation}\\
    \\
    \textcolor{orange}{Cost deduction} \quad &
    \quad \textcolor{magenta}{Instrumentation}
  \end{tabular}

% Roberto already said that we did a large experiment to validate this
% architecture: a compiler from C to MIPS. 

\end{frame}

\begin{frame}
\frametitle{Benchmarks on the MIPS compiler}

  \centering

  \begin{tabular}{r|rrr}
    & \texttt{gcc -O0} & \texttt{acc} & \texttt{gcc -O1} \\
    \hline
    \texttt{badsort} & 55.93 & 34.51 & 12.96 \\
    \texttt{fib} & 76.24 & 34.28 & 45.68 \\
    \texttt{mat\_det} & 163.42 & 156.20 & 54.76 \\ 
    \texttt{min} & 12.21 & 16.25 & 3.95 \\
    \texttt{quicksort} & 27.46 & 17.95 & 9.41 \\
    \texttt{search} & 463.19 & 623.79 & 155.38 \\
    \hline
  \end{tabular}

\end{frame}


\begin{frame}
\frametitle{Porting from MIPS to the 8051 microprocessor}

Targetting the 8051 microprocessor raised the following issues:

\begin{itemize}
\item How to represent  32 bits values in an 8 bits architecture?
\item How to deal with heterogeneous representation of pointers and integers?
(Words are 8 bits long whereas memory addresses are stored using 16 bits.)
\item How to select instructions for this microprocessor?
\item What calling convention to use?
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Where was the difficulty in the prototype implementation?}

The main issue in scaling our approach from the toy compiler to the C
compiler was \textbf{function calls} because they add an extra
complexity in the labelling process.


\end{frame}

\begin{frame}
\frametitle{How to cover the control flow with cost labels?}

  \centering

  \bigskip

  \only<1>{\includegraphics{figs/call1.mps}}
  \only<2-3>{\includegraphics{figs/call2.mps}}

  \bigskip
  \medskip

  \visible<3>{
    \begin{block}{}
      \centering
      \textcolor{red}{Function pointer: statically unresolvable destination}

      Each function should handle its cost.~\footnote{Notice that the
        proof of the compiler will provide the invariant that function
        pointers always only contain valid addresses to code generated
        using the same compiler.}
    \end{block}

    \bigskip
    \medskip

    \includegraphics{figs/call3.mps}}

\end{frame}


\begin{frame}
\frametitle{A glimpse on the compiler passes}

\begin{code}[7.5cm]
\bgroup\sf\medskip\begin{flushleft}

\noindent\hspace*{0.00em}\textbf{char} search (\textbf{char} tab[], \textbf{char} size, \textbf{char} to\_{}find) \{~\linebreak
\noindent\hspace*{1.00em}\textbf{char} low = 0, high = size-1, i;~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{1.00em}\textbf{while} (high \ensuremath{\ge} low) \{~\linebreak
\noindent\hspace*{2.00em}i = (high+low) / 2;~\linebreak
\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{==}} to\_{}find) \textbf{return} i;~\linebreak
\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{>}} to\_{}find) high = i-1;~\linebreak
\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{<}} to\_{}find) low = i+1;~\linebreak
\noindent\hspace*{1.00em}\}~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{1.00em}\textbf{return} (-1);~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}\medskip\egroup\noindent
\end{code}
\end{frame}



\begin{frame}
\frametitle{A glimpse on the compiler passes : Labelling in {\sc Clight}}

\begin{code}[7.5cm]\scriptsize
\bgroup\sf\medskip\begin{flushleft}

\noindent\hspace*{0.00em}\textbf{unsigned} \textbf{char} search(\textbf{unsigned} \textbf{char} *tab, \textbf{unsigned} \textbf{char} size, \linebreak
\noindent\hspace*{2.5cm}\textbf{unsigned} \textbf{char} to\_{}find)~\linebreak
\noindent\hspace*{0.00em}\{~\linebreak
\noindent\hspace*{1.00em}\textbf{unsigned} \textbf{char} low, high, i;~\linebreak
\noindent\hspace*{1.00em}\textcolor{red}{\_cost8:}~\linebreak
\noindent\hspace*{1.00em}low = (\textbf{unsigned} \textbf{char})0;~\linebreak
\noindent\hspace*{1.00em}high = (\textbf{unsigned} \textbf{char})((\textbf{int})size - 1);~\linebreak
\noindent\hspace*{1.00em}\textbf{while} ((\textbf{int})high \ensuremath{\ge} (\textbf{int})low) \{~\linebreak
\noindent\hspace*{2.00em}\textcolor{red}{\_cost6:}~\linebreak
\noindent\hspace*{2.00em}i = (\textbf{unsigned} \textbf{char})(((\textbf{int})high + (\textbf{int})low) / 2);~\linebreak
\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{==}} (\textbf{int})to\_{}find) \{  ~\linebreak
\noindent\hspace*{4.00em}\textcolor{red}{\_cost4}\ensuremath{:~} \textbf{return} i; ~\linebreak
\noindent\hspace*{2.00em}\} \textbf{else} \{\textcolor{red}{\_cost5:}  \}~\linebreak
\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{>}} (\textbf{int})to\_{}find) \{ ~\linebreak
\noindent\hspace*{3.00em}\textcolor{red}{\_cost2}\ensuremath{:~} high = (\textbf{unsigned} \textbf{char})((\textbf{int})i - 1); ~\linebreak
\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost3}\ensuremath{:~}  \}~\linebreak
\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{<}} (\textbf{int})to\_{}find) \{ ~\linebreak
\noindent\hspace*{3.00em}\textcolor{red}{\_cost0}\ensuremath{:~} low = (\textbf{unsigned} \textbf{char})((\textbf{int})i + 1); ~\linebreak
\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost1}\ensuremath{:~} \}~\linebreak
\noindent\hspace*{1.00em}\}~\linebreak
\noindent\hspace*{1.00em}\textcolor{red}{\_cost7}\ensuremath{:~}~\linebreak
\noindent\hspace*{1.00em}\textbf{return} (\textbf{unsigned} \textbf{char})(-1);~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}\medskip\egroup\noindent
\end{code}
\end{frame}

\begin{frame}
\frametitle{A glimpse on the compiler passes : $RTL_{abs}$}

\begin{code}[7.5cm]
\bgroup\sf\medskip\begin{flushleft}

\noindent\hspace*{0.50em}"search"([\%{}9 ; \%{}8], [\%{}2], [\%{}3])\linebreak
\noindent\hspace*{0.50em}\ensuremath{:~} ptr \ensuremath{\rightarrow} \textbf{int} \ensuremath{\rightarrow} \textbf{int} \ensuremath{\rightarrow} \textbf{int}~\linebreak
\noindent\hspace*{2.00em}locals\ensuremath{:~} ...~\linebreak
\noindent\hspace*{2.00em}result\ensuremath{:~} [\%{}10]~\linebreak
\noindent\hspace*{2.00em}stacksize\ensuremath{:~} 0~\linebreak
\noindent\hspace*{2.00em}entry\ensuremath{:~} search40~\linebreak
\noindent\hspace*{2.00em}exit\ensuremath{:~} search0~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{2.00em}search9\ensuremath{:~} lt [\%{}13], [\%{}3] -\ensuremath{\rightarrow} search8, search5~\linebreak
\noindent\hspace*{2.00em}search8\ensuremath{:~} \textcolor{red}{emit \_cost0} -\ensuremath{\rightarrow} search7~\linebreak
\noindent\hspace*{2.00em}search7\ensuremath{:~} imm [\%{}12], imm\_{}int 1 -\ensuremath{\rightarrow} search6~\linebreak
\noindent\hspace*{2.00em}search6\ensuremath{:~} add [\%{}5], [\%{}7], [\%{}12] -\ensuremath{\rightarrow} search4~\linebreak
\noindent\hspace*{2.00em}search5\ensuremath{:~} \textcolor{red}{emit \_cost1} -\ensuremath{\rightarrow} search4~\linebreak
\noindent\hspace*{2.00em}search40\ensuremath{:~} \textcolor{red}{emit \_cost8} -\ensuremath{\rightarrow} search39~\linebreak
\noindent\hspace*{2.00em}search4\ensuremath{:~} -\ensuremath{\rightarrow} search36~\linebreak
\noindent\hspace*{2.00em}\emph{// ...}
\end{flushleft}\medskip\egroup\noindent
\end{code}
\end{frame}

\begin{frame}
\frametitle{A glimpse on the compiler passes : 8051}

\begin{code}[7.5cm]\scriptsize
\bgroup\sf\medskip\begin{flushleft}

\begin{tabular}{ll}
\noindent\hspace*{1.00em}\emph{// ...}~\\
\noindent\hspace*{1.00em}\textcolor{gray}{317\ensuremath{:~}}  nop               
&\textbf{;; 1  \textcolor{red}{\_{}cost4}}~\\
\noindent\hspace*{1.00em}\textcolor{gray}{318\ensuremath{:~}}  mov   002h, \#{}000h &\textbf{;; 3  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{321\ensuremath{:~}}  mov   A, 002h     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{323\ensuremath{:~}}  mov   005h, A     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{325\ensuremath{:~}}  mov   A, 009h     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{327\ensuremath{:~}}  mov   004h, A     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{329\ensuremath{:~}}  mov   A, 000h     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{331\ensuremath{:~}}  push  0E0h        &\textbf{;; 2  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{333\ensuremath{:~}}  mov   A, 001h     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{335\ensuremath{:~}}  push  0E0h        &\textbf{;; 2  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{337\ensuremath{:~}}  mov   0E0h, \#{}004h &\textbf{;; 3  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{340\ensuremath{:~}}  add   A, 006h     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{342\ensuremath{:~}}  mov   006h, A     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{344\ensuremath{:~}}  mov   0E0h, \#{}000h &\textbf{;; 3  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{347\ensuremath{:~}}  addc  A, 007h     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{349\ensuremath{:~}}  mov   007h, A     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{351\ensuremath{:~}}  mov   A, 005h     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{353\ensuremath{:~}}  mov   083h, A     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{355\ensuremath{:~}}  mov   A, 004h     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{357\ensuremath{:~}}  mov   082h, A     &\textbf{;; 1  }~\\
\noindent\hspace*{1.00em}\textcolor{gray}{359\ensuremath{:~}}  ret               &\textbf{;; 2  }
\end{tabular}
\end{flushleft}\medskip\egroup\noindent
\end{code}
\end{frame}

\begin{frame}
\frametitle{A glimpse on the compiler passes : Annotating in {\sc Clight}}

\begin{code}[7.5cm]\scriptsize
\bgroup\sf\medskip\begin{flushleft}

\noindent\hspace*{0.00em}\textbf{unsigned} \textbf{char} search(\textbf{unsigned} \textbf{char} *tab, \textbf{unsigned} \textbf{char} size, \linebreak
\noindent\hspace*{2.5cm}\textbf{unsigned} \textbf{char} to\_{}find)~\linebreak
\noindent\hspace*{0.00em}\{~\linebreak
\noindent\hspace*{1.00em}\textbf{unsigned} \textbf{char} low, high, i;~\linebreak
\noindent\hspace*{1.00em}\textcolor{red}{\_cost8:~\textbf{cost += 117;}} \linebreak
\noindent\hspace*{1.00em}low = (\textbf{unsigned} \textbf{char})0;~\linebreak
\noindent\hspace*{1.00em}high = (\textbf{unsigned} \textbf{char})((\textbf{int})size - 1);~\linebreak
\noindent\hspace*{1.00em}\textbf{while} ((\textbf{int})high \ensuremath{\ge} (\textbf{int})low) \{~\linebreak
\noindent\hspace*{2.00em}\textcolor{red}{\_cost6:~\textbf{cost += 77;}}~\linebreak
\noindent\hspace*{2.00em}i = (\textbf{unsigned} \textbf{char})(((\textbf{int})high + (\textbf{int})low) / 2);~\linebreak
\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{==}} (\textbf{int})to\_{}find) \{  ~\linebreak
\noindent\hspace*{4.00em}\textcolor{red}{\_cost4\ensuremath{:~\textbf{cost += 30;}}} \textbf{return} i; ~\linebreak
\noindent\hspace*{2.00em}\} \textbf{else} \{\textcolor{red}{\_cost5:~\textbf{cost += 103;}}  \}~\linebreak
\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{>}} (\textbf{int})to\_{}find) \{ ~\linebreak
\noindent\hspace*{3.00em}\textcolor{red}{\_cost2\ensuremath{:~\textbf{cost += 98;}}} high = (\textbf{unsigned} \textbf{char})((\textbf{int})i - 1); ~\linebreak
\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost3\ensuremath{:~\textbf{cost += 85;}}}  \}~\linebreak
\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{<}} (\textbf{int})to\_{}find) \{ ~\linebreak
\noindent\hspace*{3.00em}\textcolor{red}{\_cost0\ensuremath{:~\textbf{cost += 98;}}} low = (\textbf{unsigned} \textbf{char})((\textbf{int})i + 1); ~\linebreak
\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost1\ensuremath{:~\textbf{cost += 88;}}} \}~\linebreak
\noindent\hspace*{1.00em}\}~\linebreak
\noindent\hspace*{1.00em}\textcolor{red}{\_cost7\ensuremath{:~\textbf{cost += 43;}}}~\linebreak
\noindent\hspace*{1.00em}\textbf{return} (\textbf{unsigned} \textbf{char})(-1);~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}\medskip\egroup\noindent
\end{code}
\end{frame}


\begin{frame}
\frametitle{Future work}

\begin{itemize}

\item Prototype maintenance, validation and testing.

\item Integration of the 8051 specification (recently provided as
  deliverable 4.1).

\item Integration of the non-standard extensions of the C language consisting
  of directives that specifies storage location (given that their semantics have
  been addressed in deliverable 3.1).

\item Integration of a preprocessor to encode 16 bits and 32 bits
  integers into records of 8 bits integers.

\item Improvement of instruction selection (but we will not sacrifice
  conceptual simplicity to keep mechanized proofs manageable).

\item Development of a {\tt Frama-C} plugin that will embed the compiler as 
  well as an algorithm to produce synthetic information on the execution of C
  functions from the current cost annotations (which only give information about
  constant time portions of code).

\end{itemize}

\end{frame}

\end{document}