source: Deliverables/D1.2/Presentations/WP1-claudio.tex @ 2097

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

...

File size: 20.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{March 16, 2012}
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 will formally certify the simple scenario}\\~\\
128
129 \alert{We have started to scale to most complex scenarios\\
130        (without certification).}\\~\\
131\end{frame}
132
133\begin{frame}
134 \frametitle{Short term objectives (achievements)}
135 \begin{enumerate}
136  \item develop a \alert{compiler} from
137        \alert{$\approx\!\!$ C} to \alert{MCS-51} processor
138        (1st period)
139  \item have the compiler infer from the assembly code a \alert{precise cost
140        model} for the source program (1st period)
141  \item \alert{certify} the compiler
142  \item embed the compiler in a \alert{prototypical environment} for
143   \begin{itemize}
144    \item stating \alert{cost invariants} based on the inferred cost model
145    \item computing \alert{proof obligations}
146    \item \alert{proving} generated obligations automatically or interactively
147   \end{itemize}
148   (partially in 2nd period)
149  \item lift the technique to a \alert{synchronous language}
150        (2nd period)
151  \item \alert{Scale} the approach to \alert{more complex scenarios}
152 \end{enumerate}
153\end{frame}
154
155\begin{frame}
156 \frametitle{CerCo interaction diagram}
157 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
158\end{frame}
159
160\begin{frame}
161 \frametitle{Case study interaction diagram}
162 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
163\end{frame}
164
165\section{State at the end of first period}
166
167\begin{frame}
168 \frametitle{Achievements (1st period)}
169 Main theoretical achievements (D2.1):
170 \begin{center}
171  \alert{\Large a methodology (basic labelling approach) for lifting in a provably correct way
172    costs on the object code to costs in the source code}\\
173 \end{center}~\\
174
175 Main practical achievements (D2.2):
176 \begin{center}
177  \alert{\Large an untrusted compiler from C-Light to the MCS-51 processor
178   that implements the methodology}
179 \end{center}
180\end{frame}
181
182\begin{frame}
183 \frametitle{Achievements (1st period)}
184 Preliminary work for future achievements (D3.1,D4.1):
185 \begin{center}
186  \alert{\Large formalized executable semantics for C-Light and the MCS-51
187   processor}
188 \end{center}
189\end{frame}
190
191\begin{frame}
192 \includegraphics[height=8cm]{figs/pert.pdf}
193\end{frame}
194
195\begin{frame}
196 \frametitle{Recommendations from the reviewers}
197  ``In order to not limit the results that can be obtained in the
198  project to processors with very old architectures \ldots the  project
199  partners  should  explicitly  consider  how  the  assumptions  on  the
200  hardware architecture influence the results obtained and in how far these
201  assumptions could be a threat to the validity and generality of the results''
202
203  Limiting assumptions for the basic labelling approach:
204  \begin{enumerate}
205   \item \alert{The compiler should not alter significantly the control flow}\\
206         Loss of precision and/or correctness
207   \item \alert{Existence of a function that associates a cost to each basic
208         block independently from the processor status}\\
209         Serious loss of precision
210  \end{enumerate}
211\end{frame}
212
213\begin{frame}
214 \frametitle{Recommendations from the reviewers}
215 Case study for the alteration of control flow:\\
216 \alert{loop optimizations} (peeling, unrolling)
217
218 Description:\\
219
220 \alert{in peeling/unrolling different iterations are compiled differently and
221 they receive a different cost}.
222
223 Alternative reading:\\
224 \alert{after peeling/unrolling the cost of an iteration is a function of the
225 program state (iteration number)}.
226
227 Symptom:\\
228 \alert{serious loss of precision} (if we take the maximum cost).
229
230 Solution sketched at the previous review:\\
231 \alert{dependent costs: the cost is a function of the state}
232\end{frame}
233
234\begin{frame}
235 \frametitle{Recommendations from the reviewers}
236 Case study for advanced hardware features:\\
237 \alert{cache}
238
239 Description:\\
240 \alert{using caches different iterations of a loop are executed with
241 a different cost}.
242
243 Alternative reading:\\
244 \alert{using caches the cost of an iteration is a function of the
245 processor state (cache)}.
246
247 Symptom:\\
248 \alert{serious loss of precision} (if we take the maximum cost).
249
250 Solution sketched at the previous review:\\
251 \alert{dependent costs: the cost is a function of the state}
252\end{frame}
253
254\begin{frame}
255 \frametitle{Recommendations from the reviewers}
256 The two scenarios are analogous, yet the first is simpler:\\
257 \begin{enumerate}
258  \item Loop optimization\\
259   \alert{program state always known and available in the source code}\\
260   Total precision can be achieved.\\
261   Problem: are the dependent annotations easy to understand and work with
262   (manually or automatically)? Probably yes
263 \item Cache\\
264   \alert{\makebox[0pt][l]{cache state only (?) approximated (via abstract interpretation)}}\\
265   Total precision impossible (?) to achieve\\
266   Problem: are the dependent annotations easy to understand and work
267   with? Open question
268 \end{enumerate}
269\end{frame}
270
271\begin{frame}
272 \frametitle{Recommendations from the reviewers: action taken}
273 Dr. Paolo Tranquilli hired at UNIBO at month 19 to
274 \begin{itemize}
275  \item Develop the dependent labelling approach (completed)
276  \item Apply it to the loop optimization scenarios (completed)
277  \item Apply it to the cache scenario (to be started)
278 \end{itemize}
279
280 Theoretical achievement:\\
281 \alert{dependent labelling approach} and pen\&paper certification of a toy
282 compiler based on it
283
284 Practical achievement:\\
285 Branch of all CerCo software (compiler, etc.) that implements
286 \alert{loop optimizations, redundancy elimination, improved constant
287 propagation}.
288\end{frame}
289
290\begin{frame}
291 \frametitle{Recommendations from the reviewers: action taken}
292 \alert{No impact on planning}\\
293 Dr. Tranquilli and Dr. Boender (Post-Docs) replaced the
294 senior researcher position which was made impossible during the first period.\\
295 ~\\
296
297 \alert{No impact on budget}\\
298 Minor delays so far on the project plan (Dr. Boender alone is less experienced
299 than the originally expected candidate)\\
300\end{frame}
301
302\begin{frame}
303 \frametitle{Recommendations from the reviewers}
304 ``we recommend to adapt the labelling approach such that basic complexity
305 annotations can be obtained  by  program  pieces  of  larger  granularity
306 than  is  done  now.  This  will  allow  \ldots  the  use  of WCET tools to
307 infer time bounds''
308\end{frame}
309
310\begin{frame}
311 \frametitle{Recommendations from the reviewers}
312 Suggested approach (EmBounded):
313 \begin{itemize}
314  \item \alert{Chunks} fed to the WCET tool and analyzed \alert{in isolation}
315  \item In isolation processor \alert{state unknown}
316        $\Rightarrow$ \alert{loss of precision}
317  \item Result of the analysis abstracted to \alert{one number} per chunk
318 \end{itemize}
319 Dependent labelling approach (\alert{CerCo}):
320 \begin{itemize}
321  \item \alert{Global analysis} of the object code
322        $\Rightarrow$ improved precision
323  \item Result of the analysis exposed via \alert{dependent costs}\\
324        $\Rightarrow$ \alert{improved precision}
325 \end{itemize}
326\end{frame}
327
328\begin{frame}
329 \frametitle{Recommendations from the reviewers: action taken}
330 Plan: to apply dependent labelling to caches.\\~\\
331
332 Reviewer's suggestion available as a fallback.
333\end{frame}
334
335\begin{frame}
336 \frametitle{Recommendations from the reviewers}
337 ``The authors should quickly outline a paper-and-pencil correctness proof for
338   each of the seven stages \ldots in order to allow for an estimation of the
339   complexity and time required''~\\~\\
340
341 Done.
342 \begin{itemize}
343  \item This made explicit the need to consider \emph{structured traces}.\\
344        Not needed in the proof of the toy compiler.
345  \item The overall \alert{effort} required is \alert{consistent} with the
346        person-months allocated to the project.
347  \item The estimation is based on our \alert{judgement of the proof complexity} and on \alert{projections} obtained from code size and coefficients computed
348        from CompCert.
349 \end{itemize}
350\end{frame}
351
352\begin{frame}
353 \frametitle{Recommendations from the reviewers}
354 ``Based on the outline of the paper-and-pencil proofs, the authors should
355 estimate the effort for two possible scenarios: a) proceed as planned in the
356 Matita system (this involves porting all proofs of the CompCert project to
357 Matita); b) modify the existing proofs in Coq\ldots If the project partners
358 stick to the usage of Matita they should argue convincingly why this is a
359 suitable choice and in how far Matita is superior to Coq\ldots''
360\end{frame}
361
362\begin{frame}
363 \frametitle{Recommendations from the reviewers: action taken}
364 \begin{enumerate}
365  \item Misconception: we \alert{do not} want to port/reuse CompCert proofs;
366        in any case CompCert \alert{licensing forbids} this
367  \item CerCo is first of all a project in certified compiler verification.
368   \alert{Comparing design alternatives is a key scientific contribution}\\~\\
369
370   \begin{tabular}{lll}
371     & CerCo & CompCert \\
372    Semantics & executable & inductive \\
373    Proofs     & computed proof obligations & traditional \\
374    Types      & dependent & ML \\
375    Datatypes  & graphs & lists \\
376    Semantics  & read-only program + pc & small step operational \\ 
377   \end{tabular}
378 \end{enumerate}
379\end{frame}
380
381\begin{frame}
382 \frametitle{Recommendations from the reviewers: action taken}
383 \begin{enumerate}
384  \item Commitment to the \alert{promotion of Matita}.
385  \item Exploiting implementation differences\\~\\
386   \begin{tabular}{lll}
387       & Matita & Coq \\
388    Small scale automation & unification hints & type classes \\
389    Big scale automation   & paramodulation & resolution \\
390    Tactics                & tinycals & LCF \\
391    Specifications         & executable & relational \\
392   \end{tabular}\\~\\
393  \item \alert{Co-development}:
394    when you have control of the tool, you can adapt the tool
395    instead of adapting the formalization
396 \end{enumerate}
397 Because of the previous motivations and the positive\\ outcome
398 of the effort estimation, \alert{we stick to original plan}.
399\end{frame}
400
401\section{Project planning and achievements}
402
403\begin{frame}
404 \includegraphics[height=8cm]{figs/pert.pdf}
405\end{frame}
406
407\begin{frame}
408 \frametitle{Achievements (2nd period) 1/3, Ayache}
409 From the \alert{CerCo annotating compiler} (1st period)\\
410 ~~~~~ - inference of costs for basic blocks;\\
411 ~~~~~ - instrumentation of the source code\\
412 to the \alert{CerCo untrusted prototype} (2nd period)\\
413 ~~~~~ - inference of cost invariants;\\
414 ~~~~~ - certified proofs of cost obligations;\\
415 \begin{enumerate}
416  \item Integration of the CerCo compiler into \alert{Frama-C} (D5.1)
417   \item The abstract interpretation based \alert{Frama-C CerCo plug-in} for
418     the inference of \alert{global complexity assertions} (D5.1)
419   \item The \alert{Lustre CerCo plug-in} for
420     automated analysis of WCRT (D5.3)
421 \end{enumerate}
422\end{frame}
423
424\begin{frame}
425 \frametitle{CerCo interaction diagram}
426 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
427\end{frame}
428
429\begin{frame}
430 \frametitle{Achievements (2nd period) 2/3, Mulligan/Campbell}
431 Towards the \alert{CerCo trusted prototype} (3rd period): to verify\\
432 ~~~ - preservation of labelled traces;\\
433 ~~~ - exact correspondence between actual and inferred cost\\
434 \begin{enumerate}
435  \item CIC encoding: Front/Back end (D4.2/D4.3)
436  \item \mbox{\rlap{Executable semantics of all intermediate languages (D3.3/D4.3)}}
437  \item Beginning of formal verification
438   \begin{itemize}
439    \item Common/generic definitions, \alert{data structures} to represent invariants,
440          \alert{invariants} enforced as dependent types
441    \item \alert{Optimizing assembler} verification (75\%)
442    \item Proof of \alert{correspondence} of actual and inferred cost (95\%)
443    \item Generation of \alert{structured} labelled traces (for
444          back-end)\\ from \alert{flat} labelled traces (from front-end)
445   \end{itemize}
446 \end{enumerate}
447\end{frame}
448
449\begin{frame}
450 \frametitle{Achievements (2nd period) 3/3 R\`egis-Gianas/Tranquilli}
451 \alert{Enlarging the scope} of CerCo techniques
452 \begin{enumerate}
453  \item Extension of the basic labelling approach to cover \alert{functional
454   languages} (D5.1)\\
455   - prototype implemented
456  \item Dependent labelling approach to cover \alert{control flow alterations}
457   and \alert{modern hardware features} (D5.1)\\
458   - branch of CerCo compiler with loop optimizations, redundancy elimination,
459     etc.
460 \end{enumerate}
461\end{frame}
462
463\begin{frame}
464 \frametitle{Assessment}
465 Assessment level and strategies:
466 \begin{enumerate}
467  \item CIC encoding: Front/Back end (D4.2/D4.3):\\
468    - \alert{tested} inside Matita (executable code);\\
469    - to be \alert{certified} in D3.4/D4.4 (Front/Back end correctness)
470  \item \makebox[0pt][l]{Executable semantics of intermediate languages
471    (D3.3/D4.3):}\\
472    \alert{tested} by executing programs
473  \item Untrusted CerCo prototype (D5.1, M2):\\
474    - tested (methodology + code) in the \alert{case study} (D5.3);\\
475    - plan to test on library of cryptographic functions
476  \item Case study: analysis of synchronous code (D5.3):\\
477   - \alert{self testing code} checks correctness and precision\\
478   - tested on examples
479 \end{enumerate}
480\end{frame}
481
482\begin{frame}
483 \frametitle{Deviations from DoW}
484 \alert{Minor deviations} from the DoW
485 (no significant impact on the future schedule):
486 \begin{enumerate}
487  \item At month 16 (+16): submission of the commitment letter and
488    addenda required by the reviewers. \alert{Done}
489  \item Late delivery of D4.2 delayed D3.2, D3.3, D4.3 (at month 21, planned
490    at month 18).\\ Bologna: one post-doc in place of senior researcher
491    (plus another on dependent labelling).\\
492    \alert{No short term impact, possible minor impact at month 36}
493 \end{enumerate}
494\end{frame}
495
496\begin{frame}
497 \hspace{-5cm}
498 \includegraphics[height=8cm]{figs/pert.pdf}
499\end{frame}
500
501\begin{frame}
502 \frametitle{Deviations from DoW}
503 \alert{Major deviations} from the DoW
504 \begin{enumerate}
505  \item Research on dependent labelling in response to reviewers.\\
506    \alert{No impact on the schedule, work done by additional Post-Doc.}
507  \item Bring forward D5.3 from the third to the second period.\\
508    D5.3 is a major case study to assess the potential
509    of CerCo technology $\Rightarrow$ \alert{early dissemination}.\\
510    Enabled by replacement of PhD student by Post-Doc in Paris\\~\\
511    {\Large \alert{We hereby officially require permission for\\
512    early delivery of D5.3 in second period}}
513 \end{enumerate}
514\end{frame}
515
516\begin{frame}
517 \hspace{-5cm}
518 \includegraphics[height=8cm]{figs/pert.pdf}
519\end{frame}
520
521\section{Project management}
522
523\begin{frame}
524 \frametitle{Management activities}
525 Management WP1:
526 \begin{enumerate}
527  \item \alert{coordinate and supervise} activities to be
528    carried out
529  \item carry out the overall \alert{administrative and
530    financial management} of the project
531  \item manage \alert{contacts with the European Commission}
532  \item \alert{monitor quality and timing} of project deliverables
533  \item establish effective internal and external
534        \alert{communication procedures}
535 \end{enumerate}
536\end{frame}
537
538\begin{frame}
539 \frametitle{Financial management and coordination}
540 During second period:
541 \begin{enumerate}
542  \item transmission \alert{pre-financing} to all beneficiaries
543  \item \alert{collecting and checking} partner's \alert{financial information} for the
544    Second Progress Report
545  \item \alert{submission of financial statement} through NEF system (in progress)
546  \item gathering all necessary information and submission of \alert{management
547   reports, activity reports and deliverables}
548 \end{enumerate}
549\end{frame}
550
551\begin{frame}
552 \frametitle{Periodic Meetings}
553 Three project meetings during 2nd period (one planned in DoW):
554 \begin{itemize}
555  \item Project meeting, Edinburgh, February 2011.\\
556   %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.
557  \item Project meeting, Paris, September 2011.\\
558   \alert{Federated CerCo and Eternal meeting}
559   %(for dissemination and to establish co-operation). Review of deliverables due at month 18. Invited speaker from WCET community.
560  \item Implementer's meeting, Edinburgh, November 2011\\
561   %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.
562 \end{itemize}
563\end{frame}
564
565\begin{frame}
566\begin{tabular}{lrlrr}
567Pass   & Lines & CompCert & Effort   & Effort \\
568Origin &       & ratio    & computed & adjusted \\
569\hline
570Common &  4864 & 4.25 \permil & 20.67 & 17.0 \\
571Clight &  1057 & 5.23 \permil & 5.53  &  6.0 \\
572Cminor &  1856 & 5.23 \permil & 9.71  & 10.0 \\ 
573RTLabs &  1252 & 1.17 \permil & 1.48  &  5.0 \\
574RTL    &   469 & 4.17 \permil & 1.95  &  2.0 \\
575ERTL   &   789 & 3.01 \permil & 2.38  & 2.5 \\
576LTL    &    92 & 5.94 \permil & 0.55  & 0.5 \\
577LIN    &   354 & 6.54 \permil & 2.31  &   1.0 \\
578ASM    &   984 & 4.80 \permil & 4.72  &  10.0 \\
579\hline
580Tot co &  4864 & 4.25 \permil & 20.67 & 17.0 \\
581Tot fe &  2913 & 5.23 \permil & 15.24 & 16.0 \\
582Tot be &  6853 & 4.17 \permil & 13.39 & 21.0 \\
583\hline
584Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
585\end{tabular}
586\end{frame}
587
588
589\end{document}
Note: See TracBrowser for help on using the repository browser.