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

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

First version.

File size: 22.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 (precison) in the 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 Simple compilation model (no changes to the control flow)
124  \item Trivial hardware model
125 \end{itemize}
126
127 \alert{We will formally certify the trivial 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}
135 \begin{enumerate}
136  \item develop a \alert{compiler} from
137        \alert{$\approx\!\!$ C} to the \alert{MCS-51} microprocessor
138        used for embedded systems (achieved in 1st period)
139  \item have the compiler infer from the assembly code a \alert{precise cost
140        model} for the source program (achieved in 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} automatically or interactively the generated proof obligations
147   \end{itemize}
148   (partially achieved in 2nd period)
149  \item lift the technique to a \alert{synchronous languages} (e.g. Esterel)
150        compiled via C (achieved in 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 microprocessor
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   microprocessor}
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 imagined 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 imagined 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{the program state is always known and availale on 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{the cache state can only (?) be 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 We hired Dr. Paolo Tranquilli (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 Impact on the project planning:\\~\\
293
294 Dr. Tranquilli and Dr. Boender (Post-Docs) were hired by UNIBO in place of the
295 senior researcher whose hiring was made impossible during the first period.\\
296 ~\\
297
298 No impact on the budget\\
299 Minor delays so far on the project plan (Dr. Boender alone is less experienced
300 than the originally expected candidate)\\
301\end{frame}
302
303\begin{frame}
304 \frametitle{Recommendations from the reviewers}
305 ``we recommend to adapt the labelling approach such that basic complexity
306 annotations can be obtained  by  program  pieces  of  larger  granularity
307 than  is  done  now.  This  will  allow  \ldots  the  use  of WCET tools to
308 infer time bounds''
309\end{frame}
310
311\begin{frame}
312 \frametitle{Recommendations from the reviewers}
313 Approach surely feasible and already followed in the EmBounded EU Project:
314 \begin{itemize}
315  \item the compiler informs the WCET tool about high level constraints on the
316   control flow
317  \item the WCET tool performs a fine grained analysis (e.g. by total unrolling
318   the loops) assuming a given processor state (e.g. empty cache)
319  \item the WCET tool abstracts the analysis to a number (the bound,
320   independent from the program status) that is returned
321  \item additional code must be generated to put the processor in the assumed
322   state to avoid caching anomalies
323 \end{itemize}
324\end{frame}
325
326\begin{frame}
327 \frametitle{Recommendations from the reviewers}
328 Comparison with dependent labelling:\\~\\
329
330  Dependent labelling does not use WCET tools as black-boxes;\\
331  it tightly integrates with WCET tools
332   \begin{itemize}
333    \item Pro: processor state exchanged in input/output, no need for a fixed
334     input state $\Rightarrow$ better precision
335    \item Pro: all details of the analysis exploited (instead of abstracting
336     to a single bound) $\Rightarrow$ better precision
337    \item Pro: it follows the interactive theorem proving perspective
338     (abstraction/automation are performed later)
339    \item Cons: require a re-implementation/modification of existing WCET
340     tools
341   \end{itemize}
342\end{frame}
343
344\begin{frame}
345 \frametitle{Recommendations from the reviewers: action taken}
346 We plan to continue the study of dependent labelling to accomodate caches.\\~\\
347
348 We will follow the reviewer's suggestion only as last resort in case of
349 failure.
350\end{frame}
351
352\begin{frame}
353 \frametitle{Recommendations from the reviewers}
354 ``The authors should quickly outline a paper-and-pencil correctness proof for
355   each of the seven stages \ldots in order to allow for an estimation of the
356   complexity and time required''~\\~\\
357
358 Done.
359 \begin{itemize}
360  \item A major issue with the proof plan has been found.\\
361        The issue was not there for the toy compiler and thus went unnoticed.\\
362        Solved introducing \emph{structured traces}.
363  \item The overall effort required is consistent with the men-months allocated
364        to the project.
365  \item The estimation is based on our perception of the proof complexity and
366        on projections obtained from code size and coefficients computed
367        from CompCert.
368 \end{itemize}
369\end{frame}
370
371\begin{frame}
372\begin{tabular}{lrlrr}
373Pass   & Lines & CompCert & Effort   & Effort \\
374Origin &       & ratio    & computed & adjusted \\
375\hline
376Common &  4864 & 4.25 \permil & 20.67 & 17.0 \\
377Clight &  1057 & 5.23 \permil & 5.53  &  6.0 \\
378Cminor &  1856 & 5.23 \permil & 9.71  & 10.0 \\ 
379RTLabs &  1252 & 1.17 \permil & 1.48  &  5.0 \\
380RTL    &   469 & 4.17 \permil & 1.95  &  2.0 \\
381ERTL   &   789 & 3.01 \permil & 2.38  & 2.5 \\
382LTL    &    92 & 5.94 \permil & 0.55  & 0.5 \\
383LIN    &   354 & 6.54 \permil & 2.31  &   1.0 \\
384ASM    &   984 & 4.80 \permil & 4.72  &  10.0 \\
385\hline
386Tot co &  4864 & 4.25 \permil & 20.67 & 17.0 \\
387Tot fe &  2913 & 5.23 \permil & 15.24 & 16.0 \\
388Tot be &  6853 & 4.17 \permil & 13.39 & 21.0 \\
389\hline
390Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
391\end{tabular}
392\end{frame}
393
394\begin{frame}
395 \frametitle{Recommendations from the reviewers}
396 ``Based on the outline of the paper-and-pencil proofs, the authors should
397 estimate the effort for two possible scenarios: a) proceed as planned in the
398 Matita system (this involves porting all proofs of the CompCert project to
399 Matita); b) modify the existing proofs in Coq\ldots If the project partners
400 stick to the usage of Matita they should argue convincingly why this is a
401 suitable choice and in how far Matita is superior to Coq\ldots''
402\end{frame}
403
404\begin{frame}
405 \frametitle{Recommendations from the reviewers: action taken}
406 \begin{enumerate}
407  \item CompCert proofs are not open source; the proposal was aiming to
408   a realistic mildly optimizing open source compiler
409  \item CerCo is first of all a project in certified compiler verification.
410   We wanted to experiment with different design choices
411   \begin{itemize}
412    \item Executable (CerCo) vs non executable (CompCert) semantics
413    \item Russell (Program) style proofs (CerCo) vs inductive reasoning (CompCert)
414    \item Dependent types (CerCo) vs simple (ML) types (CompCert)
415    \item Different program representations: graphs (Cerco) vs linear (CompCert)
416    \item Different semantics: read-only program + pc (CerCo) vs small operational semantics (CompCert)
417    \item Different back-ends (order of passes, etc.)
418   \end{itemize}
419  We do not claim to be always better: we want to\\ compare.
420 \end{enumerate}
421\end{frame}
422
423\begin{frame}
424 \frametitle{Recommendations from the reviewers: action taken}
425 \begin{enumerate}
426  \item One partner really interested in the promotion and co-development
427    of Matita.\\
428    Coq and Matita are incomparable (not clones). Examples:
429   \begin{itemize}
430    \item Type classes (Coq) vs unification hints (Matita)
431    \item Different tactic language: LCF (Coq) vs tinycals (Matita)
432    \item Different automation: ad-hoc (Coq) vs paramodulation based (Matita)
433    \item Coq favors inductive types, Matita executable definitions
434   \end{itemize}
435  \item Co-development:
436    When you have control of the tool, you can adapt the tool
437    instead of adapting the formalization
438 \end{enumerate}
439 Because of the previous motivations and the positive outcome (feasibility)
440 of the effort estimation, \alert{we keep following\\ the original plan}.
441\end{frame}
442
443\section{Project planning and achievements}
444
445\begin{frame}
446 \includegraphics[height=8cm]{figs/pert.pdf}
447\end{frame}
448
449\begin{frame}
450 \frametitle{Achievements (2nd period)}
451 From the \alert{CerCo annotating compiler} (1st period)\\
452 ~~~~~ - inference of costs for basic blocks;\\
453 ~~~~~ - instrumentation of the source code\\
454 to the \alert{CerCo untrusted prototype} (2nd period)\\
455 ~~~~~ - inference of cost invariants;\\
456 ~~~~~ - certified proofs of cost obligations;\\
457 \begin{enumerate}
458  \item Integration of the CerCo compiler into Frama-C to perform
459    \alert{totally trusted} proofs of intentional properties (D5.1)
460   \item The Abstract Interpretation based \alert{Frama-C CerCo plug-in} for
461     the inference of complexity assertions (D5.1)\\
462     A partially automatic simple but fully trusted WCET analyzer
463   \item The \alert{Lustre CerCo plug-in} for
464     the inference of complexity assertions (D5.3)\\
465     An automatic simple but fully trusted WCRT analyzer
466 \end{enumerate}
467\end{frame}
468
469\begin{frame}
470 \frametitle{CerCo interaction diagram}
471 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
472\end{frame}
473
474\begin{frame}
475 \frametitle{Case study interaction diagram}
476 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
477\end{frame}
478
479
480\begin{frame}
481 \frametitle{Achievements (2nd period)}
482 Towards the \alert{CerCo trusted prototype} (3rd period)\\
483 ~~~~~ - formal verification of the preservation of (structured)\\
484 ~~~~~ labelled traces;\\
485 ~~~~~ formal verification of correspondence between the actual\\
486 ~~~~~ - execution time (of object code) and the one predicted from\\
487 ~~~~~ (structured) labelled traces (all languages);\\
488 \begin{enumerate}
489  \item CIC encoding: Front/Back end (D4.2/D4.3)
490  \item Executable formal semantics of front/back end intermediate languages
491    (D3.3/D4.3)
492  \item Beginning of formal verification
493   \begin{itemize}
494    \item Common/generic definitions, data structures to represent invariants,
495          invariants enforced as dependent types
496    \item Optimizing assembler verification (75\%)
497    \item Proof of precise correspondence of real and estimated cost (95\%)
498    \item Generation of structured labelled traces (for the back-end) from
499          flat labelled traces (from the front-end)
500   \end{itemize}
501 \end{enumerate}
502\end{frame}
503
504\begin{frame}
505 \frametitle{Achievements (2nd period)}
506 Enlarging the scope of CerCo techniques
507 \begin{enumerate}
508  \item Extension of the basic labelling approach to cover functional
509   languages (D5.1)\\
510   - prototype implemented
511  \item Dependent labelling approach to cover control flow alterations
512   and modern hardware features (D5.1)\\
513   - branch of CerCo compiler with loop optimizations, redundancy elimination,
514     etc.
515 \end{enumerate}
516\end{frame}
517
518\begin{frame}
519 \frametitle{Assessment}
520 Assessment level and strategies:
521 \begin{enumerate}
522  \item CIC encoding: Front/Back end (D4.2/D4.3):\\
523    - tested inside Matita (executable code);\\
524    - to be certified in D3.4/D4.4 (Front/Back end correctness)
525  \item Executable formal semantics of front/back end intermediate languages
526    (D3.3/D4.3):\\
527    tested by executing programs
528  \item Untrusted CerCo prototype (D5.1, M2):\\
529    - tested (methodology + code) in the case study (D5.3);\\
530    - plan to test on library of cryptographic functions
531  \item Case study: analysis of syncrhonous code (D5.3):\\
532   - self testing code to check correctness and estimate\\ precision
533   - tested on some examples
534 \end{enumerate}
535\end{frame}
536
537\begin{frame}
538 \frametitle{Deviations from DoW}
539 \alert{Minor deviations} from the DoW
540 (no significant impact on the future schedule):
541 \begin{enumerate}
542  \item At month 16 (+16): submission of the commitment letter and
543    addenda required by the reviewers. \alert{Done}
544  \item Late delivery of D3.2, D3.3, D4.2, D4.3 (at month 21, planned
545    at month 18). Bologna hired two Post-Docs in place of a senior
546    researcher. One Post-Doc allocated to the dependent labelling approach.
547    The other has a lower level of maturity than expected. Thus we faced
548    a delay in D4.2 and D4.3 that reflected on D3.2 and D3.3 (for integration).
549    \alert{No short term impact, possible minor impact at month 36}
550 \end{enumerate}
551\end{frame}
552
553\begin{frame}
554 \hspace{-5cm}
555 \includegraphics[height=8cm]{figs/pert.pdf}
556\end{frame}
557
558\begin{frame}
559 \frametitle{Deviations from DoW}
560 \alert{Major deviations} from the DoW
561 \begin{enumerate}
562  \item Introduction of the dependent labelling approach and application to
563    the pen-and-paper proof of a toy compiler. Forking of the CerCo compiler
564    and Frama-C plug-in to implement loop optimizations and
565    redundancy elimination.
566    \alert{No impact on the schedule, work performed by additional Post-Doc.}
567  \item Anticipation of D5.3 from the third to the second period.
568    D5.3 is a major case study and its role is that of assessing the potential
569    of CerCo technology on some restricted scenario. Useful for early
570    dissemination too. Made possible by hiring problems in Paris (resignation
571    of PhD student during first period and extension of Post-Doc contract
572    to cover second period).
573    \alert{We hereby officially require permission to\\
574    anticipate delivery of D5.3 to second period}
575 \end{enumerate}
576\end{frame}
577
578\begin{frame}
579 \hspace{-5cm}
580 \includegraphics[height=8cm]{figs/pert.pdf}
581\end{frame}
582
583\section{Project management}
584
585\begin{frame}
586 \frametitle{Management activities}
587 Management WP1:
588 \begin{enumerate}
589  \item to \alert{coordinate and supervise} activities to be
590    carried out
591  \item to carry out the overall \alert{administrative and
592    financial management} of the project
593  \item to manage \alert{contacts with the European Commission}
594  \item to \alert{monitor quality and timing} of project deliverables
595  \item to establish effective internal and external
596        \alert{communication procedures}
597 \end{enumerate}
598\end{frame}
599
600\begin{frame}
601 \frametitle{Financial management and coordination}
602 During first period:
603 \begin{enumerate}
604  \item transmission \alert{pre-financing} to all beneficiaries
605  \item \alert{collecting and checking} partner's \alert{financial information} for the
606    Second Progress Report
607  \item \alert{submission of financial statement} through NEF system (in progress)
608  \item gathering all necessary information and submission of \alert{management
609   reports, activity reports and deliverables}
610 \end{enumerate}
611\end{frame}
612
613\begin{frame}
614 \frametitle{Periodic Meetings}
615 Three project meetings during 2nd period (one planned in DoW):
616 \begin{itemize}
617  \item \alert{Project meeting, Edinburgh, February 2011.}\\
618   Planning; review of
619   decisions taken during implementor's meeting, discussion on the
620   proof strategy and on the actions to be taken as an answer
621   to the reviewer's recommendations.
622  \item \alert{Project meeting, Paris, September 2011.}\\
623   Federated CerCo and Eternal meeting (for dissemination and to establish
624   co-operation). Review of deliverables due at month 18. Invited speaker
625   from WCET community.
626  \item \alert{Implementer's meeting, Edinburgh, December 2011}\\
627   Discussion of issues found in the global proof strategy; introduction
628   of the notion of structured traces and re-planning of the global
629   proof strategy. Integration problems\\ addressed.
630 \end{itemize}
631\end{frame}
632
633\end{document}
Note: See TracBrowser for help on using the repository browser.