source: Deliverables/D1.3/Presentations/WPx-claudio.tex @ 3534

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

...

File size: 34.3 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       An Overview of the Past, Present and Future of CerCo}
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{Problem Statement and CerCo's Approach in Perspective}
46
47\begin{frame}
48 \frametitle{Problem Statement}
49 \alert{Functional} properties are checked on high level \alert{source code}\\
50 \alert{Non functional} properties are checked on \alert{object code}\\
51 
52 \begin{enumerate}
53  \item The two analyses are \alert{NOT orthogonal}\\
54        \fbox{Misleading results, duplicated work}
55  \item Complex optimizations (e.g. parallelization) $\Rightarrow$\\ \alert{user contribution} to
56        control flow analysis \alert{very hard}\\
57        \fbox{Loss of precision, wrong results, simple optimizations only}
58  \item \fbox{Performance improvement is \alert{hard}}
59  \item \alert{Parametric} cost analysis \alert{very hard}
60        \fbox{Loss of precision in compositionality}
61  \item Cost analysis not available in \alert{early development}\\
62        \fbox{Tackling the problems later is more costly}
63  \item Fully automatic (+) but \alert{boolean answers} only (-)\\
64        \fbox{No incremental refinement and tradeoffs}
65 \end{enumerate}
66\end{frame}
67
68\begin{frame}
69 \frametitle{Problem Statement}
70
71 Moreover
72
73 \begin{center}
74  \alert{The most important thread of theoretical computer science is
75    raising the level of abstraction, from the machine to the human one}
76 \end{center}
77
78 State of the art:
79  \begin{center}
80   \alert{Analysis of non functional properties either is bound to the machine
81    level or it abstracts away too much by talking only of complexity classes}
82  \end{center}
83
84 \vspace{-0.2cm}
85 As a result, real time embedded systems still coded in a\\
86 constrained way and at low level to ensure non functional guarantees.
87\end{frame}
88
89\begin{frame}
90 \frametitle{CerCo's vision and approach}
91
92 Vision:\\~\\
93
94 \alert{Reconcile} functional and non-functional analysis \\~\\
95
96 Perform both \alert{on the source code} where more techniques can be employed \\~\\~\\
97
98 Approach:\\~\\
99
100 Induce a \alert{precise (thus parametric and non uniform) cost model} on the source
101 code \\~\\
102
103 \alert{Compilers} must be modified to transfer cost models from the object to the
104 source code
105 
106\end{frame}
107
108\begin{frame}
109 \frametitle{Relevance of the Problem Statement}
110 \emph{Is the problem still valid?} \alert{Yes}\\
111 \emph{Do you still believe in its relevance?} \alert{Definitely yes}\\~\\
112
113 Idealized vision of ICT from the theoretical CS community:
114
115 \begin{center}
116   \alert{Most programs will be (partially)\\ specified and certified}
117 \end{center}
118
119 \begin{enumerate}
120  \item Moving beyond constrained domains $\Rightarrow$\\
121        \alert{parametric and interactive analysis a necessity}
122  \item A lot of recent work (e.g. POPL papers) on static prediction of
123        non functional properties on idealized cost models $\Rightarrow$\\
124        \alert{realistic, non uniform cost models a necessity}
125 \end{enumerate}
126\end{frame}
127
128\begin{frame}
129 \frametitle{Relevance of the Problem Statement}
130 \emph{Is the problem still valid?}\\
131 \emph{Do you still believe in its relevance?}\\~\\
132
133 Software engineering perspective:
134
135 \begin{center}
136   \alert{System development should be made cheaper and faster
137          and deliver safer and most performant products}
138 \end{center}
139
140 In favour of its relevance:
141 \begin{enumerate}
142  \item Resource analysis in \alert{early development phases} is crucial
143  \item Massive parallelization for multicores $\Rightarrow$\\
144        disruption of the control flow\\
145        (\alert{no interactivity}, \alert{harder code improvements})
146 \end{enumerate}
147\end{frame}
148
149\begin{frame}
150 \frametitle{Relevance of the Problem Statement}
151 \emph{Is the problem still valid?}\\
152 \emph{Do you still believe in its relevance?}\\~\\
153
154 Software engineering perspective:
155
156 \begin{center}
157   \alert{System development should be made cheaper and faster
158          and deliver safer and most performant products}
159 \end{center}
160
161 Against its relevance:
162 \begin{enumerate}
163  \item \alert{Diminishing returns}: for embedded systems code the major
164        source of imprecision is becoming the \alert{hardware model}
165  \item \alert{Static analysis of current hardware is getting hopeless}\\
166        (e.g. multicores, unavailable precise hardware models)
167 \end{enumerate}
168\end{frame}
169
170
171\begin{frame}
172 \frametitle{Relevance of the Labelling Approach}
173 \emph{Is the approach still valid?} \alert{Yes} \\
174 \emph{Do you still believe in its relevance?} \alert{From our experience, yes}\\~\\
175
176 Idealized vision of ICT from the theoretical CS community:
177
178 \begin{center}
179   \alert{Most programs will be (partially)\\ specified and certified}
180 \end{center}
181
182 \begin{enumerate}
183  \item The approach provides a precise cost model that replaces the
184        idealized ones
185  \item It complements, leverages and enhances all other existing
186        approaches (but requires parametricity of the costs)
187 \end{enumerate}
188\end{frame}
189
190\begin{frame}
191 \frametitle{Relevance of the Approach}
192 \emph{Is the approach still valid?}\\
193 \emph{Do you still believe in its relevance?}\\~\\
194
195 Software engineering perspective:
196
197 \begin{center}
198   \alert{System development should be made cheaper and faster
199          and deliver safer and most performant products}
200 \end{center}
201
202 \vspace{-0.5cm}
203 In favour:
204 \begin{enumerate}
205  \item Supports early analysis and progressive refinement
206 \end{enumerate}
207 Against:
208 \begin{enumerate}
209  \item \alert{Ad-hoc} compiler and IDE, \alert{non fully automatic}
210  \item \alert{Does not leverage} existing SE techniques and tools
211  \item No major improvement expected for constrained code
212 \end{enumerate}
213\end{frame}
214
215\begin{frame}
216 \frametitle{Alternative Approach}
217 \emph{Is the approach still valid?}
218 \emph{Do you still believe in its relevance?}\\~\\
219
220 Reverse CerCo:
221
222 \vspace{-0.25cm}
223 \begin{center}
224 \alert{The compiler transfers functional properties\\ from the source to the
225 object code}
226 \end{center}
227
228 Non functional analysis is performed on the object code reusing the
229 functional information\\
230
231 \begin{enumerate}
232  \item[+] \alert{Leverages more} existing WCET techniques (not tools)
233  \item[+] Less sensitive to \alert{modern hardware} issues
234  \item[-] Does not support \alert{early analysis and progressive refinement}
235  \item[-] \alert{Ad-hoc} compiler and IDE, \alert{non fully automatic}
236 \end{enumerate}
237\end{frame}
238
239\begin{frame}
240 \frametitle{Conclusions}
241 \emph{Is the long term vision described in the proposal still valid?}\\
242 \alert{Yes, but there are major challenges}
243 \\~\\
244
245 \vspace{-0.25cm}
246 \begin{enumerate}
247  \item Driving vision shared across the formal methods community\\
248        (cfr. EMBounded)
249  \item The approach does not target the most relevant issue of current cost
250        analysis, namely the \alert{intrinsic unpredictability} of modern complex
251        architectures, and is affected by it
252  \item \alert{Unresolved rising challenge} faced by all working in cost analysis
253        (cfr. PROARTIS, PARMERASA, T-CREST, REMS, TACLe)
254 \end{enumerate}
255\end{frame}
256
257\section{Contributions to the long term vision}
258
259\begin{frame}
260 \frametitle{Contributions}
261 \emph{How far the concrete project achiev. contribute to the l.t. vision?}
262 
263 \vspace{-0.25cm}
264 Sub-problems posed by the CerCo approach:
265 \vspace{-0.25cm}
266 \begin{enumerate}
267  \item Compute \alert{manageable} parametric cost models on the
268        object c.\\
269        \alert{\underline{No contribution}: we deliberately focused on 2 and 3 as 1 requires expertise and resources that were not part of the consortium}
270  \item Transfer the cost models in a certified way without
271        introducing approximations\\
272        \alert{\underline{Major contribution}: a technique, a proof methodology, evidence
273               that it scales to more complex scenarios, a certified proof}
274  \item Exploit the cost models on the source level\\
275        \alert{\underline{Initial contribution}: integration of the compiler in Frama-C,
276               evidence that cost invariant inference is feasible and that
277               generic automatic techniques can handle the
278               proof obligations}
279 \end{enumerate}
280\end{frame}
281
282\begin{frame}
283 \frametitle{Self assessment}
284 \emph{How successful is the CERCO project in your own view?}\\
285 \alert{Fully successful in achieving the original goals}
286 and we \alert{achieved more than what was planned} in dealing with
287 \alert{optimizations that alter the control flow}.\\~\\
288
289
290 We proposed from scratch a novel approach to time analysis. \\~\\
291
292 Our goals for the project:
293
294 \begin{itemize}
295  \item To be able to transfer the cost models in a certified way without
296        introducing approximations, possibly restricting the
297        compilation/optimization techniques
298  \item To understand if the cost models obtained are simple enough to be
299        exploitable
300 \end{itemize}
301
302\end{frame}
303
304\begin{frame}
305 \frametitle{Self assessment}
306 \emph{How successful is the CERCO project in your own view?}
307
308 We did not have as an initial goal for the project (and no expertise in the
309 consortium) for:
310
311 \begin{itemize}
312  \item being able to compute manageable parametric cost models on the
313        object code for advanced hardware architectures\\
314 \end{itemize}
315
316 The proposed goals were already challenging alone and critical for the
317 long term vision.
318\end{frame}
319
320%\begin{frame}
321 %\frametitle{Self assessment}
322 %\emph{How successful is the CERCO project in your own view?}
323
324 %The reviewers and the WCET community criticized our (initial) approach for
325 %being to simplistic and restricted w.r.t. state of the art.\\~\\
326
327 %The reviewers were later surprised by the dependent labelling approach with
328 %sentences like ``\emph{you put yourself out of the corner}''.\\~\\
329
330 %\alert{We never felt in a corner and the dependent labelling approach was
331 %not a revolutionary idea (hints in the DoW)}.\\~\\
332
333 %Following basic research tradition, we expect to develop the approach
334 %incrementally by progressively tackle more complex problems.\\~\\
335
336 %Current WCET techniques are the results of two decades of improvements over
337 %the initial idea: direct comparison is unfair.
338%\end{frame}
339
340\begin{frame}
341 \frametitle{Self assessment}
342 \emph{How successful is the CERCO project in your own view?}
343
344 We believe to have been \alert{moderately successful} in identifying
345 extensions of the basic approach that have the potential of contributing
346 solutions to the forthcoming problems.\\~\\
347
348 We have been \alert{less successful} in convincing the \emph{engineering}
349 community of the potentiality of our approach
350 \begin{itemize}
351  \item targeting the non critical issues (multicores, complex hardware,
352        lack of clock precise models)
353  \item no focus on early development
354  \item no early evidence of success in performing as state of the art
355  \item certification not appealing (and workplan focused on that)
356 \end{itemize}
357\end{frame}
358
359\begin{frame}
360 \frametitle{Next steps}
361 \emph{What are the next steps still needed to move forward?}
362
363 \begin{enumerate}
364  \item Involvement of experts of WCET/clock precise hw models
365  \item Inference of \alert{compositional}, \alert{manageable} dependent cost
366        models for modern hardware
367    \begin{itemize}
368     \item Introduce approximations, to reduce the size of the model
369     \item May require combination of CerCo + reverse CerCo
370    \end{itemize}
371  \item Improve time analysis on the source
372        code; introduce tradeoff between precision and termination/speed of the
373        analysis
374  \item Focus on time analysis for early development phases
375  \item Applications of labelling to other non functional properties
376        (e.g. information flow security)
377  \item Integration with IDEs used in development
378  \item Tracking/integration of proposals to perform static\\
379        analysis for multicores and systems-on-chip
380 \end{enumerate}
381\end{frame}
382
383\begin{frame}
384 \frametitle{Effect on future ICT}
385 \emph{How future ICT will be affected by CERCO results?}
386
387 \begin{block}{Early development phases (medium term)}
388 CerCo applies to early development phases and supports progressive
389 refinement.
390 \end{block}
391
392 \begin{block}{General purpose code (long-medium term)}
393 Major ICT failures (4 in Italy alone in last 2 years)
394 for \alert{non real time software} that did not scale to production. \\~\\
395
396 Non functional analysis harder for general purpose code\\
397 (e.g. dynamic data structures).\\
398 \alert{Non parametric WCET techniques insufficient, CerCo adaptable.}\\~\\
399 \end{block}
400
401\end{frame}
402
403\begin{frame}
404 \frametitle{Effect on future ICT}
405 \emph{How future ICT will be affected by CERCO results?}
406
407 \begin{block}{High level languages everywhere (very long term)}
408 The history of computer science is a journey from lower to higher levels of
409 abstractions. \\~\\
410
411 The \alert{industrial world} is \alert{well behind} the academic community,
412 but slowly and selectively catching up. \\~\\
413
414 We do not see a real advancement in ICT unless it becomes possible to easily
415 reason on non functional properties for generic code. \\~\\
416
417 CerCo will allow such an advancement \alert{iff future hardware will still
418 allow for static analysis at all}. \\~\\
419 \end{block}
420\end{frame}
421
422
423\begin{frame}
424 \frametitle{Exploitation of results}
425 \emph{Any concrete idea for exploitation of the project results?}\\~\\
426
427 In the medium term:
428 \begin{center}
429  \alert{CerCo's prototype as a tool for time analysis\\ in
430         early development phases}
431 \end{center}
432
433 \begin{itemize}
434  \item Reduced dependency on hardware models
435  \item Emphasis on tools and techniques for invariant generation and proving
436        on the source level
437  \item Priority: graceful degradation of precision to always grant answers
438        in a reasonable time
439  \item The topic of one work package of TACLe
440 \end{itemize}
441\end{frame}
442
443\begin{frame}
444 \frametitle{CerCo as a Collaborative Project}
445 \emph{Which has been the advantage (if any) to run CERCO research in the framework of a ``Collaborative Project''?}
446
447 Honest answer:
448
449 \begin{enumerate}
450  \item The consortium put together in a focused collaboration expertises
451        that were not found in any single site
452  \item The manpower required by the project corresponded to a level of
453        funding that is no longer provided by national or bi-lateral projects
454 \end{enumerate}
455
456 Which funding scheme (if not FET-Open) is more appropriate for basic
457 research that requires a great implementation effort \\
458 to deliver a unified end product?
459\end{frame}
460
461\end{document}
462
463\section{Long, middle and short term objectives}
464
465\begin{frame}
466 \frametitle{The ICT of the future: Programs}
467 We envision a (long term) future where formal methods will be pervasive:
468 \begin{center}
469   \alert{\Large Most programs will be (partially) specified and certified}
470 \end{center}
471
472 The very same definition of ``program'' will change:
473 \begin{center}
474  \alert{\Large A program will be a triple made of a specification,
475  an implementation and a proof certificate}
476 \end{center}
477
478 Cfr: Proof Carrying Code (PCC)
479\end{frame}
480
481\begin{frame}
482 \frametitle{The ICT of the future: the ITP point of view}
483 There is always a trade off between expressivity (precision) and
484 automation (partiality, abstraction).\\~\\
485
486 Interactive theorem proving perspective:
487   \alert{\Large
488   \begin{itemize}
489    \item Maximal expressivity (precision) in specification
490    \item Interactive proofs
491    \item Abstraction, loss of precision as special cases of specification
492    \item Automation as special cases of interaction
493   \end{itemize}
494   }
495\end{frame}
496
497\begin{frame}
498 \frametitle{The ICT of the future: Compilation}
499 In our long-term vision:
500 \begin{center}
501 \alert{\Large A compiler maps triples specification-implementation-certificate
502  to triples specification-implementation-certificate.}
503 \end{center}
504
505 What is investigated in CerCo:
506 \begin{center}
507 \alert{\Large Inclusion of intensional (non functional) properties into the
508  specification to enable high level but precise reasoning.}
509 \end{center}
510\end{frame}
511
512\begin{frame}
513 \frametitle{The ICT of the future: Difficulties}
514 Non functional properties (time, space, energy) are affected by:
515
516 \begin{itemize}
517  \item \alert{The compilation process} (which is not compositional)\\
518        E.g. the cost of different high level occurrences of the same
519        instruction is different.\\
520        E.g. aggressive optimizations that change the control flow
521  \item \alert{Hardware status} (caches, pipelines, branch prediction unit)
522 \end{itemize}
523
524 Questions and trade-offs:
525 \begin{itemize}
526  \item How much \alert{precision} can be achieved?
527  \item How \alert{complex} are precise cost models for advanced compilation
528        strategies and/or modern hardware?
529  \item How much complexity can be tamed by \alert{abstraction}\\
530        and automation at the source code level?
531 \end{itemize}
532\end{frame}
533
534\begin{frame}
535 \frametitle{The ICT of the future: Coping with the difficulties}
536
537 In the project timeframe:
538
539 \alert{We started with a simple scenario:}
540 \begin{itemize}
541  \item Conventional compilation model without changes to the control flow
542  \item Deterministic widely deployed hardware model (no caching, pipelining)
543 \end{itemize}
544
545 \alert{We will formally certify the simple scenario}\\~\\
546
547 \alert{We have started to scale to most complex scenarios\\
548        (without certification).}\\~\\
549\end{frame}
550
551\begin{frame}
552 \frametitle{Short term objectives (achievements)}
553 \begin{enumerate}
554  \item develop a \alert{compiler} from
555        \alert{$\approx\!\!$ C} to \alert{MCS-51} processor
556        (1st period)
557  \item have the compiler infer from the assembly code a \alert{precise cost
558        model} for the source program (1st period)
559  \item \alert{certify} the compiler
560  \item embed the compiler in a \alert{prototypical environment} for
561   \begin{itemize}
562    \item stating \alert{cost invariants} based on the inferred cost model
563    \item computing \alert{proof obligations}
564    \item \alert{proving} generated obligations automatically or interactively
565   \end{itemize}
566   (partially in 2nd period)
567  \item lift the technique to a \alert{synchronous language}
568        (2nd period)
569  \item \alert{Scale} the approach to \alert{more complex scenarios}
570 \end{enumerate}
571\end{frame}
572
573\begin{frame}
574 \frametitle{CerCo interaction diagram}
575 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
576\end{frame}
577
578\begin{frame}
579 \frametitle{Case study interaction diagram}
580 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
581\end{frame}
582
583\section{State at the end of first period}
584
585\begin{frame}
586 \frametitle{Achievements (1st period)}
587 Main theoretical achievements (D2.1):
588 \begin{center}
589  \alert{\Large a methodology (basic labelling approach) for lifting in a provably correct way
590    costs on the object code to costs in the source code}\\
591 \end{center}~\\
592
593 Main practical achievements (D2.2):
594 \begin{center}
595  \alert{\Large an untrusted compiler from C-Light to the MCS-51 processor
596   that implements the methodology}
597 \end{center}
598\end{frame}
599
600\begin{frame}
601 \frametitle{Achievements (1st period)}
602 Preliminary work for future achievements (D3.1,D4.1):
603 \begin{center}
604  \alert{\Large formalized executable semantics for C-Light and the MCS-51
605   processor}
606 \end{center}
607\end{frame}
608
609\begin{frame}
610 \includegraphics[height=8cm]{figs/pert.pdf}
611\end{frame}
612
613\begin{frame}
614 \frametitle{Recommendations from the reviewers}
615  ``In order to not limit the results that can be obtained in the
616  project to processors with very old architectures \ldots the  project
617  partners  should  explicitly  consider  how  the  assumptions  on  the
618  hardware architecture influence the results obtained and in how far these
619  assumptions could be a threat to the validity and generality of the results''
620
621  Limiting assumptions for the basic labelling approach:
622  \begin{enumerate}
623   \item \alert{The compiler should not alter significantly the control flow}\\
624         Loss of precision and/or correctness
625   \item \alert{Existence of a function that associates a cost to each basic
626         block independently from the processor status}\\
627         Serious loss of precision
628  \end{enumerate}
629\end{frame}
630
631\begin{frame}
632 \frametitle{Recommendations from the reviewers}
633 Case study for the alteration of control flow:\\
634 \alert{loop optimizations} (peeling, unrolling)
635
636 Description:\\
637
638 \alert{in peeling/unrolling different iterations are compiled differently and
639 they receive a different cost}.
640
641 Alternative reading:\\
642 \alert{after peeling/unrolling the cost of an iteration is a function of the
643 program state (iteration number)}.
644
645 Symptom:\\
646 \alert{serious loss of precision} (if we take the maximum cost).
647
648 Solution sketched at the previous review:\\
649 \alert{dependent costs: the cost is a function of the state}
650\end{frame}
651
652\begin{frame}
653 \frametitle{Recommendations from the reviewers}
654 Case study for advanced hardware features:\\
655 \alert{cache}
656
657 Description:\\
658 \alert{using caches different iterations of a loop are executed with
659 a different cost}.
660
661 Alternative reading:\\
662 \alert{using caches the cost of an iteration is a function of the
663 processor state (cache)}.
664
665 Symptom:\\
666 \alert{serious loss of precision} (if we take the maximum cost).
667
668 Solution sketched at the previous review:\\
669 \alert{dependent costs: the cost is a function of the state}
670\end{frame}
671
672\begin{frame}
673 \frametitle{Recommendations from the reviewers}
674 The two scenarios are analogous, yet the first is simpler:\\
675 \begin{enumerate}
676  \item Loop optimization\\
677   \alert{program state always known and available in the source code}\\
678   Total precision can be achieved.\\
679   Problem: are the dependent annotations easy to understand and work with
680   (manually or automatically)? Probably yes
681 \item Cache\\
682   \alert{\makebox[0pt][l]{cache state only (?) approximated (via abstract interpretation)}}\\
683   Total precision impossible (?) to achieve\\
684   Problem: are the dependent annotations easy to understand and work
685   with? Open question
686 \end{enumerate}
687\end{frame}
688
689\begin{frame}
690 \frametitle{Recommendations from the reviewers: action taken}
691 Dr. Paolo Tranquilli hired at UNIBO at month 19 to
692 \begin{itemize}
693  \item Develop the dependent labelling approach (completed)
694  \item Apply it to the loop optimization scenarios (completed)
695  \item Apply it to the cache scenario (to be started)
696 \end{itemize}
697
698 Theoretical achievement:\\
699 \alert{dependent labelling approach} and pen\&paper certification of a toy
700 compiler based on it
701
702 Practical achievement:\\
703 Branch of all CerCo software (compiler, etc.) that implements
704 \alert{loop optimizations, redundancy elimination, improved constant
705 propagation}.
706\end{frame}
707
708\begin{frame}
709 \frametitle{Recommendations from the reviewers: action taken}
710 \alert{No impact on planning}\\
711 Dr. Tranquilli and Dr. Boender (Post-Docs) replaced the
712 senior researcher position which was made impossible during the first period.\\
713 ~\\
714
715 \alert{No impact on budget}\\
716 Minor delays so far on the project plan (Dr. Boender alone is less experienced
717 than the originally expected candidate)\\
718\end{frame}
719
720\begin{frame}
721 \frametitle{Recommendations from the reviewers}
722 ``we recommend to adapt the labelling approach such that basic complexity
723 annotations can be obtained  by  program  pieces  of  larger  granularity
724 than  is  done  now.  This  will  allow  \ldots  the  use  of WCET tools to
725 infer time bounds''
726\end{frame}
727
728\begin{frame}
729 \frametitle{Recommendations from the reviewers}
730 Suggested approach (EmBounded):
731 \begin{itemize}
732  \item \alert{Chunks} fed to the WCET tool and analyzed \alert{in isolation}
733  \item In isolation processor \alert{state unknown}
734        $\Rightarrow$ \alert{loss of precision}
735  \item Result of the analysis abstracted to \alert{one number} per chunk
736 \end{itemize}
737 Dependent labelling approach (\alert{CerCo}):
738 \begin{itemize}
739  \item \alert{Global analysis} of the object code
740        $\Rightarrow$ improved precision
741  \item Result of the analysis exposed via \alert{dependent costs}\\
742        $\Rightarrow$ \alert{improved precision}
743 \end{itemize}
744\end{frame}
745
746\begin{frame}
747 \frametitle{Recommendations from the reviewers: action taken}
748 Plan: to apply dependent labelling to caches.\\~\\
749
750 Reviewer's suggestion available as a fallback.
751\end{frame}
752
753\begin{frame}
754 \frametitle{Recommendations from the reviewers}
755 ``The authors should quickly outline a paper-and-pencil correctness proof for
756   each of the seven stages \ldots in order to allow for an estimation of the
757   complexity and time required''~\\~\\
758
759 Done.
760 \begin{itemize}
761  \item This made explicit the need to consider \emph{structured traces}.\\
762        Not needed in the proof of the toy compiler.
763  \item The overall \alert{effort} required is \alert{consistent} with the
764        person-months allocated to the project.
765  \item The estimation is based on our \alert{judgement of the proof complexity} and on \alert{projections} obtained from code size and coefficients computed
766        from CompCert.
767 \end{itemize}
768\end{frame}
769
770\begin{frame}
771 \frametitle{Recommendations from the reviewers}
772 ``Based on the outline of the paper-and-pencil proofs, the authors should
773 estimate the effort for two possible scenarios: a) proceed as planned in the
774 Matita system (this involves porting all proofs of the CompCert project to
775 Matita); b) modify the existing proofs in Coq\ldots If the project partners
776 stick to the usage of Matita they should argue convincingly why this is a
777 suitable choice and in how far Matita is superior to Coq\ldots''
778\end{frame}
779
780\begin{frame}
781 \frametitle{Recommendations from the reviewers: action taken}
782 \begin{enumerate}
783  \item Misconception: we \alert{do not} want to port/reuse CompCert proofs;
784        in any case CompCert \alert{licensing forbids} this
785  \item CerCo is first of all a project in certified compiler verification.
786   \alert{Comparing design alternatives is a key scientific contribution}\\~\\
787
788   \begin{tabular}{lll}
789     & CerCo & CompCert \\
790    Semantics & executable & inductive \\
791    Proofs     & computed proof obligations & traditional \\
792    Types      & dependent & ML \\
793    Datatypes  & graphs & lists \\
794    Semantics  & read-only program + pc & small step operational \\ 
795   \end{tabular}
796 \end{enumerate}
797\end{frame}
798
799\begin{frame}
800 \frametitle{Recommendations from the reviewers: action taken}
801 \begin{enumerate}
802  \item Commitment to the \alert{promotion of Matita}.
803  \item Exploiting implementation differences\\~\\
804   \begin{tabular}{lll}
805       & Matita & Coq \\
806    Small scale automation & unification hints & type classes \\
807    Big scale automation   & paramodulation & resolution \\
808    Tactics                & tinycals & LCF \\
809    Specifications         & executable & relational \\
810   \end{tabular}\\~\\
811  \item \alert{Co-development}:
812    when you have control of the tool, you can adapt the tool
813    instead of adapting the formalization
814 \end{enumerate}
815 Because of the previous motivations and the positive\\ outcome
816 of the effort estimation, \alert{we stick to original plan}.
817\end{frame}
818
819\section{Project planning and achievements}
820
821\begin{frame}
822 \includegraphics[height=8cm]{figs/pert.pdf}
823\end{frame}
824
825\begin{frame}
826 \frametitle{Achievements (2nd period) 1/3, Ayache}
827 From the \alert{CerCo annotating compiler} (1st period)\\
828 ~~~~~ - inference of costs for basic blocks;\\
829 ~~~~~ - instrumentation of the source code\\
830 to the \alert{CerCo untrusted prototype} (2nd period)\\
831 ~~~~~ - inference of cost invariants;\\
832 ~~~~~ - certified proofs of cost obligations;\\
833 \begin{enumerate}
834  \item Integration of the CerCo compiler into \alert{Frama-C} (D5.1)
835   \item The abstract interpretation based \alert{Frama-C CerCo plug-in} for
836     the inference of \alert{global complexity assertions} (D5.1)
837   \item The \alert{Lustre CerCo plug-in} for
838     automated analysis of WCRT (D5.3)
839 \end{enumerate}
840\end{frame}
841
842\begin{frame}
843 \frametitle{CerCo interaction diagram}
844 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
845\end{frame}
846
847\begin{frame}
848 \frametitle{Achievements (2nd period) 2/3, Mulligan/Campbell}
849 Towards the \alert{CerCo trusted prototype} (3rd period): to verify\\
850 ~~~ - preservation of labelled traces;\\
851 ~~~ - exact correspondence between actual and inferred cost\\
852 \begin{enumerate}
853  \item CIC encoding: Front/Back end (D4.2/D4.3)
854  \item \mbox{\rlap{Executable semantics of all intermediate languages (D3.3/D4.3)}}
855  \item Beginning of formal verification
856   \begin{itemize}
857    \item Common/generic definitions, \alert{data structures} to represent invariants,
858          \alert{invariants} enforced as dependent types
859    \item \alert{Optimizing assembler} verification (75\%)
860    \item Proof of \alert{correspondence} of actual and inferred cost (95\%)
861    \item Generation of \alert{structured} labelled traces (for
862          back-end)\\ from \alert{flat} labelled traces (from front-end)
863   \end{itemize}
864 \end{enumerate}
865\end{frame}
866
867\begin{frame}
868 \frametitle{Achievements (2nd period) 3/3 R\`egis-Gianas/Tranquilli}
869 \alert{Enlarging the scope} of CerCo techniques
870 \begin{enumerate}
871  \item Extension of the basic labelling approach to cover \alert{functional
872   languages} (D5.1)\\
873   - prototype implemented
874  \item Dependent labelling approach to cover \alert{control flow alterations}
875   and \alert{modern hardware features} (D5.1)\\
876   - branch of CerCo compiler with loop optimizations, redundancy elimination,
877     etc.
878 \end{enumerate}
879\end{frame}
880
881\begin{frame}
882 \frametitle{Assessment}
883 Assessment level and strategies:
884 \begin{enumerate}
885  \item CIC encoding: Front/Back end (D4.2/D4.3):\\
886    - \alert{tested} inside Matita (executable code);\\
887    - to be \alert{certified} in D3.4/D4.4 (Front/Back end correctness)
888  \item \makebox[0pt][l]{Executable semantics of intermediate languages
889    (D3.3/D4.3):}\\
890    \alert{tested} by executing programs
891  \item Untrusted CerCo prototype (D5.1, M2):\\
892    - tested (methodology + code) in the \alert{case study} (D5.3);\\
893    - plan to test on library of cryptographic functions
894  \item Case study: analysis of synchronous code (D5.3):\\
895   - \alert{self testing code} checks correctness and precision\\
896   - tested on examples
897 \end{enumerate}
898\end{frame}
899
900\begin{frame}
901 \frametitle{Deviations from DoW}
902 \alert{Minor deviations} from the DoW
903 (no significant impact on the future schedule):
904 \begin{enumerate}
905  \item At month 16 (+16): submission of the commitment letter and
906    addenda required by the reviewers. \alert{Done}
907  \item Late delivery of D4.2 delayed D3.2, D3.3, D4.3 (at month 21, planned
908    at month 18).\\ Bologna: one post-doc in place of senior researcher
909    (plus another on dependent labelling).\\
910    \alert{No short term impact, possible minor impact at month 36}
911 \end{enumerate}
912\end{frame}
913
914\begin{frame}
915 \hspace{-5cm}
916 \includegraphics[height=8cm]{figs/pert.pdf}
917\end{frame}
918
919\begin{frame}
920 \frametitle{Deviations from DoW}
921 \alert{Major deviations} from the DoW
922 \begin{enumerate}
923  \item Research on dependent labelling in response to reviewers.\\
924    \alert{No impact on the schedule, work done by additional Post-Doc.}
925  \item Bring forward D5.3 from the third to the second period.\\
926    D5.3 is a major case study to assess the potential
927    of CerCo technology $\Rightarrow$ \alert{early dissemination}.\\
928    Enabled by replacement of PhD student by Post-Doc in Paris\\~\\
929    {\Large \alert{We hereby officially require permission for\\
930    early delivery of D5.3 in second period}}
931 \end{enumerate}
932\end{frame}
933
934\begin{frame}
935 \hspace{-5cm}
936 \includegraphics[height=8cm]{figs/pert.pdf}
937\end{frame}
938
939\section{Project management}
940
941\begin{frame}
942 \frametitle{Management activities}
943 Management WP1:
944 \begin{enumerate}
945  \item \alert{coordinate and supervise} activities to be
946    carried out
947  \item carry out the overall \alert{administrative and
948    financial management} of the project
949  \item manage \alert{contacts with the European Commission}
950  \item \alert{monitor quality and timing} of project deliverables
951  \item establish effective internal and external
952        \alert{communication procedures}
953 \end{enumerate}
954\end{frame}
955
956\begin{frame}
957 \frametitle{Financial management and coordination}
958 During second period:
959 \begin{enumerate}
960  \item transmission \alert{pre-financing} to all beneficiaries
961  \item \alert{collecting and checking} partner's \alert{financial information} for the
962    Second Progress Report
963  \item \alert{submission of financial statement} through NEF system (in progress)
964  \item gathering all necessary information and submission of \alert{management
965   reports, activity reports and deliverables}
966 \end{enumerate}
967\end{frame}
968
969\begin{frame}
970 \frametitle{Periodic Meetings}
971 Three project meetings during 2nd period (one planned in DoW):
972 \begin{itemize}
973  \item Project meeting, Edinburgh, February 2011.\\
974   %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.
975  \item Project meeting, Paris, September 2011.\\
976   \alert{Federated CerCo and Eternal meeting}
977   %(for dissemination and to establish co-operation). Review of deliverables due at month 18. Invited speaker from WCET community.
978  \item Implementer's meeting, Edinburgh, November 2011\\
979   %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.
980 \end{itemize}
981\end{frame}
982
983\begin{frame}
984\begin{tabular}{lrlrr}
985Pass   & Lines & CompCert & Effort   & Effort \\
986Origin &       & ratio    & computed & adjusted \\
987\hline
988Common &  4864 & 4.25 \permil & 20.67 & 17.0 \\
989Clight &  1057 & 5.23 \permil & 5.53  &  6.0 \\
990Cminor &  1856 & 5.23 \permil & 9.71  & 10.0 \\ 
991RTLabs &  1252 & 1.17 \permil & 1.48  &  5.0 \\
992RTL    &   469 & 4.17 \permil & 1.95  &  2.0 \\
993ERTL   &   789 & 3.01 \permil & 2.38  & 2.5 \\
994LTL    &    92 & 5.94 \permil & 0.55  & 0.5 \\
995LIN    &   354 & 6.54 \permil & 2.31  &   1.0 \\
996ASM    &   984 & 4.80 \permil & 4.72  &  10.0 \\
997\hline
998Tot co &  4864 & 4.25 \permil & 20.67 & 17.0 \\
999Tot fe &  2913 & 5.23 \permil & 15.24 & 16.0 \\
1000Tot be &  6853 & 4.17 \permil & 13.39 & 21.0 \\
1001\hline
1002Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
1003\end{tabular}
1004\end{frame}
1005
1006
1007\end{document}
Note: See TracBrowser for help on using the repository browser.