source: Deliverables/D1.1/Presentations/management_and_overall-sacerdoti-presentation.tex @ 654

Last change on this file since 654 was 654, checked in by sacerdot, 9 years ago

In progress

File size: 16.3 KB
Line 
1\documentclass{beamer}
2
3\usetheme{Frankfurt}
4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
5
6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{amssymb}
9\usepackage[english]{babel}
10\usepackage{color}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{stmaryrd}
14\usepackage{fancyvrb}
15% \usepackage{microtype}
16
17\author{Claudio Sacerdoti Coen}
18\title{Certified Complexity (CerCo)\\
19       Overall Presentation and Project Managemnt}
20\date{March 11, 2011}
21
22\setlength{\parskip}{1em}
23
24\AtBeginSection[]
25{
26  \begin{frame}<beamer>
27    \frametitle{Outline}
28    \tableofcontents[currentsection]
29  \end{frame}
30}
31
32\begin{document}
33
34\begin{frame}
35\maketitle
36\end{frame}
37
38\section{Long, middle and short term objectives}
39
40\begin{frame}
41 \frametitle{The ICT of the future}
42 We envision a (long term) future where formal methods will be pervasive:
43 \begin{center}
44   \alert{\Large Most programs will be (partially) specified and certified}
45 \end{center}
46
47 The very same definition of ``program'' will change:
48 \begin{center}
49  \alert{\Large A program will be a triple made of a specification,
50  an implementation and a proof certificate}
51 \end{center}
52
53 Cfr: Proof Carrying Code (PCC)
54\end{frame}
55
56\begin{frame}
57 \frametitle{The ICT of the future}
58 Signals in this direction:
59
60 \begin{itemize}
61  \item Formal methods are more and more embraced in industry
62  \item If total certification remains mostly unfeasible,
63        techniques for pay-as-you-ride certification are reaching larger
64        audiences\\
65        (model checking, type systems, abstract interpretation, dependent
66         types, \ldots)
67  \item Larger varities of user-friendly tools for partial certifications\\
68        (termination checkers, WCET analyzers, source code analyzers based
69         on WP, \ldots)
70  \item New open tools that integrate collaborating plug-ins to perform
71        automatic or interactive analyses (e.g. Frama-C)
72 \end{itemize}
73\end{frame}
74
75\begin{frame}
76 \frametitle{The ICT of the future}
77 Compiler = a tool to translates programs
78  \alert{preserving something}\\~\\
79
80 In our long-term vision:
81 \begin{center}
82 \alert{\Large A compiler maps triples specification-implementation-certificate
83  to triples specification-implementation-certificate.}
84 \end{center}
85
86 Questions:
87 \begin{enumerate}
88  \item What properties are \alert{preserved} during compilation?
89  \item What properties are \alert{affected} by the compilation strategy?
90  \item To what extent can you trust your compiler in preserving those properties?
91 \end{enumerate}
92\end{frame}
93
94\begin{frame}
95 \frametitle{The ICT of the future}
96 Preservation of properties during compilation:
97 \begin{itemize}
98  \item Extensional properties are easily specifiable and easily preserved
99        during compilation, but \alert{only assuming infinite resources}
100  \item Little is known even foundationally on the
101        \alert{preservation of intensional properties}
102        (e.g. use of space, time, energy)
103  \item For sure \alert{compilation} (which is not compositional)
104        \alert{affects the intensional properties}\\
105        E.g. the cost of different occurrences of $x+1$ can be different
106  \item Hence \alert{how} can you \alert{specify} intensional properties
107        as a function of the compilation strategy?
108 \end{itemize}
109\end{frame}
110
111\begin{frame}
112 \frametitle{Long term theoretical objectives}
113 \begin{enumerate}
114  \item to study the \alert{specification} of intensional properties
115        under \alert{realistic and precise cost models} induced by the
116        compilation strategy
117  \item to study \alert{preservation} of extensional and intensional
118        properties (\alert{under finiteness assumption})
119 \end{enumerate}
120
121 Byproducts:
122 \begin{enumerate}
123  \item being able to prove the efficacity of optimizations
124  \item being able to state completeness of compilation under
125        finiteness assumptions
126 \end{enumerate}
127\end{frame}
128
129\begin{frame}
130 \frametitle{Long term practical objectives}
131 \begin{enumerate}
132  \item allow developers of \alert{(hard) real time systems} to comfortably
133    prove meeting of deadline on \alert{high level languages} with the guarantee
134    that they hold on the object code
135  \item allow developers of \alert{embedded systems} to reason on
136    \alert{resource consumption} on \alert{high level languages} with the same
137     guarantee
138  \item augment the \alert{precision of formal methods} for intensional
139    properties on high level languages
140  \item obtain a new generation of \alert{precise and fully trustable WCET}
141    analyzers
142 \end{enumerate}
143\end{frame}
144
145\begin{frame}
146 \frametitle{Short term objectives}
147 \begin{enumerate}
148  \item develop a \alert{compiler} from
149        \alert{$\approx\!\!$ C} to the \alert{MCS-51} microprocessor
150        used for embedded systems
151  \item have the compiler infer from the assembly code a \alert{precise cost
152        model} for the source program
153  \item \alert{certify} the compiler
154  \item embed the compiler in a \alert{prototypical environment} for
155   \begin{itemize}
156    \item stating \alert{cost invariants} based on the inferred cost model
157    \item computing \alert{proof obligations}
158    \item \alert{proving} automatically or interactively the generated proof obligations
159   \end{itemize}
160  \item lift the technique to a \alert{synchronous languaged} (e.g. Esterel)
161        compiled via C
162 \end{enumerate}
163\end{frame}
164
165\begin{frame}
166 \frametitle{CerCo interaction diagram}
167 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
168\end{frame}
169
170\begin{frame}[fragile]
171 \frametitle{Source code}
172\begin{Verbatim}[commandchars=\\\{\}]
173char search (char tab[], char size, char to_find) \{
174  char low = 0, high = size-1, i;
175
176  while (high >= low) \{
177    i = (high+low) / 2;
178    if (tab[i] == to_find) return i;
179
180    if (tab[i] > to_find) high = i-1;
181
182    if (tab[i] < to_find) low = i+1;
183
184  \}
185
186  return (-1);
187\}
188\end{Verbatim}
189\end{frame}
190
191\begin{frame}[fragile]
192 \frametitle{Instrumented source code}
193\begin{Verbatim}[commandchars=\\\{\}]
194char search (char tab[], char size, char to_find) \{
195  char low = 0, high = size-1, i;
196  \alert{cost_incr(117);}
197  while (high >= low) \{
198    \alert{cost_incr(77);}
199    i = (high+low) / 2;
200    if (tab[i] == to_find) \{\alert{cost_incr(30);} return i;\}
201    \alert{else cost_incr(103);}
202    if (tab[i] > to_find) \{\alert{cost_incr(98);} high = i-1;\}
203    \alert{else cost_incr(85);}
204    if (tab[i] < to_find) \{\alert{cost_incr(98);} low = i+1;\}
205    \alert{else cost_incr(88);}
206  \}
207  \alert{cost_incr(43);}
208  return (-1);
209\}
210\end{Verbatim}
211\end{frame}
212
213\begin{frame}[fragile]
214 \frametitle{Foreseen problems}
215 \begin{itemize}
216  \item The \alert{high level implicit control structures}
217    (e.g. missing \texttt{else}) must be made explicit
218  \item Additional \alert{low level control structures} must be made explicit\\
219    (e.g. add low bytes; if overflow then add high bytes)\\
220    Alternative: loss of precision
221  \item The \alert{guards} of the low level control structures could be
222    \alert{``unrelated''} to the high level data\\
223    (e.g. if the carry bit is set then \ldots else \ldots)
224  \item Optimizations can \alert{modify the control flow}\\
225    (e.g. loop hoisting and unrolling)
226  \item The cost can depend on the data manipulated (\alert{dependent annotations}) (e.g. shift, multiplication in simple microprocessors)
227  \item Precise information on the source code required to avoid total
228    alteration (e.g. comments)
229 \end{itemize}
230\end{frame}
231
232\begin{frame}[fragile]
233 \frametitle{Foreseen problems}
234 Strategy in CerCo:
235 \begin{enumerate}
236  \item We consider \alert{simple optimizations} that do not alter the control
237    flow (cfr. CompCert)\\
238    The study of control flow altering optimizations left as optional
239  \item Complex low level control flows \alert{encapsulated} in library
240    functions (if possible) or else \alert{precision loss} (not required yet)
241  \item \alert{Partial alteration of the source program} for justified reasons
242    (e.g. explicit CFs) and for temporary ones (reusal of the CIL suite)\\
243    \alert{To be refined in the next periods}
244 \end{enumerate}
245\end{frame}
246
247\begin{frame}[fragile]
248 \frametitle{Cost invariants: loose invariants}
249{\small
250\begin{Verbatim}[commandchars=\\\{\}]
251char search (char tab[], char size, char to_find) \{
252  char low = 0, high = size-1, i;
253  cost_incr(117);
254  \alert{/* @ label L}
255     \alert{@ invariant cost <= at(cost,L) +}
256      \alert{(77+103+98+88)*((at(high,L) - at(low,L))/(high - low))-1) */}
257  while (high >= low) \{
258    cost_incr(\alert{77});
259    i = (high+low) / 2;
260    if (tab[i] == to_find) \{cost_incr(\alert{30}); return i;\}
261    else cost_incr(\alert{103});
262    if (tab[i] > to_find) \{cost_incr(\alert{98}); high = i-1;\}
263    else cost_incr(\alert{85});
264    if (tab[i] < to_find) \{cost_incr(\alert{98}); low = i+1;\}
265    else cost_incr(\alert{88});
266  \}
267  cost_incr(43);
268  return (-1);
269\}
270\end{Verbatim}
271}
272\end{frame}
273
274\begin{frame}[fragile]
275 \frametitle{Cost invariants: precise invariants}
276 When needed the \alert{user} can also state a precise invariant:
277 \begin{Verbatim}[commandchars=\\\{\}]
278 \alert{cost = at(cost,L) +}
279   \alert{(77 + 103 + 98 + 85) * min(0,#iterations - 1) +}
280   \alert{if tab[(high+low)/2] == to_find then 30 else 103 +}
281   \alert{3 * #high_decremented}
282 \end{Verbatim}
283 where \verb+#high_decremented+ has a complex description.\\~\\
284
285 The more precise the invariant, the more knowledge is required on the
286 extensional semantics of the program.
287\end{frame}
288
289\begin{frame}[fragile]
290 \frametitle{Proof obligations for costs}
291 \alert{Proof obligations} are then generated from the cost invariants using standard
292 techniques (e.g. Weakest Precondition generators for Hoare logic)\\~\\
293
294 \begin{itemize}
295  \item Can use off-the-shelf WP generators
296  \item Ad-hoc tactics/proof strategies to handle the proof obligations will
297        probably help
298 \end{itemize}
299\end{frame}
300
301\begin{frame}
302 \frametitle{Other cost obligations}
303 The same technique applies to: space (stack, heap), energy, etc.\\~\\
304
305 But
306 \begin{center}
307   \alert{\Large space constraints have an effect on the\\extensional semantics too}\end{center}
308
309 Similarly
310 \begin{center}
311   \alert{\Large time constraints have an effect on the\\extensional semantics too when\\considering timers or I/O}\end{center}
312\end{frame}
313
314\begin{frame}
315 \frametitle{Other cost obligations and embedded systems}
316 In CerCo \alert{we have not committed} to other kinds of costs but time.\\~\\
317
318 \alert{Embedded and reactive systems} could greatly benefit from space
319 constraints and from time in presence of timers.\\~\\
320
321 Compatibly with the project timing and effort required, we would like to
322 experiment with other costs too.\\~\\
323
324 Otherwise, this will be left to \alert{future work}.
325\end{frame}
326
327\begin{frame}
328 \frametitle{Case study interaction diagram}
329 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
330\end{frame}
331
332\section{Project context}
333
334\begin{frame}
335 \frametitle{Related work}
336 \alert{Invariant generation} (also for termination)
337 \begin{itemize}
338  \item Automatic and assisted invariant discovery plays a \alert{central role}
339    for the long term objectives
340  \item Existing techniques are \alert{fully orthogonal} to CerCo: we provide
341    a realistic and precise cost model to be used for cost invariants
342  \item CerCo will \alert{guarantee} that the inferred intensional properties
343    will \alert{carry over to assembly code}
344 \end{itemize}
345\end{frame}
346
347\begin{frame}
348 \frametitle{Related work}
349 \alert{Worst Case Execution Time}
350 \begin{itemize}
351  \item Sophisticated techniques for computing approximate costs of
352    object code programs
353  \item Can target modern architectures (caches, pipelines, reordering of
354    instructions, \ldots) using \alert{static (precise) or dinamic (empyrical)
355    techniques}
356  \item Main problem: \alert{how to relate} analysis on object code to the
357    intermediate and source languages and \alert{how to trust} the results
358  \item In CerCo:
359   \begin{enumerate}
360    \item Costs are tightly related by designing \alert{compilers} with this aim
361     (cfr. wcc)
362    \item WCET computations are \alert{certified}
363    \item \alert{Interactivity} vs full automation
364   \end{enumerate}
365  \item CerCo will target only a simple architecture;\\ \alert{combination} with
366    (dynamic?) WCET \alert{necessary}\\ in the long term
367 \end{itemize}
368\end{frame}
369
370\begin{frame}
371 \frametitle{Related work}
372 \alert{Compiler certification and interactive theorem proving}
373 \begin{itemize}
374  \item A large and older litterature that focuses on academic examples
375  \item Some impressive recent examples that targets realistic
376    mildly optimizing compilers (e.g. CompCert, FR)
377  \item On-going projects that targets more complex scenarios:
378    intensional properties (CerCo, EU), whole software/hardware
379    architectures (e.g. VeriSoft, DE), concurrent systems (USA), \ldots
380 \end{itemize}
381\end{frame}
382
383\section{Project planning and achievements}
384
385\begin{frame}
386 \includegraphics[height=8cm]{figs/pert.pdf}
387\end{frame}
388
389\begin{frame}
390 \frametitle{Achievements (1st period)}
391 Main theoretical achievements (D2.1):
392 \begin{center}
393  \alert{\Large a methodology for lifting in a provably correct way
394    costs on the object code to costs in the source code}
395 \end{center}~\\
396
397 Main practical achievements (D2.2):
398 \begin{center}
399  \alert{\Large an untrusted compiler from C-Light to the MCS-51 microprocessor
400   that lifts costs on the object code to costs in the source code}
401 \end{center}
402\end{frame}
403
404\begin{frame}
405 \frametitle{Achievements (1st period)}
406 More in detail:
407 \begin{enumerate}
408  \item The methodology itself, with comparison with an alternative proposal.
409    Main issues:
410   \begin{enumerate}
411    \item meaning of cost annotations
412    \item method to prove them sound and precise
413    \item compositionality
414   \end{enumerate}
415  \item Assessment of the methodology: formalization of a toy compiler in Coq
416  \item First untrusted prototype from C-Light to Mips
417  \item Full formalization in O'Caml of the MCS-51 ``environment'':
418    \begin{enumerate}
419     \item ALU
420     \item UART, I/O lines, timers, interrupts
421     \item an assembly language with pseudo-instructions + an assembler
422     \item an Intel HEX parser/pretty printer
423    \end{enumerate}
424 \end{enumerate}
425\end{frame}
426
427\begin{frame}
428 \frametitle{Achievements (1st period)}
429 More in detail:
430 \begin{enumerate}
431  \item \alert{Partial} assessment of the MCS-51 O'Caml formalization
432  \item Extension of C, the CIL suite and the CompCert memory model to the
433    MCS-51 unorthogonal memory model (new type and pointer modifiers taken
434    from SDCC)
435  \item \alert{Partial} porting of the CerCo untrusted prototype to the
436    MCS-51 and to the extended C
437  \item Partial porting of the MCS-51 O'Caml formalization to Matita\\
438        The formalization is directly executable
439  \item Formalization in Matita of the extended C-Light version\\
440        The formalization is directly executable
441  \item \alert{Partial} assessment of the executable semantics by
442        proving it equivalent to the CompCert one (up to extensions)
443 \end{enumerate}
444\end{frame}
445
446\begin{frame}
447 \frametitle{Assessment}
448 Assessment level and strategies:
449 \begin{enumerate}
450  \item Untrusted CerCo compiler (D2.2, M1):\\
451    the compiler will be fully certified; several bugs already found after
452    the release of the deliverables
453  \item MCS-51 model (D4.1):\\
454    more thorough testing vs emulators and real processors is required;\\
455    minor impact on the rest of the projects;\\
456    the assembler will be certified (some bugs already found + unimplemented
457    features)
458  \item extended C semantics (D3.1):\\
459    already proved to be equivalent to the CompCert one (up to extensions);\\
460    we do not commit to support the planned extensions
461 \end{enumerate}
462\end{frame}
463
464\begin{frame}
465 \frametitle{Deviations from DoW}
466 Minor deviations from the DoW (no significant impact on the future schedule):
467 \begin{enumerate}
468  \item Late delivery of the deliverable related to the Web site and
469    internal work-flow due to hardware problems. \alert{Solved}
470  \item Compiler prototype D2.2 (M1):\\
471    computation of realistic costs requires full integration with D4.1
472    (not completed/tested at release time) \alert{Solved}
473  \item MCS-51 memory model + C extensions:\\
474    we did not foresee the need of MCS-51 specific extensions;\\
475    they will be taken in account with low priority\\
476    at the moment, only partially implemented in a branch of D2.2
477    not ready for release. \alert{Under consideration}
478 \end{enumerate}
479\end{frame}
480
481\begin{frame}
482 \frametitle{Foreseen deviations from DoW}
483\end{frame}
484
485\end{document}
Note: See TracBrowser for help on using the repository browser.