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

Last change on this file was 673, checked in by regisgia, 9 years ago
  • Cosmetics.
File size: 15.8 KB
Line 
1\documentclass[10pt]{beamer}
2\usetheme{Frankfurt}
3\logo{\includegraphics[height=1.0cm]{fetopen.png}}
4\usepackage[english]{babel}
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
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}
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{}
90\date{March $11$, 2011}
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
104  \includegraphics[width=\linewidth]{figs/diagram3.mps}
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{Benchmarks on the MIPS compiler}
126
127  \centering
128
129  \begin{tabular}{r|rrr}
130    & \texttt{gcc -O0} & \texttt{acc} & \texttt{gcc -O1} \\
131    \hline
132    \texttt{badsort} & 55.93 & 34.51 & 12.96 \\
133    \texttt{fib} & 76.24 & 34.28 & 45.68 \\
134    \texttt{mat\_det} & 163.42 & 156.20 & 54.76 \\ 
135    \texttt{min} & 12.21 & 16.25 & 3.95 \\
136    \texttt{quicksort} & 27.46 & 17.95 & 9.41 \\
137    \texttt{search} & 463.19 & 623.79 & 155.38 \\
138    \hline
139  \end{tabular}
140
141\end{frame}
142
143
144\begin{frame}
145\frametitle{Porting from MIPS to the 8051 microprocessor}
146
147Targetting the 8051 microprocessor raised the following issues:
148
149\begin{itemize}
150\item How to represent  32 bits values in an 8 bits architecture?
151\item How to deal with heterogeneous representation of pointers and integers?
152(Words are 8 bits long whereas memory addresses are stored using 16 bits.)
153\item How to select instructions for this microprocessor?
154\item What calling convention to use?
155\end{itemize}
156
157\end{frame}
158
159\begin{frame}
160\frametitle{Where was the difficulty in the prototype implementation?}
161
162The main issue in scaling our approach from the toy compiler to the C
163compiler was \textbf{function calls} because they add an extra
164complexity in the labelling process.
165
166
167\end{frame}
168
169\begin{frame}
170\frametitle{How to cover the control flow with cost labels?}
171
172  \centering
173
174  \bigskip
175
176  \only<1>{\includegraphics{figs/call1.mps}}
177  \only<2-3>{\includegraphics{figs/call2.mps}}
178
179  \bigskip
180  \medskip
181
182  \visible<3>{
183    \begin{block}{}
184      \centering
185      \textcolor{red}{Function pointer: statically unresolvable destination}
186
187      Each function should handle its cost.~\footnote{Notice that the
188        proof of the compiler will provide the invariant that function
189        pointers always only contain valid addresses to code generated
190        using the same compiler.}
191    \end{block}
192
193    \bigskip
194    \medskip
195
196    \includegraphics{figs/call3.mps}}
197
198\end{frame}
199
200
201\begin{frame}
202\frametitle{A glimpse on the compiler passes}
203
204\begin{code}[7.5cm]
205\bgroup\sf\medskip\begin{flushleft}
206
207\noindent\hspace*{0.00em}\textbf{char} search (\textbf{char} tab[], \textbf{char} size, \textbf{char} to\_{}find) \{~\linebreak
208\noindent\hspace*{1.00em}\textbf{char} low = 0, high = size-1, i;~\linebreak
209\noindent\hspace*{0.00em}~\linebreak
210\noindent\hspace*{1.00em}\textbf{while} (high \ensuremath{\ge} low) \{~\linebreak
211\noindent\hspace*{2.00em}i = (high+low) / 2;~\linebreak
212\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{==}} to\_{}find) \textbf{return} i;~\linebreak
213\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{>}} to\_{}find) high = i-1;~\linebreak
214\noindent\hspace*{2.00em}\textbf{if} (tab[i] {\scriptsize\ensuremath{<}} to\_{}find) low = i+1;~\linebreak
215\noindent\hspace*{1.00em}\}~\linebreak
216\noindent\hspace*{0.00em}~\linebreak
217\noindent\hspace*{1.00em}\textbf{return} (-1);~\linebreak
218\noindent\hspace*{0.00em}\}
219\end{flushleft}\medskip\egroup\noindent
220\end{code}
221\end{frame}
222
223
224
225\begin{frame}
226\frametitle{A glimpse on the compiler passes : Labelling in {\sc Clight}}
227
228\begin{code}[7.5cm]\scriptsize
229\bgroup\sf\medskip\begin{flushleft}
230
231\noindent\hspace*{0.00em}\textbf{unsigned} \textbf{char} search(\textbf{unsigned} \textbf{char} *tab, \textbf{unsigned} \textbf{char} size, \linebreak
232\noindent\hspace*{2.5cm}\textbf{unsigned} \textbf{char} to\_{}find)~\linebreak
233\noindent\hspace*{0.00em}\{~\linebreak
234\noindent\hspace*{1.00em}\textbf{unsigned} \textbf{char} low, high, i;~\linebreak
235\noindent\hspace*{1.00em}\textcolor{red}{\_cost8:}~\linebreak
236\noindent\hspace*{1.00em}low = (\textbf{unsigned} \textbf{char})0;~\linebreak
237\noindent\hspace*{1.00em}high = (\textbf{unsigned} \textbf{char})((\textbf{int})size - 1);~\linebreak
238\noindent\hspace*{1.00em}\textbf{while} ((\textbf{int})high \ensuremath{\ge} (\textbf{int})low) \{~\linebreak
239\noindent\hspace*{2.00em}\textcolor{red}{\_cost6:}~\linebreak
240\noindent\hspace*{2.00em}i = (\textbf{unsigned} \textbf{char})(((\textbf{int})high + (\textbf{int})low) / 2);~\linebreak
241\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{==}} (\textbf{int})to\_{}find) \{  ~\linebreak
242\noindent\hspace*{4.00em}\textcolor{red}{\_cost4}\ensuremath{:~} \textbf{return} i; ~\linebreak
243\noindent\hspace*{2.00em}\} \textbf{else} \{\textcolor{red}{\_cost5:}  \}~\linebreak
244\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{>}} (\textbf{int})to\_{}find) \{ ~\linebreak
245\noindent\hspace*{3.00em}\textcolor{red}{\_cost2}\ensuremath{:~} high = (\textbf{unsigned} \textbf{char})((\textbf{int})i - 1); ~\linebreak
246\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost3}\ensuremath{:~}  \}~\linebreak
247\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{<}} (\textbf{int})to\_{}find) \{ ~\linebreak
248\noindent\hspace*{3.00em}\textcolor{red}{\_cost0}\ensuremath{:~} low = (\textbf{unsigned} \textbf{char})((\textbf{int})i + 1); ~\linebreak
249\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost1}\ensuremath{:~} \}~\linebreak
250\noindent\hspace*{1.00em}\}~\linebreak
251\noindent\hspace*{1.00em}\textcolor{red}{\_cost7}\ensuremath{:~}~\linebreak
252\noindent\hspace*{1.00em}\textbf{return} (\textbf{unsigned} \textbf{char})(-1);~\linebreak
253\noindent\hspace*{0.00em}\}
254\end{flushleft}\medskip\egroup\noindent
255\end{code}
256\end{frame}
257
258\begin{frame}
259\frametitle{A glimpse on the compiler passes : $RTL_{abs}$}
260
261\begin{code}[7.5cm]
262\bgroup\sf\medskip\begin{flushleft}
263
264\noindent\hspace*{0.50em}"search"([\%{}9 ; \%{}8], [\%{}2], [\%{}3])\linebreak
265\noindent\hspace*{0.50em}\ensuremath{:~} ptr \ensuremath{\rightarrow} \textbf{int} \ensuremath{\rightarrow} \textbf{int} \ensuremath{\rightarrow} \textbf{int}~\linebreak
266\noindent\hspace*{2.00em}locals\ensuremath{:~} ...~\linebreak
267\noindent\hspace*{2.00em}result\ensuremath{:~} [\%{}10]~\linebreak
268\noindent\hspace*{2.00em}stacksize\ensuremath{:~} 0~\linebreak
269\noindent\hspace*{2.00em}entry\ensuremath{:~} search40~\linebreak
270\noindent\hspace*{2.00em}exit\ensuremath{:~} search0~\linebreak
271\noindent\hspace*{0.00em}~\linebreak
272\noindent\hspace*{2.00em}search9\ensuremath{:~} lt [\%{}13], [\%{}3] -\ensuremath{\rightarrow} search8, search5~\linebreak
273\noindent\hspace*{2.00em}search8\ensuremath{:~} \textcolor{red}{emit \_cost0} -\ensuremath{\rightarrow} search7~\linebreak
274\noindent\hspace*{2.00em}search7\ensuremath{:~} imm [\%{}12], imm\_{}int 1 -\ensuremath{\rightarrow} search6~\linebreak
275\noindent\hspace*{2.00em}search6\ensuremath{:~} add [\%{}5], [\%{}7], [\%{}12] -\ensuremath{\rightarrow} search4~\linebreak
276\noindent\hspace*{2.00em}search5\ensuremath{:~} \textcolor{red}{emit \_cost1} -\ensuremath{\rightarrow} search4~\linebreak
277\noindent\hspace*{2.00em}search40\ensuremath{:~} \textcolor{red}{emit \_cost8} -\ensuremath{\rightarrow} search39~\linebreak
278\noindent\hspace*{2.00em}search4\ensuremath{:~} -\ensuremath{\rightarrow} search36~\linebreak
279\noindent\hspace*{2.00em}\emph{// ...}
280\end{flushleft}\medskip\egroup\noindent
281\end{code}
282\end{frame}
283
284\begin{frame}
285\frametitle{A glimpse on the compiler passes : 8051}
286
287\begin{code}[7.5cm]\scriptsize
288\bgroup\sf\medskip\begin{flushleft}
289
290\begin{tabular}{ll}
291\noindent\hspace*{1.00em}\emph{// ...}~\\
292\noindent\hspace*{1.00em}\textcolor{gray}{317\ensuremath{:~}}  nop               
293&\textbf{;; 1  \textcolor{red}{\_{}cost4}}~\\
294\noindent\hspace*{1.00em}\textcolor{gray}{318\ensuremath{:~}}  mov   002h, \#{}000h &\textbf{;; 3  }~\\
295\noindent\hspace*{1.00em}\textcolor{gray}{321\ensuremath{:~}}  mov   A, 002h     &\textbf{;; 1  }~\\
296\noindent\hspace*{1.00em}\textcolor{gray}{323\ensuremath{:~}}  mov   005h, A     &\textbf{;; 1  }~\\
297\noindent\hspace*{1.00em}\textcolor{gray}{325\ensuremath{:~}}  mov   A, 009h     &\textbf{;; 1  }~\\
298\noindent\hspace*{1.00em}\textcolor{gray}{327\ensuremath{:~}}  mov   004h, A     &\textbf{;; 1  }~\\
299\noindent\hspace*{1.00em}\textcolor{gray}{329\ensuremath{:~}}  mov   A, 000h     &\textbf{;; 1  }~\\
300\noindent\hspace*{1.00em}\textcolor{gray}{331\ensuremath{:~}}  push  0E0h        &\textbf{;; 2  }~\\
301\noindent\hspace*{1.00em}\textcolor{gray}{333\ensuremath{:~}}  mov   A, 001h     &\textbf{;; 1  }~\\
302\noindent\hspace*{1.00em}\textcolor{gray}{335\ensuremath{:~}}  push  0E0h        &\textbf{;; 2  }~\\
303\noindent\hspace*{1.00em}\textcolor{gray}{337\ensuremath{:~}}  mov   0E0h, \#{}004h &\textbf{;; 3  }~\\
304\noindent\hspace*{1.00em}\textcolor{gray}{340\ensuremath{:~}}  add   A, 006h     &\textbf{;; 1  }~\\
305\noindent\hspace*{1.00em}\textcolor{gray}{342\ensuremath{:~}}  mov   006h, A     &\textbf{;; 1  }~\\
306\noindent\hspace*{1.00em}\textcolor{gray}{344\ensuremath{:~}}  mov   0E0h, \#{}000h &\textbf{;; 3  }~\\
307\noindent\hspace*{1.00em}\textcolor{gray}{347\ensuremath{:~}}  addc  A, 007h     &\textbf{;; 1  }~\\
308\noindent\hspace*{1.00em}\textcolor{gray}{349\ensuremath{:~}}  mov   007h, A     &\textbf{;; 1  }~\\
309\noindent\hspace*{1.00em}\textcolor{gray}{351\ensuremath{:~}}  mov   A, 005h     &\textbf{;; 1  }~\\
310\noindent\hspace*{1.00em}\textcolor{gray}{353\ensuremath{:~}}  mov   083h, A     &\textbf{;; 1  }~\\
311\noindent\hspace*{1.00em}\textcolor{gray}{355\ensuremath{:~}}  mov   A, 004h     &\textbf{;; 1  }~\\
312\noindent\hspace*{1.00em}\textcolor{gray}{357\ensuremath{:~}}  mov   082h, A     &\textbf{;; 1  }~\\
313\noindent\hspace*{1.00em}\textcolor{gray}{359\ensuremath{:~}}  ret               &\textbf{;; 2  }
314\end{tabular}
315\end{flushleft}\medskip\egroup\noindent
316\end{code}
317\end{frame}
318
319\begin{frame}
320\frametitle{A glimpse on the compiler passes : Annotating in {\sc Clight}}
321
322\begin{code}[7.5cm]\scriptsize
323\bgroup\sf\medskip\begin{flushleft}
324
325\noindent\hspace*{0.00em}\textbf{unsigned} \textbf{char} search(\textbf{unsigned} \textbf{char} *tab, \textbf{unsigned} \textbf{char} size, \linebreak
326\noindent\hspace*{2.5cm}\textbf{unsigned} \textbf{char} to\_{}find)~\linebreak
327\noindent\hspace*{0.00em}\{~\linebreak
328\noindent\hspace*{1.00em}\textbf{unsigned} \textbf{char} low, high, i;~\linebreak
329\noindent\hspace*{1.00em}\textcolor{red}{\_cost8:~\textbf{cost += 117;}} \linebreak
330\noindent\hspace*{1.00em}low = (\textbf{unsigned} \textbf{char})0;~\linebreak
331\noindent\hspace*{1.00em}high = (\textbf{unsigned} \textbf{char})((\textbf{int})size - 1);~\linebreak
332\noindent\hspace*{1.00em}\textbf{while} ((\textbf{int})high \ensuremath{\ge} (\textbf{int})low) \{~\linebreak
333\noindent\hspace*{2.00em}\textcolor{red}{\_cost6:~\textbf{cost += 77;}}~\linebreak
334\noindent\hspace*{2.00em}i = (\textbf{unsigned} \textbf{char})(((\textbf{int})high + (\textbf{int})low) / 2);~\linebreak
335\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{==}} (\textbf{int})to\_{}find) \{  ~\linebreak
336\noindent\hspace*{4.00em}\textcolor{red}{\_cost4\ensuremath{:~\textbf{cost += 30;}}} \textbf{return} i; ~\linebreak
337\noindent\hspace*{2.00em}\} \textbf{else} \{\textcolor{red}{\_cost5:~\textbf{cost += 103;}}  \}~\linebreak
338\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{>}} (\textbf{int})to\_{}find) \{ ~\linebreak
339\noindent\hspace*{3.00em}\textcolor{red}{\_cost2\ensuremath{:~\textbf{cost += 98;}}} high = (\textbf{unsigned} \textbf{char})((\textbf{int})i - 1); ~\linebreak
340\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost3\ensuremath{:~\textbf{cost += 85;}}}  \}~\linebreak
341\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{<}} (\textbf{int})to\_{}find) \{ ~\linebreak
342\noindent\hspace*{3.00em}\textcolor{red}{\_cost0\ensuremath{:~\textbf{cost += 98;}}} low = (\textbf{unsigned} \textbf{char})((\textbf{int})i + 1); ~\linebreak
343\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost1\ensuremath{:~\textbf{cost += 88;}}} \}~\linebreak
344\noindent\hspace*{1.00em}\}~\linebreak
345\noindent\hspace*{1.00em}\textcolor{red}{\_cost7\ensuremath{:~\textbf{cost += 43;}}}~\linebreak
346\noindent\hspace*{1.00em}\textbf{return} (\textbf{unsigned} \textbf{char})(-1);~\linebreak
347\noindent\hspace*{0.00em}\}
348\end{flushleft}\medskip\egroup\noindent
349\end{code}
350\end{frame}
351
352
353\begin{frame}
354\frametitle{Future work}
355
356\begin{itemize}
357
358\item Prototype maintenance, validation and testing.
359
360\item Integration of the 8051 specification (recently provided as
361  deliverable 4.1).
362
363\item Integration of the non-standard extensions of the C language consisting
364  of directives that specifies storage location (given that their semantics have
365  been addressed in deliverable 3.1).
366
367\item Integration of a preprocessor to encode 16 bits and 32 bits
368  integers into records of 8 bits integers.
369
370\item Improvement of instruction selection (but we will not sacrifice
371  conceptual simplicity to keep mechanized proofs manageable).
372
373\item Development of a {\tt Frama-C} plugin that will embed the compiler as
374  well as an algorithm to produce synthetic information on the execution of C
375  functions from the current cost annotations (which only give information about
376  constant time portions of code).
377
378\end{itemize}
379
380\end{frame}
381
382\end{document}
Note: See TracBrowser for help on using the repository browser.