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

Last change on this file since 662 was 662, checked in by regisgia, 9 years ago

New version of the slides.

File size: 12.8 KB
RevLine 
[655]1\documentclass[10pt]{beamer}
[662]2\usetheme{Frankfurt}
3\logo{\includegraphics[height=1.0cm]{fetopen.png}}
4\usepackage[english]{babel}
[655]5\usepackage[latin1]{inputenc}
6\usepackage[T1]{fontenc}
7\usepackage{amsmath, amssymb, amsfonts}
8\usepackage{stmaryrd}
9\usepackage{graphicx}
10\usepackage{array}
11\usepackage{fancybox}
12
[662]13
14\newcommand{\N}{\mathbb{N}}
15\newcommand{\sem}[1]{\llbracket #1 \rrbracket}
16\newcommand{\Comp}{\mathcal{C}}
17\newcommand{\semequiv}{\equiv}
18\newcommand{\Annot}{\mathit{An}}
19\newcommand{\semleads}{\Downarrow}
20\newcommand{\Lab}{\mathcal{L}}
21\newcommand{\LabLang}[1]{$\text{#1}^\Lab$}
22\newcommand{\medquad}{\quad\quad}
23\newcommand{\bigquad}{\quad\quad\quad}
24\newcommand{\PSet}[1]{\mathcal{P}(#1)}
25
26\definecolor{transblack}{RGB}{217,217,217}
27\definecolor{transred}{RGB}{255,215,215}
28\definecolor{transgreen}{RGB}{215,255,215}
29\definecolor{transblue}{RGB}{215,215,255}
30\definecolor{transorange}{RGB}{255,235,215}
31\definecolor{transmagenta}{RGB}{255,215,235}
32
33\definecolor{darkred}{RGB}{102,0,0}
34\definecolor{transdarkred}{RGB}{230,215,215}
35\definecolor{darkgreen}{RGB}{0,102,0}
36\definecolor{transdarkgreen}{RGB}{215,230,215}
37
38\definecolor{violet}{RGB}{160,0,160}
39\definecolor{lightviolet}{RGB}{255,204,204}
40
41\newcommand{\checked}{\textcolor{darkgreen}{$\surd$}}
42\newcommand{\unchecked}{\textcolor{red}{X}}
43\newcommand{\plus}{\textcolor{darkgreen}{+}}
44\newcommand{\minus}{\textcolor{red}{-}}
45
46\newcommand{\notitle}{\frametitle{\textcolor{white}{A}}}
47\newcommand{\moveup}{\includegraphics[height=10cm]{figs/nothing.mps}}
48
49\newcommand{\Clang}{\textsc{C}}
50\newcommand{\Clight}{\textsc{Clight}}
51\newcommand{\Cminor}{\textsc{Cminor}}
52\newcommand{\RTLabs}{\textsc{RTL}_{\textsc{abs}}}
53\newcommand{\RTL}{\textsc{RTL}}
54\newcommand{\ERTL}{\textsc{ERTL}}
55\newcommand{\LTL}{\textsc{LTL}}
56\newcommand{\LIN}{\textsc{LIN}}
57\newcommand{\MIPS}{\textsc{MIPS}}
58\newcommand{\Imp}{\textsc{Imp}}
59\newcommand{\VM}{\textsc{VM}}
60\newcommand{\ASM}{\textsc{ASM}}
61\newcommand{\Labelled}[1]{#1^\mathcal{L}}
62
63\newcommand{\lbl}{\ell}
64
65\newlength\codewidth
66\newenvironment{code}[1][\codewidth]{
67\begin{center}
68\Sbox
69\hspace{0.3cm}\minipage{#1}
70}{
71\endminipage
72\endSbox\fbox{\TheSbox}
73\end{center}
74}
75
76
77%\input{mybeamer}
[655]78\newcommand{\BlueLabelled}[1]{#1^{\textcolor{blockTColor}{\mathcal{L}}}}
79
80\setbeamersize{text margin left=5mm, text margin right=5mm}
81\parskip=3mm
82\setbeamercovered{invisible}
83
84\title{
85CerCo Work Package 2 : \\
86The Untrusted Compiler Prototype \\
87{\small (part 2)}}
88\author{Yann Régis-Gianas}
89\institute{}
[662]90\date{March $11$, 2011}
[655]91
92
93\begin{document}
94
95\begin{frame}
96\titlepage
97\end{frame}
98
99\begin{frame}
100  \frametitle{Architecture of the Compiler}
101
102  \centering
103
[662]104  \includegraphics[width=\linewidth]{figs/diagram3.mps}
[655]105
106  \bigskip
107  \bigskip
108
109  \begin{tabular}{cc}
110    \textcolor{blue}{Labelling} \quad & \quad \textcolor{darkgreen}{Erasure}\\
111    \\
112    \textcolor{red}{Compilation} \quad &
113    \quad \textcolor{darkred}{Labelled compilation}\\
114    \\
115    \textcolor{orange}{Cost deduction} \quad &
116    \quad \textcolor{magenta}{Instrumentation}
117  \end{tabular}
118
119% Roberto already said that we did a large experiment to validate this
120% architecture: a compiler from C to MIPS.
121
122\end{frame}
123
124\begin{frame}
125\frametitle{Porting from MIPS to the 8051 microprocessor}
126
127Targetting the 8051 microprocessor raised the following issues:
128
129\begin{itemize}
130\item How to represent  32bits values in an 8bits architecture?
131\item How to deal with heterogeneous representation of pointers and integers?
132(Words are 8bits long whereas memory addresses are stored using 16bits.)
133\item How to select instruction for this microprocessor?
134\item What calling convention to use?
135\end{itemize}
136
137\end{frame}
138
139\begin{frame}
140\frametitle{Where was the difficulty in the prototype implementation?}
141
142The main issue in scaling our approach from the toy compiler to the C
143compiler was \textbf{function calls} because they add an extra
144complexity in the labelling process.
145
146
147\end{frame}
148
149\begin{frame}
150\frametitle{How to cover the control flow with cost labels?}
151
152  \centering
153
154  \bigskip
155
[662]156  \only<1>{\includegraphics{figs/call1.mps}}
157  \only<2-3>{\includegraphics{figs/call2.mps}}
[655]158
159  \bigskip
160  \medskip
161
162  \visible<3>{
163    \begin{block}{}
164      \centering
165      \textcolor{red}{Function pointer: statically unresolvable destination}
166
167      Each function should handle its cost.~\footnote{Notice that the
168        proof of the compiler will provide the invariant that function
169        pointers always only contain valid addresses to code generated
170        using the same compiler.}
171    \end{block}
172
173    \bigskip
174    \medskip
175
[662]176    \includegraphics{figs/call3.mps}}
[655]177
178\end{frame}
179
180
181\begin{frame}
182\frametitle{A glimpse on the compiler passes}
183
[662]184\begin{code}[7.5cm]
[655]185\bgroup\sf\medskip\begin{flushleft}
186
187\noindent\hspace*{0.00em}\textbf{char} search (\textbf{char} tab[], \textbf{char} size, \textbf{char} to\_{}find) \{~\linebreak
188\noindent\hspace*{1.00em}\textbf{char} low = 0, high = size-1, i;~\linebreak
189\noindent\hspace*{0.00em}~\linebreak
190\noindent\hspace*{1.00em}\textbf{while} (high \ensuremath{\ge} low) \{~\linebreak
191\noindent\hspace*{2.00em}i = (high+low) / 2;~\linebreak
192\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{==}} to\_{}find) \textbf{return} i;~\linebreak
193\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{>}} to\_{}find) high = i-1;~\linebreak
194\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{<}} to\_{}find) low = i+1;~\linebreak
195\noindent\hspace*{1.00em}\}~\linebreak
196\noindent\hspace*{0.00em}~\linebreak
197\noindent\hspace*{1.00em}\textbf{return} (-1);~\linebreak
198\noindent\hspace*{0.00em}\}
199\end{flushleft}\medskip\egroup\noindent
200\end{code}
201\end{frame}
202
203
204
205\begin{frame}
206\frametitle{A glimpse on the compiler passes : Labelling in {\sc Clight}}
207
[662]208\begin{code}[7.5cm]\scriptsize
[655]209\bgroup\sf\medskip\begin{flushleft}
210
211\noindent\hspace*{0.00em}\textbf{unsigned} \textbf{char} search(\textbf{unsigned} \textbf{char} *tab, \textbf{unsigned} \textbf{char} size, \textbf{unsigned} \textbf{char} to\_{}find)~\linebreak
212\noindent\hspace*{0.00em}\{~\linebreak
213\noindent\hspace*{1.00em}\textbf{unsigned} \textbf{char} low, high, i;~\linebreak
214\noindent\hspace*{1.00em}\textcolor{red}{\_cost8:}~\linebreak
215\noindent\hspace*{1.00em}low = (\textbf{unsigned} \textbf{char})0;~\linebreak
216\noindent\hspace*{1.00em}high = (\textbf{unsigned} \textbf{char})((\textbf{int})size - 1);~\linebreak
217\noindent\hspace*{1.00em}\textbf{while} ((\textbf{int})high \ensuremath{\ge} (\textbf{int})low) \{~\linebreak
218\noindent\hspace*{2.00em}\textcolor{red}{\_cost6:}~\linebreak
219\noindent\hspace*{2.00em}i = (\textbf{unsigned} \textbf{char})(((\textbf{int})high + (\textbf{int})low) / 2);~\linebreak
220\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{==}} (\textbf{int})to\_{}find) \{  ~\linebreak
221\noindent\hspace*{4.00em}\textcolor{red}{\_cost4}\ensuremath{:~} \textbf{return} i; ~\linebreak
222\noindent\hspace*{2.00em}\} \textbf{else} \{\textcolor{red}{\_cost5:}  \}~\linebreak
223\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{>}} (\textbf{int})to\_{}find) \{ ~\linebreak
224\noindent\hspace*{3.00em}\textcolor{red}{\_cost2}\ensuremath{:~} high = (\textbf{unsigned} \textbf{char})((\textbf{int})i - 1); ~\linebreak
225\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost3}\ensuremath{:~}  \}~\linebreak
226\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{<}} (\textbf{int})to\_{}find) \{ ~\linebreak
227\noindent\hspace*{3.00em}\textcolor{red}{\_cost0}\ensuremath{:~} low = (\textbf{unsigned} \textbf{char})((\textbf{int})i + 1); ~\linebreak
228\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost1}\ensuremath{:~} \}~\linebreak
229\noindent\hspace*{1.00em}\}~\linebreak
230\noindent\hspace*{1.00em}\textcolor{red}{\_cost7}\ensuremath{:~}~\linebreak
231\noindent\hspace*{1.00em}\textbf{return} (\textbf{unsigned} \textbf{char})(-1);~\linebreak
232\noindent\hspace*{0.00em}\}
233\end{flushleft}\medskip\egroup\noindent
234\end{code}
235\end{frame}
236
237\begin{frame}
238\frametitle{A glimpse on the compiler passes : $RTL_{abs}$}
239
[662]240\begin{code}[7.5cm]
[655]241\bgroup\sf\medskip\begin{flushleft}
242
[662]243\noindent\hspace*{0.50em}"search"([\%{}9 ; \%{}8], [\%{}2], [\%{}3])\linebreak
244\noindent\hspace*{0.50em}\ensuremath{:~} ptr \ensuremath{\rightarrow} \textbf{int} \ensuremath{\rightarrow} \textbf{int} \ensuremath{\rightarrow} \textbf{int}~\linebreak
[655]245\noindent\hspace*{2.00em}locals\ensuremath{:~} ...~\linebreak
246\noindent\hspace*{2.00em}result\ensuremath{:~} [\%{}10]~\linebreak
247\noindent\hspace*{2.00em}stacksize\ensuremath{:~} 0~\linebreak
248\noindent\hspace*{2.00em}entry\ensuremath{:~} search40~\linebreak
249\noindent\hspace*{2.00em}exit\ensuremath{:~} search0~\linebreak
250\noindent\hspace*{0.00em}~\linebreak
251\noindent\hspace*{2.00em}search9\ensuremath{:~} lt [\%{}13], [\%{}3] -\ensuremath{\rightarrow} search8, search5~\linebreak
252\noindent\hspace*{2.00em}search8\ensuremath{:~} \textcolor{red}{emit \_cost0} -\ensuremath{\rightarrow} search7~\linebreak
253\noindent\hspace*{2.00em}search7\ensuremath{:~} imm [\%{}12], imm\_{}int 1 -\ensuremath{\rightarrow} search6~\linebreak
254\noindent\hspace*{2.00em}search6\ensuremath{:~} add [\%{}5], [\%{}7], [\%{}12] -\ensuremath{\rightarrow} search4~\linebreak
255\noindent\hspace*{2.00em}search5\ensuremath{:~} \textcolor{red}{emit \_cost1} -\ensuremath{\rightarrow} search4~\linebreak
256\noindent\hspace*{2.00em}search40\ensuremath{:~} \textcolor{red}{emit \_cost8} -\ensuremath{\rightarrow} search39~\linebreak
257\noindent\hspace*{2.00em}search4\ensuremath{:~} -\ensuremath{\rightarrow} search36~\linebreak
258\noindent\hspace*{2.00em}\emph{// ...}
259\end{flushleft}\medskip\egroup\noindent
260\end{code}
261\end{frame}
262
263\begin{frame}
264\frametitle{A glimpse on the compiler passes : 8051}
265
[662]266\begin{code}[7.5cm]\scriptsize
[655]267\bgroup\sf\medskip\begin{flushleft}
268
269\noindent\hspace*{1.00em}\emph{// ...}~\linebreak
270\noindent\hspace*{1.00em}317\ensuremath{:~}  nop                ;; 1  \_{}cost4~\linebreak
271\noindent\hspace*{1.00em}318\ensuremath{:~}  mov   002h, \#{}000h  ;; 3  ~\linebreak
272\noindent\hspace*{1.00em}321\ensuremath{:~}  mov   A, 002h      ;; 1  ~\linebreak
273\noindent\hspace*{1.00em}323\ensuremath{:~}  mov   005h, A      ;; 1  ~\linebreak
274\noindent\hspace*{1.00em}325\ensuremath{:~}  mov   A, 009h      ;; 1  ~\linebreak
275\noindent\hspace*{1.00em}327\ensuremath{:~}  mov   004h, A      ;; 1  ~\linebreak
276\noindent\hspace*{1.00em}329\ensuremath{:~}  mov   A, 000h      ;; 1  ~\linebreak
277\noindent\hspace*{1.00em}331\ensuremath{:~}  push  0E0h         ;; 2  ~\linebreak
278\noindent\hspace*{1.00em}333\ensuremath{:~}  mov   A, 001h      ;; 1  ~\linebreak
279\noindent\hspace*{1.00em}335\ensuremath{:~}  push  0E0h         ;; 2  ~\linebreak
280\noindent\hspace*{1.00em}337\ensuremath{:~}  mov   0E0h, \#{}004h  ;; 3  ~\linebreak
281\noindent\hspace*{1.00em}340\ensuremath{:~}  add   A, 006h      ;; 1  ~\linebreak
282\noindent\hspace*{1.00em}342\ensuremath{:~}  mov   006h, A      ;; 1  ~\linebreak
283\noindent\hspace*{1.00em}344\ensuremath{:~}  mov   0E0h, \#{}000h  ;; 3  ~\linebreak
284\noindent\hspace*{1.00em}347\ensuremath{:~}  addc  A, 007h      ;; 1  ~\linebreak
285\noindent\hspace*{1.00em}349\ensuremath{:~}  mov   007h, A      ;; 1  ~\linebreak
286\noindent\hspace*{1.00em}351\ensuremath{:~}  mov   A, 005h      ;; 1  ~\linebreak
287\noindent\hspace*{1.00em}353\ensuremath{:~}  mov   083h, A      ;; 1  ~\linebreak
288\noindent\hspace*{1.00em}355\ensuremath{:~}  mov   A, 004h      ;; 1  ~\linebreak
289\noindent\hspace*{1.00em}357\ensuremath{:~}  mov   082h, A      ;; 1  ~\linebreak
290\noindent\hspace*{1.00em}359\ensuremath{:~}  ret                ;; 2 
291\end{flushleft}\medskip\egroup\noindent
292\end{code}
293\end{frame}
294
295\begin{frame}
296\frametitle{Benchmarks}
297
298  \centering
299
300  \begin{tabular}{r|rrr}
301    & \texttt{gcc -O0} & \texttt{acc} & \texttt{gcc -O1} \\
302    \hline
303    \texttt{badsort} & 55.93 & 34.51 & 12.96 \\
304    \texttt{fib} & 76.24 & 34.28 & 45.68 \\
305    \texttt{mat\_det} & 163.42 & 156.20 & 54.76 \\ 
306    \texttt{min} & 12.21 & 16.25 & 3.95 \\
307    \texttt{quicksort} & 27.46 & 17.95 & 9.41 \\
308    \texttt{search} & 463.19 & 623.79 & 155.38 \\
309    \hline
310  \end{tabular}
311
312\end{frame}
313
314\begin{frame}
315\frametitle{Future work}
316
317\begin{itemize}
318
319\item Prototype maintenance, validation and testing.
320
321\item Integration of the 8051 specification (recently provided as
322  deliverable 4.1).
323
324\item Integration of the non-standard extensions of the C language consisting
325  of directives that specifies storage location (given that their semantics have
326  been addressed in deliverable 3.1).
327
328\item Integration of a preprocessor to encode 16 bits and 32 bits
329  integers into records of 8 bits integers.
330
331\item Improvement of instruction selection (but we will not sacrifice
332  conceptual simplicity to keep mechanized proofs manageable).
333
334\item Development of a {\tt Frama-C} plugin that will embed the compiler as
335  well as an algorithm to produce synthetic information on the execution of C
336  functions from the current cost annotations (which only give information about
337  constant time portions of code).
338
339\end{itemize}
340
341\end{frame}
342
343\end{document}
Note: See TracBrowser for help on using the repository browser.