source: Deliverables/D1.1/Presentations/WP1-claudio.tex @ 661

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

Renaming.

File size: 21.6 KB
Line 
1\documentclass{beamer}
2
3\usetheme{Frankfurt}
4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
5
6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{amssymb}
9\usepackage[english]{babel}
10\usepackage{color}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{stmaryrd}
14\usepackage{fancyvrb}
15% \usepackage{microtype}
16
17\author{Claudio Sacerdoti Coen}
18\title{Certified Complexity (CerCo)\\
19       Overall Presentation and Project Managemnt}
20\date{March 11, 2011}
21
22\setlength{\parskip}{1em}
23
24\AtBeginSection[]
25{
26  \begin{frame}<beamer>
27    \frametitle{Outline}
28    \tableofcontents[currentsection]
29  \end{frame}
30}
31
32\begin{document}
33
34\begin{frame}
35\maketitle
36\end{frame}
37
38\begin{frame}
39  \frametitle{Outline}
40  \tableofcontents
41\end{frame}
42
43\section{Long, middle and short term objectives}
44
45\begin{frame}
46 \frametitle{The ICT of the future}
47 We envision a (long term) future where formal methods will be pervasive:
48 \begin{center}
49   \alert{\Large Most programs will be (partially) specified and certified}
50 \end{center}
51
52 The very same definition of ``program'' will change:
53 \begin{center}
54  \alert{\Large A program will be a triple made of a specification,
55  an implementation and a proof certificate}
56 \end{center}
57
58 Cfr: Proof Carrying Code (PCC)
59\end{frame}
60
61\begin{frame}
62 \frametitle{The ICT of the future}
63 Signals in this direction:
64
65 \begin{itemize}
66  \item Formal methods are more and more embraced in industry
67  \item If total certification remains mostly unfeasible,
68        techniques for pay-as-you-ride certification are reaching larger
69        audiences\\
70        (model checking, type systems, abstract interpretation, dependent
71         types, \ldots)
72  \item Larger varities of user-friendly tools for partial certifications\\
73        (termination checkers, WCET analyzers, source code analyzers based
74         on WP, \ldots)
75  \item New open tools that integrate collaborating plug-ins to perform
76        automatic or interactive analyses (e.g. Frama-C)
77 \end{itemize}
78\end{frame}
79
80\begin{frame}
81 \frametitle{The ICT of the future}
82 Compiler = a tool to translates programs
83  \alert{preserving something}\\~\\
84
85 In our long-term vision:
86 \begin{center}
87 \alert{\Large A compiler maps triples specification-implementation-certificate
88  to triples specification-implementation-certificate.}
89 \end{center}
90
91 Questions:
92 \begin{enumerate}
93  \item What properties are \alert{preserved} during compilation?
94  \item What properties are \alert{affected} by the compilation strategy?
95  \item To what extent can you trust your compiler in preserving those properties?
96 \end{enumerate}
97\end{frame}
98
99\begin{frame}
100 \frametitle{The ICT of the future}
101 Preservation of properties during compilation:
102 \begin{itemize}
103  \item Extensional properties are easily specifiable and easily preserved
104        during compilation, but \alert{only assuming infinite resources}
105  \item Little is known even foundationally on the
106        \alert{preservation of intensional properties}
107        (e.g. use of space, time, energy)
108  \item For sure \alert{compilation} (which is not compositional)
109        \alert{affects the intensional properties}\\
110        E.g. the cost of different occurrences of $x+1$ can be different
111  \item Hence \alert{how} can you \alert{specify} intensional properties
112        as a function of the compilation strategy?
113 \end{itemize}
114\end{frame}
115
116\begin{frame}
117 \frametitle{Long term theoretical objectives}
118 \begin{enumerate}
119  \item to study the \alert{specification} of intensional properties
120        under \alert{realistic and precise cost models} induced by the
121        compilation strategy
122  \item to study \alert{preservation} of extensional and intensional
123        properties (\alert{under finiteness assumption})
124 \end{enumerate}
125
126 Byproducts:
127 \begin{enumerate}
128  \item being able to prove the efficacity of optimizations
129  \item being able to state completeness of compilation under
130        finiteness assumptions
131 \end{enumerate}
132\end{frame}
133
134\begin{frame}
135 \frametitle{Long term practical objectives}
136 \begin{enumerate}
137  \item allow developers of \alert{(hard) real time systems} to comfortably
138    prove meeting of deadline on \alert{high level languages} with the guarantee
139    that they hold on the object code
140  \item allow developers of \alert{embedded systems} to reason on
141    \alert{resource consumption} on \alert{high level languages} with the same
142     guarantee
143  \item augment the \alert{precision of formal methods} for intensional
144    properties on high level languages
145  \item obtain a new generation of \alert{precise and fully trustable WCET}
146    analyzers
147 \end{enumerate}
148\end{frame}
149
150\begin{frame}
151 \frametitle{Short term objectives}
152 \begin{enumerate}
153  \item develop a \alert{compiler} from
154        \alert{$\approx\!\!$ C} to the \alert{MCS-51} microprocessor
155        used for embedded systems
156  \item have the compiler infer from the assembly code a \alert{precise cost
157        model} for the source program
158  \item \alert{certify} the compiler
159  \item embed the compiler in a \alert{prototypical environment} for
160   \begin{itemize}
161    \item stating \alert{cost invariants} based on the inferred cost model
162    \item computing \alert{proof obligations}
163    \item \alert{proving} automatically or interactively the generated proof obligations
164   \end{itemize}
165  \item lift the technique to a \alert{synchronous languaged} (e.g. Esterel)
166        compiled via C
167 \end{enumerate}
168\end{frame}
169
170\begin{frame}
171 \frametitle{CerCo interaction diagram}
172 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
173\end{frame}
174
175\begin{frame}[fragile]
176 \frametitle{Source code}
177\begin{Verbatim}[commandchars=\\\{\}]
178char search (char tab[], char size, char to_find) \{
179  char low = 0, high = size-1, i;
180
181  while (high >= low) \{
182    i = (high+low) / 2;
183    if (tab[i] == to_find) return i;
184
185    if (tab[i] > to_find) high = i-1;
186
187    if (tab[i] < to_find) low = i+1;
188
189  \}
190
191  return (-1);
192\}
193\end{Verbatim}
194\end{frame}
195
196\begin{frame}[fragile]
197 \frametitle{Instrumented source code}
198\begin{Verbatim}[commandchars=\\\{\}]
199char search (char tab[], char size, char to_find) \{
200  char low = 0, high = size-1, i;
201  \alert{cost_incr(117);}
202  while (high >= low) \{
203    \alert{cost_incr(77);}
204    i = (high+low) / 2;
205    if (tab[i] == to_find) \{\alert{cost_incr(30);} return i;\}
206    \alert{else cost_incr(103);}
207    if (tab[i] > to_find) \{\alert{cost_incr(98);} high = i-1;\}
208    \alert{else cost_incr(85);}
209    if (tab[i] < to_find) \{\alert{cost_incr(98);} low = i+1;\}
210    \alert{else cost_incr(88);}
211  \}
212  \alert{cost_incr(43);}
213  return (-1);
214\}
215\end{Verbatim}
216\end{frame}
217
218\begin{frame}[fragile]
219 \frametitle{Foreseen problems}
220 \begin{itemize}
221  \item The \alert{high level implicit control structures}
222    (e.g. missing \texttt{else}) must be made explicit
223  \item Additional \alert{low level control structures} must be made explicit\\
224    (e.g. add low bytes; if overflow then add high bytes)\\
225    Alternative: loss of precision
226  \item The \alert{guards} of the low level control structures could be
227    \alert{``unrelated''} to the high level data\\
228    (e.g. if the carry bit is set then \ldots else \ldots)
229  \item Optimizations can \alert{modify the control flow}\\
230    (e.g. loop hoisting and unrolling)
231  \item The cost can depend on the data manipulated (\alert{dependent annotations}) (e.g. shift, multiplication in simple microprocessors)
232  \item Precise information on the source code required to avoid total
233    alteration (e.g. comments)
234 \end{itemize}
235\end{frame}
236
237\begin{frame}[fragile]
238 \frametitle{Foreseen problems}
239 Strategy in CerCo:
240 \begin{enumerate}
241  \item We consider \alert{simple optimizations} that do not alter the control
242    flow (cfr. CompCert)\\
243    The study of control flow altering optimizations left as optional
244  \item Complex low level control flows \alert{encapsulated} in library
245    functions (if possible) or else \alert{precision loss} (not required yet)
246  \item \alert{Partial alteration of the source program} for justified reasons
247    (e.g. explicit CFs) and for temporary ones (reusal of the CIL suite)\\
248    \alert{To be refined in the next periods}
249 \end{enumerate}
250\end{frame}
251
252\begin{frame}[fragile]
253 \frametitle{Cost invariants: loose invariants}
254{\small
255\begin{Verbatim}[commandchars=\\\{\}]
256char search (char tab[], char size, char to_find) \{
257  char low = 0, high = size-1, i;
258  cost_incr(117);
259  \alert{/* @ label L}
260     \alert{@ invariant cost <= at(cost,L) +}
261      \alert{(77+103+98+88)*((at(high,L) - at(low,L))/(high - low))-1) */}
262  while (high >= low) \{
263    cost_incr(\alert{77});
264    i = (high+low) / 2;
265    if (tab[i] == to_find) \{cost_incr(\alert{30}); return i;\}
266    else cost_incr(\alert{103});
267    if (tab[i] > to_find) \{cost_incr(\alert{98}); high = i-1;\}
268    else cost_incr(\alert{85});
269    if (tab[i] < to_find) \{cost_incr(\alert{98}); low = i+1;\}
270    else cost_incr(\alert{88});
271  \}
272  cost_incr(43);
273  return (-1);
274\}
275\end{Verbatim}
276}
277\end{frame}
278
279\begin{frame}[fragile]
280 \frametitle{Cost invariants: precise invariants}
281 When needed the \alert{user} can also state a precise invariant:
282 \begin{Verbatim}[commandchars=\\\{\}]
283 \alert{cost = at(cost,L) +}
284   \alert{(77 + 103 + 98 + 85) * min(0,#iterations - 1) +}
285   \alert{if tab[(high+low)/2] == to_find then 30 else 103 +}
286   \alert{3 * #high_decremented}
287 \end{Verbatim}
288 where \verb+#high_decremented+ has a complex description.\\~\\
289
290 The more precise the invariant, the more knowledge is required on the
291 extensional semantics of the program.
292\end{frame}
293
294\begin{frame}[fragile]
295 \frametitle{Proof obligations for costs}
296 \alert{Proof obligations} are then generated from the cost invariants using standard
297 techniques (e.g. Weakest Precondition generators for Hoare logic)\\~\\
298
299 \begin{itemize}
300  \item Can use off-the-shelf WP generators
301  \item Ad-hoc tactics/proof strategies to handle the proof obligations will
302        probably help
303 \end{itemize}
304\end{frame}
305
306\begin{frame}
307 \frametitle{Other cost obligations}
308 The same technique applies to: space (stack, heap), energy, etc.\\~\\
309
310 But
311 \begin{center}
312   \alert{\Large space constraints have an effect on the\\extensional semantics too}\end{center}
313
314 Similarly
315 \begin{center}
316   \alert{\Large time constraints have an effect on the\\extensional semantics too when\\considering timers or I/O}\end{center}
317\end{frame}
318
319\begin{frame}
320 \frametitle{Other cost obligations and embedded systems}
321 In CerCo \alert{we have not committed} to other kinds of costs but time.\\~\\
322
323 \alert{Embedded and reactive systems} could greatly benefit from space
324 constraints and from time in presence of timers.\\~\\
325
326 Compatibly with the project timing and effort required, we would like to
327 experiment with other costs too.\\~\\
328
329 Otherwise, this will be left to \alert{future work}.
330\end{frame}
331
332\begin{frame}
333 \frametitle{Case study interaction diagram}
334 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
335\end{frame}
336
337\section{Project context}
338
339\begin{frame}
340 \frametitle{Related work}
341 \alert{Invariant generation} (also for termination)
342 \begin{itemize}
343  \item Automatic and assisted invariant discovery plays a \alert{central role}
344    for the long term objectives
345  \item Existing techniques are \alert{fully orthogonal} to CerCo: we provide
346    a realistic and precise cost model to be used for cost invariants
347  \item CerCo will \alert{guarantee} that the inferred intensional properties
348    will \alert{carry over to assembly code}
349 \end{itemize}
350\end{frame}
351
352\begin{frame}
353 \frametitle{Related work}
354 \alert{Worst Case Execution Time}
355 \begin{itemize}
356  \item Sophisticated techniques for computing approximate costs of
357    object code programs
358  \item Can target modern architectures (caches, pipelines, reordering of
359    instructions, \ldots) using \alert{static (precise) or dinamic (empyrical)
360    techniques}
361  \item Main problem: \alert{how to relate} analysis on object code to the
362    intermediate and source languages and \alert{how to trust} the results
363  \item In CerCo:
364   \begin{enumerate}
365    \item Costs are tightly related by designing \alert{compilers} with this aim
366     (cfr. wcc)
367    \item WCET computations are \alert{certified}
368    \item \alert{Interactivity} vs full automation
369   \end{enumerate}
370  \item CerCo will target only a simple architecture;\\ \alert{combination} with
371    (dynamic?) WCET \alert{necessary}\\ in the long term
372 \end{itemize}
373\end{frame}
374
375\begin{frame}
376 \frametitle{Related work}
377 \alert{Compiler certification and interactive theorem proving}
378 \begin{itemize}
379  \item A large and older litterature that focuses on \alert{academic examples}
380  \item Some impressive recent examples that targets \alert{realistic
381    mildly optimizing compilers} (e.g. CompCert, FR)
382  \item On-going projects that targets more \alert{complex scenarios}:
383    intensional properties (CerCo, EU), whole software/hardware
384    architectures (e.g. VeriSoft, DE), concurrent systems (USA),
385    higher level languages, \ldots
386 \end{itemize}
387\end{frame}
388
389\section{Project planning and achievements}
390
391\begin{frame}
392 \includegraphics[height=8cm]{figs/pert.pdf}
393\end{frame}
394
395\begin{frame}
396 \frametitle{Achievements (1st period)}
397 Main theoretical achievements (D2.1):
398 \begin{center}
399  \alert{\Large a methodology for lifting in a provably correct way
400    costs on the object code to costs in the source code}
401 \end{center}~\\
402
403 Main practical achievements (D2.2):
404 \begin{center}
405  \alert{\Large an untrusted compiler from C-Light to the MCS-51 microprocessor
406   that lifts costs on the object code to costs in the source code}
407 \end{center}
408\end{frame}
409
410\begin{frame}
411 \frametitle{Achievements (1st period)}
412 More in detail:
413 \begin{enumerate}
414  \item The \alert{methodology itself}, with comparison with an alternative proposal (D2.1).  Main issues:
415   \begin{enumerate}
416    \item meaning of cost annotations
417    \item method to prove them sound and precise
418    \item \alert{compositionality}
419   \end{enumerate}
420  \item Assessment of the methodology: formalization of a \alert{toy compiler in Coq}
421  \item First untrusted prototype from C-Light to Mips
422  \item Full \alert{formalization} in O'Caml of the \alert{MCS-51} ``environment'':
423    \begin{enumerate}
424     \item ALU
425     \item UART, I/O lines, timers, interrupts
426     \item an assembly language with pseudo-instructions +\\ an assembler
427     \item an Intel HEX parser/pretty printer
428    \end{enumerate}
429 \end{enumerate}
430\end{frame}
431
432\begin{frame}
433 \frametitle{Achievements (1st period)}
434 More in detail:
435 \begin{enumerate}
436  \item \alert{Partial assessment} of the MCS-51 O'Caml formalization
437  \item \alert{Extension of C}, the CIL suite and the CompCert
438    \alert{memory model} to the MCS-51 unorthogonal memory model (new type and
439    pointer modifiers taken from SDCC)
440  \item \alert{Partial porting} of the CerCo untrusted prototype to the
441    MCS-51 and to the extended C
442  \item \alert{Partial porting} of the MCS-51 O'Caml formalization to Matita\\
443        The formalization is directly executable
444  \item \alert{Formalization} in Matita of the \alert{extended C-Light version}\\
445        The formalization is directly \alert{executable}
446  \item \alert{Partial assessment} of the executable semantics by
447        proving it equivalent to the CompCert one (up to extensions)
448 \end{enumerate}
449\end{frame}
450
451\begin{frame}
452 \frametitle{Assessment}
453 Assessment level and strategies:
454 \begin{enumerate}
455  \item Untrusted CerCo compiler (D2.2, M1):\\
456    the compiler will be \alert{fully certified};
457    several bugs already found after
458    the release of the deliverables
459  \item MCS-51 model (D4.1):\\
460    \alert{more thorough testing} vs emulators and real processors is
461    required;\\
462    minor impact on the rest of the projects;\\
463    the assembler will be certified (some bugs already found + unimplemented
464    features)
465  \item extended C semantics (D3.1):\\
466    already \alert{proved to be equivalent} to the CompCert one
467    (up to extensions);\\
468    we do not commit to support the planned extensions
469 \end{enumerate}
470\end{frame}
471
472\begin{frame}
473 \frametitle{Deviations from DoW}
474 \alert{Minor deviations} from the DoW
475 (no significant impact on the future schedule):
476 \begin{enumerate}
477  \item Late delivery of the deliverable related to the Web site and
478    internal work-flow due to hardware problems. \alert{Solved}
479  \item Compiler prototype D2.2 (M1):\\
480    computation of realistic costs requires full integration with D4.1
481    (not completed/tested at release time) \alert{Solved}
482  \item MCS-51 memory model + C extensions:\\
483    we did not foresee the need of MCS-51 specific extensions;\\
484    they will be taken in account with low priority\\
485    at the moment, only partially implemented in a branch of D2.2
486    not ready for release. \alert{Under consideration}
487 \end{enumerate}
488\end{frame}
489
490\begin{frame}
491 \frametitle{Foreseen deviations from DoW}
492 All sites have faced different hiring problems.\\~\\
493
494  UNIBO (Project Coordinator).\\
495   \alert{Personel planned:} 1 post-doc (24m) + 1 RTD (non permanent researcher) 24m\\
496   \alert{Personel acquired:} 1 post-doc (24m)\\
497   \alert{Cause:}
498   Because of the reform of the Italian University it has not been possible
499   to hire a RTD yet and it is unlikely to be possible to hire him soon.\\
500   \alert{Solution:} in place of the RTD, we will acquire two post-docs
501   (24m + 18m) that will start later then expected and will have a lower
502   level of expertise. Both positions are still waiting for clarifications
503   from the ministry or approval from the Corte dei Conti.\\
504   \alert{Expected impact:} delivery of D4.2 (month 18) could\\
505   be delayed with no impact on the next milestone\\
506   (M2, month 24), potential impact on M3, month 36.
507\end{frame}
508
509\begin{frame}
510 \hspace{-5cm}
511 \includegraphics[height=8cm]{figs/pert.pdf}
512\end{frame}
513
514\begin{frame}
515 \frametitle{Foreseen deviations from DoW}
516 All sites have faced different hiring problems.\\~\\
517
518  UPD.\\
519   \alert{Personel planned:} 1 post-doc (12m) + 1 PhD student (36m) + master students\\
520   \alert{Personel acquired:} 1 post-doc (12m) + 1 phd student (6m) + 2 master students\\
521   \alert{Cause:}
522    After 6 months of work the PhD student has decided to resign.
523    At this point, it is neither possible (incomplete funding)
524    nor desirable (bootstrapping period) to look for another PhD
525    student.\\
526   \alert{Solution:}
527    We plan --- if possible --- to extend as much as
528    possible the post-doc to cover also the second and/or third period.\\
529   \alert{Expected impact:} no major expected impact.
530\end{frame}
531
532\begin{frame}
533 \frametitle{Foreseen deviations from DoW}
534 All sites have faced different hiring problems.\\~\\
535
536  UEDIN.\\
537   \alert{Personel planned:} 1 lecturer (36m) + 1 post-doc (36m) + 1 phd-student \\
538   \alert{Personel acquired:} 1 lecturer (14m) + Senior lecturer (24m) + 1 post-doc
539   \alert{Cause:}
540    Dr. Randy Pollack (former site leader) is moving to Harvard.
541    He will be employed 90\% of his time there and 10\% on CerCo at UEDIN.
542    Dr. Ian Stark is the new site leader (since 01 February).
543    No student with appropriate background was found.\\
544   \alert{Solution:}
545    We plan to hire a post-doc during the later part of the project to
546    compensate for the missing PhD student.\\
547   \alert{Expected impact:} some trading of person-months between projects
548    and reassignment of costs: an experienced researcher will be more expensive
549    than a PhD student, but could reasonably expect to carry out the formal
550    proof work in less time than a student.
551\end{frame}
552
553\section{Project management}
554
555\begin{frame}
556 \frametitle{Management activities}
557 Management WP1:
558 \begin{enumerate}
559  \item to \alert{coordinate and supervise} activities to be
560    carried out
561  \item to carry out the overall \alert{administrative and
562    financial management} of the project
563  \item to manage \alert{contacts with the European Commission}
564  \item to \alert{monitor quality and timing} of project deliverables
565  \item to establish effective internal and external
566        \alert{communication procedures}
567 \end{enumerate}
568\end{frame}
569
570\begin{frame}
571 \frametitle{Consortium structure}
572 \includegraphics[height=8cm]{figs/management.pdf}
573\end{frame}
574
575\begin{frame}
576 \frametitle{Finantial management and coordination}
577 During first period:
578 \begin{enumerate}
579  \item transmission \alert{pre-financing} to all beneficiaries
580  \item \alert{providing} to partners detailed \alert{information} on consortium
581    organization and FP7 management rules during Kick Off
582  \item \alert{collecting and checking} partner's \alert{financial information} for the
583    First Progress Report
584  \item \alert{submission of financial statement} through NEF system (in progress)
585  \item gathering all necessary information and submission of \alert{management
586   reports, activity reports and deliverables}
587 \end{enumerate}
588\end{frame}
589
590\begin{frame}
591 \frametitle{Consortium agreement}
592 \begin{itemize}
593  \item signed in \alert{January 2010}
594  \item Intellectual Property Rights, Access Rights, roles,
595    functioning and responsibilities of governing bodies, liability of the
596    partners
597 \end{itemize}
598\end{frame}
599
600\begin{frame}
601 \frametitle{Periodic Meetings}
602 Four project meetings during first period (two planned in the DoW):
603 \begin{itemize}
604  \item \alert{Kick-off, Bologna, February 2010.}\\
605   coordination of research activities, planning of future work,
606   financial and administrative organization
607  \item \alert{Project meeting, Edinburgh, July 2010.}\\
608   Just after D2.1. Fixing more precise scheduling; first informal
609   dissemination via co-location with FLOC
610  \item \alert{Project meeting, Paris, Septermber 2010.}\\
611   Adoption of the MCS-51 target; discussion of the design of the costing
612   compiler (D2.2), memory model (D4.1). Integration problems foreseen.
613  \item \alert{Implementer's meeting, Bologna, January 2011}\\
614   Addressing remaining integration problems regarding\\ D2.2, D3.1 and D4.1.
615   Post-poning some integration\\ steps to Task 2.4 (second period).
616 \end{itemize}
617\end{frame}
618
619\end{document}
Note: See TracBrowser for help on using the repository browser.