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

Last change on this file since 672 was 672, checked in by regisgia, 9 years ago
  • Slides shuffling.
File size: 12.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  32bits values in an 8bits architecture?
151\item How to deal with heterogeneous representation of pointers and integers?
152(Words are 8bits long whereas memory addresses are stored using 16bits.)
153\item How to select instruction 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, \textbf{unsigned} \textbf{char} to\_{}find)~\linebreak
232\noindent\hspace*{0.00em}\{~\linebreak
233\noindent\hspace*{1.00em}\textbf{unsigned} \textbf{char} low, high, i;~\linebreak
234\noindent\hspace*{1.00em}\textcolor{red}{\_cost8:}~\linebreak
235\noindent\hspace*{1.00em}low = (\textbf{unsigned} \textbf{char})0;~\linebreak
236\noindent\hspace*{1.00em}high = (\textbf{unsigned} \textbf{char})((\textbf{int})size - 1);~\linebreak
237\noindent\hspace*{1.00em}\textbf{while} ((\textbf{int})high \ensuremath{\ge} (\textbf{int})low) \{~\linebreak
238\noindent\hspace*{2.00em}\textcolor{red}{\_cost6:}~\linebreak
239\noindent\hspace*{2.00em}i = (\textbf{unsigned} \textbf{char})(((\textbf{int})high + (\textbf{int})low) / 2);~\linebreak
240\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{==}} (\textbf{int})to\_{}find) \{  ~\linebreak
241\noindent\hspace*{4.00em}\textcolor{red}{\_cost4}\ensuremath{:~} \textbf{return} i; ~\linebreak
242\noindent\hspace*{2.00em}\} \textbf{else} \{\textcolor{red}{\_cost5:}  \}~\linebreak
243\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{>}} (\textbf{int})to\_{}find) \{ ~\linebreak
244\noindent\hspace*{3.00em}\textcolor{red}{\_cost2}\ensuremath{:~} high = (\textbf{unsigned} \textbf{char})((\textbf{int})i - 1); ~\linebreak
245\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost3}\ensuremath{:~}  \}~\linebreak
246\noindent\hspace*{2.00em}\textbf{if} ((\textbf{int})tab[i] {\scriptsize\ensuremath{<}} (\textbf{int})to\_{}find) \{ ~\linebreak
247\noindent\hspace*{3.00em}\textcolor{red}{\_cost0}\ensuremath{:~} low = (\textbf{unsigned} \textbf{char})((\textbf{int})i + 1); ~\linebreak
248\noindent\hspace*{2.00em}\} \textbf{else} \{ \textcolor{red}{\_cost1}\ensuremath{:~} \}~\linebreak
249\noindent\hspace*{1.00em}\}~\linebreak
250\noindent\hspace*{1.00em}\textcolor{red}{\_cost7}\ensuremath{:~}~\linebreak
251\noindent\hspace*{1.00em}\textbf{return} (\textbf{unsigned} \textbf{char})(-1);~\linebreak
252\noindent\hspace*{0.00em}\}
253\end{flushleft}\medskip\egroup\noindent
254\end{code}
255\end{frame}
256
257\begin{frame}
258\frametitle{A glimpse on the compiler passes : $RTL_{abs}$}
259
260\begin{code}[7.5cm]
261\bgroup\sf\medskip\begin{flushleft}
262
263\noindent\hspace*{0.50em}"search"([\%{}9 ; \%{}8], [\%{}2], [\%{}3])\linebreak
264\noindent\hspace*{0.50em}\ensuremath{:~} ptr \ensuremath{\rightarrow} \textbf{int} \ensuremath{\rightarrow} \textbf{int} \ensuremath{\rightarrow} \textbf{int}~\linebreak
265\noindent\hspace*{2.00em}locals\ensuremath{:~} ...~\linebreak
266\noindent\hspace*{2.00em}result\ensuremath{:~} [\%{}10]~\linebreak
267\noindent\hspace*{2.00em}stacksize\ensuremath{:~} 0~\linebreak
268\noindent\hspace*{2.00em}entry\ensuremath{:~} search40~\linebreak
269\noindent\hspace*{2.00em}exit\ensuremath{:~} search0~\linebreak
270\noindent\hspace*{0.00em}~\linebreak
271\noindent\hspace*{2.00em}search9\ensuremath{:~} lt [\%{}13], [\%{}3] -\ensuremath{\rightarrow} search8, search5~\linebreak
272\noindent\hspace*{2.00em}search8\ensuremath{:~} \textcolor{red}{emit \_cost0} -\ensuremath{\rightarrow} search7~\linebreak
273\noindent\hspace*{2.00em}search7\ensuremath{:~} imm [\%{}12], imm\_{}int 1 -\ensuremath{\rightarrow} search6~\linebreak
274\noindent\hspace*{2.00em}search6\ensuremath{:~} add [\%{}5], [\%{}7], [\%{}12] -\ensuremath{\rightarrow} search4~\linebreak
275\noindent\hspace*{2.00em}search5\ensuremath{:~} \textcolor{red}{emit \_cost1} -\ensuremath{\rightarrow} search4~\linebreak
276\noindent\hspace*{2.00em}search40\ensuremath{:~} \textcolor{red}{emit \_cost8} -\ensuremath{\rightarrow} search39~\linebreak
277\noindent\hspace*{2.00em}search4\ensuremath{:~} -\ensuremath{\rightarrow} search36~\linebreak
278\noindent\hspace*{2.00em}\emph{// ...}
279\end{flushleft}\medskip\egroup\noindent
280\end{code}
281\end{frame}
282
283\begin{frame}
284\frametitle{A glimpse on the compiler passes : 8051}
285
286\begin{code}[7.5cm]\scriptsize
287\bgroup\sf\medskip\begin{flushleft}
288
289\noindent\hspace*{1.00em}\emph{// ...}~\linebreak
290\noindent\hspace*{1.00em}317\ensuremath{:~}  nop                ;; 1  \_{}cost4~\linebreak
291\noindent\hspace*{1.00em}318\ensuremath{:~}  mov   002h, \#{}000h  ;; 3  ~\linebreak
292\noindent\hspace*{1.00em}321\ensuremath{:~}  mov   A, 002h      ;; 1  ~\linebreak
293\noindent\hspace*{1.00em}323\ensuremath{:~}  mov   005h, A      ;; 1  ~\linebreak
294\noindent\hspace*{1.00em}325\ensuremath{:~}  mov   A, 009h      ;; 1  ~\linebreak
295\noindent\hspace*{1.00em}327\ensuremath{:~}  mov   004h, A      ;; 1  ~\linebreak
296\noindent\hspace*{1.00em}329\ensuremath{:~}  mov   A, 000h      ;; 1  ~\linebreak
297\noindent\hspace*{1.00em}331\ensuremath{:~}  push  0E0h         ;; 2  ~\linebreak
298\noindent\hspace*{1.00em}333\ensuremath{:~}  mov   A, 001h      ;; 1  ~\linebreak
299\noindent\hspace*{1.00em}335\ensuremath{:~}  push  0E0h         ;; 2  ~\linebreak
300\noindent\hspace*{1.00em}337\ensuremath{:~}  mov   0E0h, \#{}004h  ;; 3  ~\linebreak
301\noindent\hspace*{1.00em}340\ensuremath{:~}  add   A, 006h      ;; 1  ~\linebreak
302\noindent\hspace*{1.00em}342\ensuremath{:~}  mov   006h, A      ;; 1  ~\linebreak
303\noindent\hspace*{1.00em}344\ensuremath{:~}  mov   0E0h, \#{}000h  ;; 3  ~\linebreak
304\noindent\hspace*{1.00em}347\ensuremath{:~}  addc  A, 007h      ;; 1  ~\linebreak
305\noindent\hspace*{1.00em}349\ensuremath{:~}  mov   007h, A      ;; 1  ~\linebreak
306\noindent\hspace*{1.00em}351\ensuremath{:~}  mov   A, 005h      ;; 1  ~\linebreak
307\noindent\hspace*{1.00em}353\ensuremath{:~}  mov   083h, A      ;; 1  ~\linebreak
308\noindent\hspace*{1.00em}355\ensuremath{:~}  mov   A, 004h      ;; 1  ~\linebreak
309\noindent\hspace*{1.00em}357\ensuremath{:~}  mov   082h, A      ;; 1  ~\linebreak
310\noindent\hspace*{1.00em}359\ensuremath{:~}  ret                ;; 2 
311\end{flushleft}\medskip\egroup\noindent
312\end{code}
313\end{frame}
314
315
316\begin{frame}
317\frametitle{Future work}
318
319\begin{itemize}
320
321\item Prototype maintenance, validation and testing.
322
323\item Integration of the 8051 specification (recently provided as
324  deliverable 4.1).
325
326\item Integration of the non-standard extensions of the C language consisting
327  of directives that specifies storage location (given that their semantics have
328  been addressed in deliverable 3.1).
329
330\item Integration of a preprocessor to encode 16 bits and 32 bits
331  integers into records of 8 bits integers.
332
333\item Improvement of instruction selection (but we will not sacrifice
334  conceptual simplicity to keep mechanized proofs manageable).
335
336\item Development of a {\tt Frama-C} plugin that will embed the compiler as
337  well as an algorithm to produce synthetic information on the execution of C
338  functions from the current cost annotations (which only give information about
339  constant time portions of code).
340
341\end{itemize}
342
343\end{frame}
344
345\end{document}
Note: See TracBrowser for help on using the repository browser.