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

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