source: Deliverables/D1.3/Presentations/WP1-claudio.tex @ 3296

Last change on this file since 3296 was 3296, checked in by sacerdot, 8 years ago

...

File size: 18.2 KB
Line 
1\documentclass{beamer}
2
3\usetheme{Frankfurt}
4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
5
6\usepackage{wasysym}
7\usepackage{amsfonts}
8\usepackage{amsmath}
9\usepackage{eurosym}
10\usepackage{amssymb}
11\usepackage[english]{babel}
12\usepackage{color}
13\usepackage[utf8x]{inputenc}
14\usepackage{listings}
15\usepackage{stmaryrd}
16\usepackage{fancyvrb}
17% \usepackage{microtype}
18
19\author{Claudio Sacerdoti Coen}
20\title{Certified Complexity (CerCo)\\
21       Overall Presentation and Project Management}
22\date{May 16, 2013}
23
24\setlength{\parskip}{1em}
25
26\AtBeginSection[]
27{
28  \begin{frame}<beamer>
29    \frametitle{Outline}
30    \tableofcontents[currentsection]
31  \end{frame}
32}
33
34\begin{document}
35
36\begin{frame}
37\maketitle
38\end{frame}
39
40\begin{frame}
41  \frametitle{Outline}
42  \tableofcontents
43\end{frame}
44
45\section{Long, middle and short term objectives}
46
47\begin{frame}
48 \frametitle{The ICT of the future: Programs}
49 We envision a (long term) future where formal methods will be pervasive:
50 \begin{center}
51   \alert{\Large Most programs will be (partially) specified and certified}
52 \end{center}
53
54 The very same definition of ``program'' will change:
55 \begin{center}
56  \alert{\Large A program will be a triple made of a specification,
57  an implementation and a proof certificate}
58 \end{center}
59
60 Cfr: Proof Carrying Code (PCC)
61\end{frame}
62
63\begin{frame}
64 \frametitle{The ICT of the future: the ITP point of view}
65 There is always a trade off between expressivity (precision) and
66 automation (partiality, abstraction).\\~\\
67
68 Interactive theorem proving perspective:
69   \alert{\Large
70   \begin{itemize}
71    \item Maximal expressivity (precision) in specification
72    \item Interactive proofs
73    \item Abstraction, loss of precision as special cases of specification
74    \item Automation as special cases of interaction
75   \end{itemize}
76   }
77\end{frame}
78
79\begin{frame}
80 \frametitle{The ICT of the future: Compilation}
81 In our long-term vision:
82 \begin{center}
83 \alert{\Large A compiler maps triples specification-implementation-certificate
84  to triples specification-implementation-certificate.}
85 \end{center}
86
87 What is investigated in CerCo:
88 \begin{center}
89 \alert{\Large Inclusion of intensional (non functional) properties into the
90  specification to enable high level but precise reasoning.}
91 \end{center}
92\end{frame}
93
94\begin{frame}
95 \frametitle{The ICT of the future: Difficulties}
96 Non functional properties (time, space, energy) are affected by:
97
98 \begin{itemize}
99  \item \alert{The compilation process} (which is not compositional)\\
100        E.g. the cost of different high level occurrences of the same
101        instruction is different.\\
102        E.g. aggressive optimizations that change the control flow
103  \item \alert{Hardware status} (caches, pipelines, branch prediction unit)
104 \end{itemize}
105
106 Questions and trade-offs:
107 \begin{itemize}
108  \item How much \alert{precision} can be achieved?
109  \item How \alert{complex} are precise cost models for advanced compilation
110        strategies and/or modern hardware?
111  \item How much complexity can be tamed by \alert{abstraction}\\
112        and automation at the source code level?
113 \end{itemize}
114\end{frame}
115
116\begin{frame}
117 \frametitle{The ICT of the future: Coping with the difficulties}
118
119 In the project timeframe:
120
121 \alert{We started with a simple scenario:}
122 \begin{itemize}
123  \item Conventional compilation model without changes to the control flow
124  \item Deterministic widely deployed hardware model (no caching, pipelining)
125 \end{itemize}
126
127 \alert{We provided a formal certification of preservation of the
128        non functional properties, modulo functional correctness}\\~\\
129
130 \alert{We have started to scale to most complex scenarios\\
131        (without certification).}\\~\\
132\end{frame}
133
134\begin{frame}
135 \frametitle{Short term objectives (achievements)}
136 \begin{enumerate}
137  \item develop a \alert{compiler} from
138        \alert{$\approx\!\!$ C} to \alert{MCS-51} processor
139        (1st period)
140  \item have the compiler infer from the assembly code a \alert{precise cost
141        model} for the source program (1st period)
142  \item \alert{certify} the preservation of non functional properties
143        by the compiler (3rd period, open proof obligations for
144        functional properties)
145  \item embed the compiler in a \alert{prototypical environment} for
146   \begin{itemize}
147    \item stating \alert{cost invariants} based on the inferred cost model
148    \item computing \alert{proof obligations}
149    \item \alert{proving} generated obligations automatically or interactively
150   \end{itemize}
151   (2nd period and 3rd period)
152  \item lift the technique to a \alert{synchronous language}
153        (2nd period)
154  \item \alert{Scale} the approach to \alert{more complex scenarios}
155        (loop optimizations in 2nd period, investigations on modern hardware
156         in 3rd period)
157 \end{enumerate}
158\end{frame}
159
160\begin{frame}
161 \frametitle{CerCo interaction diagram}
162 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
163\end{frame}
164
165\begin{frame}
166 \frametitle{Case study interaction diagram}
167 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
168\end{frame}
169
170\section{State at the end of second period}
171
172\begin{frame}
173 \frametitle{Achievements (2nd period)}
174 Main theoretical achievements (D2.1):
175 \begin{center}
176  \alert{A methodology (basic labelling approach) for lifting in a provably correct way costs on the object code to costs in the source code}\\
177 \end{center}
178
179 \begin{itemize}
180  \item Scaled to dependent labelling to cover optimizations that do not
181        preserve the control flow (D5.1)
182  \item Applied to imperative and functional languages (D5.1)
183  \item \alert{The proof did not cover function calls}
184 \end{itemize}
185\end{frame}
186
187\begin{frame}
188 \frametitle{Achievements (2nd period)}
189
190 Main practical achievements (1/2):
191  \alert{\begin{enumerate}
192   \item An untrusted compiler from C-Light to the MCS-51 processor
193   that implements the methodology (D2.2), also extended with
194   loop optimizations (D5.1)\\
195   \item Its formalization in Matita (D3.2, D4.2)\\
196   \item Formalized executable semantics for source, target and intermediate
197         languages (D3.1, D3.3, D4.1, D4.3)
198  \end{enumerate}}
199
200 \begin{itemize}
201  \item The code was not extracted
202  \item Not completely executable because of calls to untrusted code
203        (cfr. translation validation, but also parsing/pretty printing)
204  \item Code correct, not necessarily proof friendly
205 \end{itemize}
206\end{frame}
207
208\begin{frame}
209 \frametitle{Achievements (1st period)}
210
211 Main practical achievements (2/2):
212
213 \begin{center}
214  \alert{Implementation for the Frama-C platform of a cost invariant
215         synthesizer based on the CerCo's compiler (D5.1)}
216 \end{center}
217
218 \begin{itemize}
219  \item Considered only simple cases
220  \item Proof obligations produced by Jessie for the Why tool
221        (Why3 in development, Frama-C under significant rewriting too)
222 \end{itemize}
223\end{frame}
224
225\begin{frame}
226 \hspace{-5.5cm}\includegraphics[height=8cm]{figs/pert.pdf}
227\end{frame}
228
229\begin{frame}
230 \frametitle{Recommendations from the reviewers}
231  ``In order to not limit the results that can be obtained in the
232  project to processors with very old architectures \ldots the  project
233  partners  should  explicitly  consider  how  the  assumptions  on  the
234  hardware architecture influence the results obtained and in how far these
235  assumptions could be a threat to the validity and generality of the results''
236
237  Limiting assumptions for the basic labelling approach:
238  \begin{enumerate}
239   \item \alert{The compiler should not alter significantly the control flow}\\
240         Loss of precision and/or correctness
241   \item \alert{Existence of a function that associates a cost to each basic
242         block independently from the processor status}\\
243         Serious loss of precision
244  \end{enumerate}
245\end{frame}
246
247\begin{frame}
248 \frametitle{Recommendations from the reviewers}
249 Case study for the alteration of control flow:\\
250 \alert{loop optimizations} (peeling, unrolling)
251
252 Description:\\
253
254 \alert{in peeling/unrolling different iterations are compiled differently and
255 they receive a different cost}.
256
257 Alternative reading:\\
258 \alert{after peeling/unrolling the cost of an iteration is a function of the
259 program state (iteration number)}.
260
261 Symptom:\\
262 \alert{serious loss of precision} (if we take the maximum cost).
263
264 Solution sketched at the previous review:\\
265 \alert{dependent costs: the cost is a function of the state}
266\end{frame}
267
268\begin{frame}
269 \frametitle{Recommendations from the reviewers}
270 Case study for advanced hardware features:\\
271 \alert{cache}
272
273 Description:\\
274 \alert{using caches different iterations of a loop are executed with
275 a different cost}.
276
277 Alternative reading:\\
278 \alert{using caches the cost of an iteration is a function of the
279 processor state (cache)}.
280
281 Symptom:\\
282 \alert{serious loss of precision} (if we take the maximum cost).
283
284 Solution sketched at the previous review:\\
285 \alert{dependent costs: the cost is a function of the state}
286\end{frame}
287
288\begin{frame}
289 \frametitle{Recommendations from the reviewers}
290 The two scenarios are analogous, yet the first is simpler:\\
291 \begin{enumerate}
292  \item Loop optimization\\
293   \alert{program state always known and available in the source code}\\
294   Total precision can be achieved.\\
295   Problem: are the dependent annotations easy to understand and work with
296   (manually or automatically)? Probably yes
297 \item Cache\\
298   \alert{\makebox[0pt][l]{cache state only (?) approximated (via abstract interpretation)}}\\
299   Total precision impossible (?) to achieve\\
300   Problem: are the dependent annotations easy to understand and work
301   with? Open question
302 \end{enumerate}
303\end{frame}
304
305\begin{frame}
306 \frametitle{Recommendations from the reviewers: action taken}
307 Dr. Paolo Tranquilli hired at UNIBO at month 19 to
308 \begin{itemize}
309  \item Develop the dependent labelling approach (completed)
310  \item Apply it to the loop optimization scenarios (completed)
311  \item Apply it to the cache scenario (to be started)
312 \end{itemize}
313
314 Theoretical achievement:\\
315 \alert{dependent labelling approach} and pen\&paper certification of a toy
316 compiler based on it
317
318 Practical achievement:\\
319 Branch of all CerCo software (compiler, etc.) that implements
320 \alert{loop optimizations, redundancy elimination, improved constant
321 propagation}.
322\end{frame}
323
324\begin{frame}
325 \frametitle{Recommendations from the reviewers: action taken}
326 \alert{No impact on planning}\\
327 Dr. Tranquilli and Dr. Boender (Post-Docs) replaced the
328 senior researcher position which was made impossible during the first period.\\
329 ~\\
330
331 \alert{No impact on budget}\\
332 Minor delays so far on the project plan (Dr. Boender alone is less experienced
333 than the originally expected candidate)\\
334\end{frame}
335
336\begin{frame}
337 \frametitle{Recommendations from the reviewers}
338 ``The authors should quickly outline a paper-and-pencil correctness proof for
339   each of the seven stages \ldots in order to allow for an estimation of the
340   complexity and time required''~\\~\\
341
342 Done.
343 \begin{itemize}
344  \item This made explicit the need to consider \emph{structured traces}.\\
345        Not needed in the proof of the toy compiler.
346  \item The overall \alert{effort} required is \alert{consistent} with the
347        person-months allocated to the project.
348  \item The estimation is based on our \alert{judgement of the proof complexity} and on \alert{projections} obtained from code size and coefficients computed
349        from CompCert.
350 \end{itemize}
351\end{frame}
352
353\section{Project planning and achievements}
354
355\begin{frame}
356 \hspace{-5.5cm}\includegraphics[height=8cm]{figs/pert.pdf}
357\end{frame}
358
359\begin{frame}
360 \frametitle{Achievements (3rd period) (WP3/WP4 talks)}
361 From the \alert{formalized CerCo compiler} (2nd period)\\
362  ~~~ - untrusted code\\
363  ~~~ - not optimized for proving\\
364  ~~~ - with axiomatized fixpoint computer and\\
365  ~~~~~ graph colouring algorithm\\
366  ~~~ - with formalized semantics for intermediate languages\\~\\
367 to the \alert{trusted CerCo compiler} (3rd period) (WP5 talk)\\
368  ~~~ - \alert{extracted code} integrated with untrusted code\\
369  ~~~~~ from the untrusted prototype\\
370  ~~~ - preservation of costs (time + \alert{stack space}) \alert{certified}\\
371  ~~~~~ modulo preservation of functional properties
372\end{frame}
373
374\begin{frame}
375 \frametitle{Achievements (3rd period) (WP5 talk)}
376 From the \alert{untrusted CerCo prototype} (2nd period)\\
377 ~~~ - untrusted compiler +\\
378 ~~~~~ plug-in for Frama-C + Jessie + Why\\~\\
379 to the \alert{trusted CerCo prototype} (3rd period)\\
380 ~~~ - trusted/untrusted compiler +\\
381 ~~~~~ plug-in for \alert{experimental Frama-C + Jessie + Why3}\\
382 ~~~ - code simplification, \alert{better coverage}, integration with\\
383 ~~~~~ \alert{separation logic} to cover arrays\\
384 ~~~ - \alert{fine tuning of the generated invariants} to match\\
385 ~~~~~ the automatic provers expertises\\
386 ~~~ - a simplified interface for \alert{casual users}\\
387 ~~~ - testing\\
388 ~~~ - Debian packages + \alert{Live CD} for dissemination
389\end{frame}
390
391\begin{frame}
392 \frametitle{Achievements (3rd period) (second WP4 talk)}
393 \alert{Enlarging the scope} of CerCo techniques\\
394 ~~~ - application of the \alert{dependent labelling approach} to cover\\
395 ~~~~~ certain cost models that capture \alert{parametricity} of the cost\\
396 ~~~~~ on the \alert{internal state of hardware} components that is\\
397 ~~~~~ \alert{history dependent}\\
398 ~~~ - sufficient to deal with pipelines (further research required)\\
399 ~~~ - caches still problematic: towards \alert{probabilistic static analysis}?
400\end{frame}
401
402\begin{frame}
403 \frametitle{Other activities (3rd period) (WP6 talk)}
404 Organization of CerCo events targeted to potential industrial stakeholders
405 and the academic community.
406\end{frame}
407
408\begin{frame}
409 \frametitle{Assessment}
410 Assessment level and strategies:
411 \begin{enumerate}
412  \item Trusted CerCo compiler encoding: (D3.4/D4.4):\\
413    - extracted code \alert{tested};\\
414    - partially \alert{certified} using Matita\\
415  \item Trusted CerCo prototype (D5.2, D6.3, M3):\\
416    - tested (methodology + code) in the \alert{case study} (D5.3);\\
417    - tested on library of cryptographic functions (D6.3)\\
418  \item Case study: analysis of synchronous code (D5.3):\\
419   - \alert{self testing code} checks correctness and precision\\
420   - tested on examples
421 \end{enumerate}
422\end{frame}
423
424\begin{frame}
425 \frametitle{Deviations from DoW}
426 \alert{Minor deviations} from the DoW
427 (no significant impact on the schedule):
428 \begin{enumerate}
429  \item At month XXX (+XXX): submission of the
430    addenda required by the reviewers. \alert{Done}
431  \item Late delivery of D6.3 (at end of project, planned
432    at month XXX).\\
433    The source code of the Debian packages and the infrastructure for the
434    Live CD were ready on time, but the extracted code was changing because
435    of adjustments to the proofs.
436 \end{enumerate}
437\end{frame}
438
439\begin{frame}
440 \frametitle{Deviations from DoW}
441 \alert{Major deviations} from the DoW
442 \begin{enumerate}
443  \item DoW amended for administrative issues and to extend the length of
444        the projects by two months
445  \item Research on handling history sensitive hardware in response to
446        reviewers.\\
447    \alert{No impact on the schedule, work done by additional Post-Doc.}
448  \item Bring forward work on D5.3 from the third to the second period.\\
449    Enabled by replacement of PhD student by Post-Doc in Paris
450  \item Compared to the formal proof for the Why language, the one for C
451        revealed a \alert{much larger set of intensional invariants}
452        to be preserved; our \alert{contingency plan} dictated that we focused
453        on the aspects that
454        are novel of our approach. The proof was finally \alert{completed up to
455        proofs of functional correctness} already covered by existing projects.
456 \end{enumerate}
457\end{frame}
458
459\section{Project management}
460
461\begin{frame}
462 \frametitle{Management activities}
463 Management WP1:
464 \begin{enumerate}
465  \item \alert{coordinate and supervise} activities to be
466    carried out
467  \item carry out the overall \alert{administrative and
468    financial management} of the project
469  \item manage \alert{contacts with the European Commission}
470  \item \alert{monitor quality and timing} of project deliverables
471  \item establish effective internal and external
472        \alert{communication procedures}
473 \end{enumerate}
474\end{frame}
475
476\begin{frame}
477 \frametitle{Financial management and coordination}
478 During second period:
479 \begin{enumerate}
480  \item transmission \alert{pre-financing} to all beneficiaries
481  \item \alert{collecting and checking} partner's \alert{financial information} for the
482    Second Progress Report
483  \item \alert{submission of financial statement} through NEF system (in progress)
484  \item gathering all necessary information and submission of \alert{management
485   reports, activity reports and deliverables}
486 \end{enumerate}
487\end{frame}
488
489\begin{frame}
490 \frametitle{Periodic Meetings}
491 Three project meetings during 2nd period (one planned in DoW):
492 \begin{itemize}
493  \item Project meeting, Edinburgh, February 2011.\\
494   %Planning; review of decisions taken during implementor's meeting, discussion on the proof strategy and on the actions to be taken as an answer to the reviewer's recommendations.
495  \item Project meeting, Paris, September 2011.\\
496   \alert{Federated CerCo and Eternal meeting}
497   %(for dissemination and to establish co-operation). Review of deliverables due at month 18. Invited speaker from WCET community.
498  \item Implementer's meeting, Edinburgh, November 2011\\
499   %Discussion of issues found in the global proof strategy; introduction of the notion of structured traces and re-planning of the global proof strategy. Integration problems\\ addressed.
500 \end{itemize}
501\end{frame}
502
503\begin{frame}
504\begin{tabular}{lrlrr}
505Pass   & Lines & CompCert & Effort   & Effort \\
506Origin &       & ratio    & computed & adjusted \\
507\hline
508Common &  4864 & 4.25 \permil & 20.67 & 17.0 \\
509Clight &  1057 & 5.23 \permil & 5.53  &  6.0 \\
510Cminor &  1856 & 5.23 \permil & 9.71  & 10.0 \\ 
511RTLabs &  1252 & 1.17 \permil & 1.48  &  5.0 \\
512RTL    &   469 & 4.17 \permil & 1.95  &  2.0 \\
513ERTL   &   789 & 3.01 \permil & 2.38  & 2.5 \\
514LTL    &    92 & 5.94 \permil & 0.55  & 0.5 \\
515LIN    &   354 & 6.54 \permil & 2.31  &   1.0 \\
516ASM    &   984 & 4.80 \permil & 4.72  &  10.0 \\
517\hline
518Tot co &  4864 & 4.25 \permil & 20.67 & 17.0 \\
519Tot fe &  2913 & 5.23 \permil & 15.24 & 16.0 \\
520Tot be &  6853 & 4.17 \permil & 13.39 & 21.0 \\
521\hline
522Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
523\end{tabular}
524\end{frame}
525
526
527\end{document}
Note: See TracBrowser for help on using the repository browser.