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

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

...

File size: 17.5 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  ``The consortium should concentrate on positioning the project with
232    respect to the state of the art which requires a detailed literature
233    survey. In particular, the consortium should clearly formulate what
234    distinguishes the project from existing work and which results are
235    clear improvements.''
236
237  \begin{itemize}
238   \item We got in touch with \alert{other EU projects} active in the area of WCET,
239         in particular EMBounded, PROARTIS, TACLe, PARMERASA, T-CREST, REMS.
240   \item Direct contacts during the \alert{CerCo events}
241   \item It \alert{really helped} in understanding what are the relevant novelties,
242         the possible application scenarios and the weaknesses
243         from the engineering perspective
244   \item More details in D1.4 and the \alert{final presentation}
245  \end{itemize}
246\end{frame}
247
248\begin{frame}
249 \frametitle{Recommendations from the reviewers}
250 ``The consortium should as soon as possible start with the verification of
251   the compiler.'' ``The reviewers are worried that the whole verification tasks
252   cannot be successfully completed by the end of the third project period.''
253
254  \begin{itemize}
255   \item The formal proof for the While language (1st period) was \alert{misleading}:
256    function calls introduce a \alert{much larger set of novel intensional invariants}
257   \item Moreover, the invariants are no longer expressed in terms of static
258         code $\Rightarrow$ complete redesign of the proof strategy
259   \item Had to consider \alert{stack space} too
260   \item \alert{Contingency plan}: focus on the \alert{novel parts}
261         (preservation of non functional properties), also exploiting the
262         \alert{uniform representation of backend languages}
263   \item Proof of preservation of costs \alert{completed up to} proofs\\
264         of preservation of functional properties
265  \end{itemize}
266\end{frame}
267
268\begin{frame}
269 \frametitle{Recommendations from the reviewers}
270 ``The consortium should develop a code extractor for MATITA which allows
271obtaining executable code from specifications s.t. an executable
272version of the trusted CerCo compiler can be automatically generated. This
273extraction will be crucial to apply the CerCo approach to practical case studies
274and to present it to industry.''
275
276 \vspace{-0.25cm}
277 \begin{itemize}
278  \item \alert{Done}
279  \item Many issues faced on the \alert{quality of the extracted code}
280        (e.g. because of dependent types) (D5.2)
281  \item \alert{Very nice example of very weakly typed extracted code}:
282        opens several nice research directions
283   \begin{itemize}
284    \item Targeting OCaml's new \alert{first class modules} to capture $\Sigma$-types
285    \item Targeting \alert{GADTs} to capture most dependent types
286    \item A new technique to represent \alert{polymorphic variants} and
287          \alert{extensible records} (had to be presented at TYPES'13)
288    \item Targeting GHC \alert{$F_\omega$-like} language (working prototype,\\
289          does not accept all programs, much harder than expected)
290   \end{itemize}
291 \end{itemize}
292\end{frame}
293
294\begin{frame}
295 \frametitle{Recommendations from the reviewers}
296 ``The consortium should concentrate on further developing and publishing
297the dependent labelling approach. In particular, the approach should be
298extended to further compiler optimizations, apart from loop peeling and
299hoisting, and be applied to more modern processor architectures, eventually
300aiming at multi-level caches and pipelines.''
301
302 \begin{itemize}
303  \item Dependent labelling \alert{published} at QAPL (journal version in preparation)
304  \item One Post-Doc hired by UNIBO to work on \alert{application of dependent
305        labelling to history sensitive hardware components} (pipelines, caches)
306  \item Outcome in my next talk
307 \end{itemize}
308\end{frame}
309
310\begin{frame}
311 \frametitle{Recommendations from the reviewers}
312 The reviewers required a revision of some deliverables and a few addenda.\\~\\
313
314 The new versions and addenda were submitted to the EU as expected.
315\end{frame}
316
317\section{Project planning and achievements}
318
319\begin{frame}
320 \hspace{-5.5cm}\includegraphics[height=8cm]{figs/pert.pdf}
321\end{frame}
322
323\begin{frame}
324 \frametitle{Achievements (3rd period) (WP3/WP4 talks)}
325 From the \alert{formalized CerCo compiler} (2nd period)\\
326  ~~~ - untrusted code\\
327  ~~~ - not optimized for proving\\
328  ~~~ - with axiomatized fixpoint computer and\\
329  ~~~~~ graph colouring algorithm\\
330  ~~~ - with formalized semantics for intermediate languages\\~\\
331 to the \alert{trusted CerCo compiler} (3rd period) (WP5 talk)\\
332  ~~~ - \alert{extracted code} integrated with untrusted code\\
333  ~~~~~ from the untrusted prototype\\
334  ~~~ - preservation of costs (time + \alert{stack space}) \alert{certified}\\
335  ~~~~~ modulo preservation of functional properties
336\end{frame}
337
338\begin{frame}
339 \frametitle{Achievements (3rd period) (WP5 talk)}
340 From the \alert{untrusted CerCo prototype} (2nd period)\\
341 ~~~ - untrusted compiler +\\
342 ~~~~~ plug-in for Frama-C + Jessie + Why\\~\\
343 to the \alert{trusted CerCo prototype} (3rd period)\\
344 ~~~ - trusted/untrusted compiler +\\
345 ~~~~~ plug-in for \alert{experimental Frama-C + Jessie + Why3}\\
346 ~~~ - code simplification, \alert{better coverage}, integration with\\
347 ~~~~~ \alert{separation logic} to cover arrays\\
348 ~~~ - \alert{fine tuning of the generated invariants} to match\\
349 ~~~~~ the automatic provers expertises\\
350 ~~~ - a simplified interface for \alert{casual users}\\
351 ~~~ - testing\\
352 ~~~ - Debian packages + \alert{Live CD} for dissemination
353\end{frame}
354
355\begin{frame}
356 \frametitle{Achievements (3rd period) (second WP4 talk)}
357 \alert{Enlarging the scope} of CerCo techniques\\
358 ~~~ - application of the \alert{dependent labelling approach} to cover\\
359 ~~~~~ certain cost models that capture \alert{parametricity} of the cost\\
360 ~~~~~ on the \alert{internal state of hardware} components that is\\
361 ~~~~~ \alert{history dependent}\\
362 ~~~ - sufficient to deal with pipelines (further research required)\\
363 ~~~ - caches still problematic: towards \alert{probabilistic static analysis}?
364\end{frame}
365
366\begin{frame}
367 \frametitle{Other activities (3rd period) (WP6 talk)}
368 Organization of CerCo events targeted to potential industrial stakeholders
369 and the academic community.
370\end{frame}
371
372\begin{frame}
373 \frametitle{Assessment}
374 Assessment level and strategies:
375 \begin{enumerate}
376  \item Trusted CerCo compiler encoding: (D3.4/D4.4):\\
377    - extracted code \alert{tested};\\
378    - partially \alert{certified} using Matita\\
379  \item Trusted CerCo prototype (D5.2, D6.3, M3):\\
380    - tested (methodology + code) in the \alert{case study} (D5.3);\\
381    - tested on library of cryptographic functions (D6.3)\\
382  \item Case study: analysis of synchronous code (D5.3):\\
383   - \alert{self testing code} checks correctness and precision\\
384   - tested on examples
385 \end{enumerate}
386\end{frame}
387
388\begin{frame}
389 \frametitle{Deviations from DoW}
390 \alert{Minor deviations} from the DoW
391 (no significant impact on the schedule):
392 \begin{enumerate}
393  \item At month 28: submission of the
394    addenda required by the reviewers. \alert{Done}
395  \item Late delivery of D5.3 (at end of project, planned at 36).\\
396    Most job completed during the 2nd period, we needed to test it again
397    on the last version of the trusted compiler.
398  \item Late delivery of D6.6 (at end of project, planned
399    at 33).\\
400    The source code of the Debian packages and the infrastructure for the
401    Live CD were ready on time, but the extracted code came later and was
402    changing because of adjustments to the proofs.
403 \end{enumerate}
404\end{frame}
405
406\begin{frame}
407 \frametitle{Deviations from DoW}
408 \alert{Major deviations} from the DoW
409 \begin{enumerate}
410  \item DoW amended for administrative issues and to extend the length of
411        the projects by two months
412  \item Research on handling history sensitive hardware in response to
413        reviewers.\\
414    \alert{No impact on the schedule, work done by additional Post-Doc.}
415  \item Bring forward work on D5.3 from the third to the second period.\\
416    Enabled by replacement of PhD student by Post-Doc in Paris
417  \item Compared to the formal proof for the Why language, the one for C
418        revealed a \alert{much larger set of intensional invariants}
419        to be preserved; our \alert{contingency plan} dictated that we focused
420        on the aspects that
421        are novel of our approach. The proof was finally \alert{completed up to
422        proofs of functional correctness} already covered by existing projects.
423 \end{enumerate}
424\end{frame}
425
426\section{Project management}
427
428\begin{frame}
429 \frametitle{Management activities}
430 Management WP1:
431 \begin{enumerate}
432  \item \alert{coordinate and supervise} activities to be
433    carried out
434  \item carry out the overall \alert{administrative and
435    financial management} of the project
436  \item manage \alert{contacts with the European Commission}
437  \item \alert{monitor quality and timing} of project deliverables
438  \item establish effective internal and external
439        \alert{communication procedures}
440 \end{enumerate}
441\end{frame}
442
443\begin{frame}
444 \frametitle{Financial management and coordination}
445 During second period:
446 \begin{enumerate}
447  \item \alert{amend} the DoW for administrative reasons (organizational changes
448        in UNIBO) and to \alert{extend the duration to 38 months}
449  \item transmission \alert{pre-financing} to all beneficiaries
450  \item \alert{collecting and checking} partner's \alert{financial information} for the
451    Second Progress Report
452  \item \alert{submission of financial statement} through NEF system (in progress)
453  \item gathering all necessary information and submission of \alert{management
454   reports, activity reports and deliverables}
455  \item two sites (UNIBO and UEDIN) are undergoing the \alert{financial
456        auditing}
457 \end{enumerate}
458\end{frame}
459
460\begin{frame}
461 \frametitle{Periodic Meetings}
462 Two project meetings and two short meetings during 3rd period
463 (one planned in DoW):
464 \begin{itemize}
465  \item Short project meeting, Paris, March 2012.\\
466   %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.
467  \item Short project meeting, Tallin, March 2012.\\
468   At ETAPS, negotiation of the CerCo event at next ETAPS
469   %(for dissemination and to establish co-operation). Review of deliverables due at month 18. Invited speaker from WCET community.
470  \item Project meeting, Bologna, May 2012\\
471   %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.
472  \item Implementer's meeting, Edinburgh, August 2012\\
473 \end{itemize}
474\end{frame}
475
476\end{document}
Note: See TracBrowser for help on using the repository browser.