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

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

Draft version completed.

File size: 19.1 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 \alert{academic examples}
375  \item Some impressive recent examples that targets \alert{realistic
376    mildly optimizing compilers} (e.g. CompCert, FR)
377  \item On-going projects that targets more \alert{complex scenarios}:
378    intensional properties (CerCo, EU), whole software/hardware
379    architectures (e.g. VeriSoft, DE), concurrent systems (USA),
380    higher level languages, \ldots
381 \end{itemize}
382\end{frame}
383
384\section{Project planning and achievements}
385
386\begin{frame}
387 \includegraphics[height=8cm]{figs/pert.pdf}
388\end{frame}
389
390\begin{frame}
391 \frametitle{Achievements (1st period)}
392 Main theoretical achievements (D2.1):
393 \begin{center}
394  \alert{\Large a methodology for lifting in a provably correct way
395    costs on the object code to costs in the source code}
396 \end{center}~\\
397
398 Main practical achievements (D2.2):
399 \begin{center}
400  \alert{\Large an untrusted compiler from C-Light to the MCS-51 microprocessor
401   that lifts costs on the object code to costs in the source code}
402 \end{center}
403\end{frame}
404
405\begin{frame}
406 \frametitle{Achievements (1st period)}
407 More in detail:
408 \begin{enumerate}
409  \item The \alert{methodology itself}, with comparison with an alternative proposal (D2.1).  Main issues:
410   \begin{enumerate}
411    \item meaning of cost annotations
412    \item method to prove them sound and precise
413    \item \alert{compositionality}
414   \end{enumerate}
415  \item Assessment of the methodology: formalization of a \alert{toy compiler in Coq}
416  \item First untrusted prototype from C-Light to Mips
417  \item Full \alert{formalization} in O'Caml of the \alert{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 \alert{Extension of C}, the CIL suite and the CompCert
433    \alert{memory model} to the MCS-51 unorthogonal memory model (new type and
434    pointer modifiers taken from SDCC)
435  \item \alert{Partial porting} of the CerCo untrusted prototype to the
436    MCS-51 and to the extended C
437  \item \alert{Partial porting} of the MCS-51 O'Caml formalization to Matita\\
438        The formalization is directly executable
439  \item \alert{Formalization} in Matita of the \alert{extended C-Light version}\\
440        The formalization is directly \alert{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 \alert{fully certified};
452    several bugs already found after
453    the release of the deliverables
454  \item MCS-51 model (D4.1):\\
455    \alert{more thorough testing} vs emulators and real processors is
456    required;\\
457    minor impact on the rest of the projects;\\
458    the assembler will be certified (some bugs already found + unimplemented
459    features)
460  \item extended C semantics (D3.1):\\
461    already \alert{proved to be equivalent} to the CompCert one
462    (up to extensions);\\
463    we do not commit to support the planned extensions
464 \end{enumerate}
465\end{frame}
466
467\begin{frame}
468 \frametitle{Deviations from DoW}
469 \alert{Minor deviations} from the DoW
470 (no significant impact on the future schedule):
471 \begin{enumerate}
472  \item Late delivery of the deliverable related to the Web site and
473    internal work-flow due to hardware problems. \alert{Solved}
474  \item Compiler prototype D2.2 (M1):\\
475    computation of realistic costs requires full integration with D4.1
476    (not completed/tested at release time) \alert{Solved}
477  \item MCS-51 memory model + C extensions:\\
478    we did not foresee the need of MCS-51 specific extensions;\\
479    they will be taken in account with low priority\\
480    at the moment, only partially implemented in a branch of D2.2
481    not ready for release. \alert{Under consideration}
482 \end{enumerate}
483\end{frame}
484
485\begin{frame}
486 \frametitle{Foreseen deviations from DoW}
487 All sites have faced different hiring problems.\\~\\
488
489  UNIBO (Project Coordinator).\\
490   \alert{Personel planned:} 1 post-doc (24m) + 1 RTD (non permanent researcher) 24m\\
491   \alert{Personel acquired:} 1 post-doc (24m)\\
492   \alert{Cause:}
493   Because of the reform of the Italian University it has not been possible
494   to hire a RTD yet and it is unlikely to be possible to hire him soon.\\
495   \alert{Solution:} in place of the RTD, we will acquire two post-docs
496   (24m + 18m) that will start later then expected and will have a lower
497   level of expertise. Both positions are still waiting for clarifications
498   from the ministry or approval from the Corte dei Conti.\\
499   \alert{Expected impact:} delivery of D4.2 (month 18) could\\
500   be delayed with no impact on the next milestone\\
501   (M2, month 24), potential impact on M3, month 36.
502\end{frame}
503
504\begin{frame}
505 \hspace{-5cm}
506 \includegraphics[height=8cm]{figs/pert.pdf}
507\end{frame}
508
509\begin{frame}
510 \frametitle{Foreseen deviations from DoW}
511 All sites have faced different hiring problems.\\~\\
512
513  UPD.\\
514   \alert{Personel planned:} 1 post-doc (12m) + 1 PhD student (36m) + master students\\
515   \alert{Personel acquired:} 1 post-doc (12m) + 1 phd student (6m) + 2 master students\\
516   \alert{Cause:}
517    After 6 months of work the PhD student has decided to resign.
518    At this point, it is neither possible (incomplete funding)
519    nor desirable (bootstrapping period) to look for another PhD
520    student.\\
521   \alert{Solution:}
522    We plan --- if possible --- to extend as much as
523    possible the post-doc to cover also the second and/or third period.\\
524   \alert{Expected impact:} no major expected impact.
525\end{frame}
526
527\begin{frame}
528 \frametitle{Foreseen deviations from DoW}
529 All sites have faced different hiring problems.\\~\\
530
531  UEDIN.\\
532   \alert{Personel planned:} 1 lecturer (36m) + 1 post-doc (36m) + 1 phd-student \\
533   \alert{Personel acquired:} 1 lecturer (14m) + Senior lecturer (24m) + 1 post-doc
534   \alert{Cause:}
535    Dr. Randy Pollack (former site leader) is moving to Harvard.
536    He will be employed 90\% of his time there and 10\% on CerCo at UEDIN.
537    Dr. Ian Stark is the new site leader (since 01 February).
538    No student with appropriate background was found.\\
539   \alert{Solution:}
540    We plan to hire a post-doc during the later part of the project to
541    compensate for the missing PhD student.\\
542   \alert{Expected impact:} some trading of person-months between projects
543    and reassignment of costs: an experienced researcher will be more expensive
544    than a PhD student, but could reasonably expect to carry out the formal
545    proof work in less time than a student.
546\end{frame}
547
548\end{document}
Note: See TracBrowser for help on using the repository browser.