source: Deliverables/D1.1/Presentations/management_and_overall-sacerdoti-presentation.tex @ 652

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

Still unfinished.

File size: 10.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\begin{document}
25
26\begin{frame}
27\maketitle
28\end{frame}
29
30\begin{frame}
31 \frametitle{The ICT of the future}
32 We envision a (long term) future where formal methods will be pervasive:
33 \begin{center}
34   \alert{\Large Most programs will be (partially) specified and certified}
35 \end{center}
36
37 The very same definition of ``program'' will change:
38 \begin{center}
39  \alert{\Large A program will be a triple made of a specification,
40  an implementation and a proof certificate}
41 \end{center}
42
43 Cfr: Proof Carrying Code (PCC)
44\end{frame}
45
46\begin{frame}
47 \frametitle{The ICT of the future}
48 Signals in this direction:
49
50 \begin{itemize}
51  \item Formal methods are more and more embraced in industry
52  \item If total certification remains mostly unfeasible,
53        techniques for pay-as-you-ride certification are reaching larger
54        audiences\\
55        (model checking, type systems, abstract interpretation, dependent
56         types, \ldots)
57  \item Larger varities of user-friendly tools for partial certifications\\
58        (termination checkers, WCET analyzers, source code analyzers based
59         on WP, \ldots)
60  \item New open tools that integrate collaborating plug-ins to perform
61        automatic or interactive analyses (e.g. Frama-C)
62 \end{itemize}
63\end{frame}
64
65\begin{frame}
66 \frametitle{The ICT of the future}
67 Compiler = a tool to translates programs
68  \alert{preserving something}\\~\\
69
70 In our long-term vision:
71 \begin{center}
72 \alert{\Large A compiler maps triples specification-implementation-certificate
73  to triples specification-implementation-certificate.}
74 \end{center}
75
76 Questions:
77 \begin{enumerate}
78  \item What properties are \alert{preserved} during compilation?
79  \item What properties are \alert{affected} by the compilation strategy?
80  \item To what extent can you trust your compiler in preserving those properties?
81 \end{enumerate}
82\end{frame}
83
84\begin{frame}
85 \frametitle{The ICT of the future}
86 Preservation of properties during compilation:
87 \begin{itemize}
88  \item Extensional properties are easily specifiable and easily preserved
89        during compilation, but \alert{only assuming infinite resources}
90  \item Little is known even foundationally on the
91        \alert{preservation of intensional properties}
92        (e.g. use of space, time, energy)
93  \item For sure \alert{compilation} (which is not compositional)
94        \alert{affects the intensional properties}\\
95        E.g. the cost of different occurrences of $x+1$ can be different
96  \item Hence \alert{how} can you \alert{specify} intensional properties
97        as a function of the compilation strategy?
98 \end{itemize}
99\end{frame}
100
101\begin{frame}
102 \frametitle{Long term theoretical objectives}
103 \begin{enumerate}
104  \item to study the \alert{specification} of intensional properties
105        under \alert{realistic and precise cost models} induced by the
106        compilation strategy
107  \item to study \alert{preservation} of extensional and intensional
108        properties (\alert{under finiteness assumption})
109 \end{enumerate}
110
111 Byproducts:
112 \begin{enumerate}
113  \item being able to prove the efficacity of optimizations
114  \item being able to state completeness of compilation under
115        finiteness assumptions
116 \end{enumerate}
117\end{frame}
118
119\begin{frame}
120 \frametitle{Long term practical objectives}
121 \begin{enumerate}
122  \item allow developers of \alert{(hard) real time systems} to comfortably
123    prove meeting of deadline on \alert{high level languages} with the guarantee
124    that they hold on the object code
125  \item allow developers of \alert{embedded systems} to reason on
126    \alert{resource consumption} on \alert{high level languages} with the same
127     guarantee
128  \item augment the \alert{precision of formal methods} for intensional
129    properties on high level languages
130  \item obtain a new generation of \alert{precise and fully trustable WCET}
131    analyzers
132 \end{enumerate}
133\end{frame}
134
135\begin{frame}
136 \frametitle{Short term objectives}
137 \begin{enumerate}
138  \item develop a \alert{compiler} from
139        \alert{$\approx\!\!$ C} to the \alert{MCS-51} microprocessor
140        used for embedded systems
141  \item have the compiler infer from the assembly code a \alert{precise cost
142        model} for the source program
143  \item \alert{certify} the compiler
144  \item embed the compiler in a \alert{prototypical environment} for
145   \begin{itemize}
146    \item stating \alert{cost invariants} based on the inferred cost model
147    \item computing \alert{proof obligations}
148    \item \alert{proving} automatically or interactively the generated proof obligations
149   \end{itemize}
150  \item lift the technique to a \alert{synchronous languaged} (e.g. Esterel)
151        compiled via C
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}[fragile]
161 \frametitle{Source code}
162\begin{Verbatim}[commandchars=\\\{\}]
163char search (char tab[], char size, char to_find) \{
164  char low = 0, high = size-1, i;
165
166  while (high >= low) \{
167    i = (high+low) / 2;
168    if (tab[i] == to_find) return i;
169
170    if (tab[i] > to_find) high = i-1;
171
172    if (tab[i] < to_find) low = i+1;
173
174  \}
175
176  return (-1);
177\}
178\end{Verbatim}
179\end{frame}
180
181\begin{frame}[fragile]
182 \frametitle{Instrumented source code}
183\begin{Verbatim}[commandchars=\\\{\}]
184char search (char tab[], char size, char to_find) \{
185  char low = 0, high = size-1, i;
186  \alert{cost_incr(117);}
187  while (high >= low) \{
188    \alert{cost_incr(77);}
189    i = (high+low) / 2;
190    if (tab[i] == to_find) \{\alert{cost_incr(30);} return i;\}
191    \alert{else cost_incr(103);}
192    if (tab[i] > to_find) \{\alert{cost_incr(98);} high = i-1;\}
193    \alert{else cost_incr(85);}
194    if (tab[i] < to_find) \{\alert{cost_incr(98);} low = i+1;\}
195    \alert{else cost_incr(88);}
196  \}
197  \alert{cost_incr(43);}
198  return (-1);
199\}
200\end{Verbatim}
201\end{frame}
202
203\begin{frame}[fragile]
204 \frametitle{Foreseen problems}
205 \begin{itemize}
206  \item The \alert{high level implicit control structures}
207    (e.g. missing \texttt{else}) must be made explicit
208  \item Additional \alert{low level control structures} must be made explicit\\
209    (e.g. add low bytes; if overflow then add high bytes)\\
210    Alternative: loss of precision
211  \item The \alert{guards} of the low level control structures could be
212    \alert{``unrelated''} to the high level data\\
213    (e.g. if the carry bit is set then \ldots else \ldots)
214  \item Optimizations can \alert{modify the control flow}\\
215    (e.g. loop hoisting and unrolling)
216  \item The cost can depend on the data manipulated (\alert{dependent annotations}) (e.g. shift, multiplication in simple microprocessors)
217  \item Precise information on the source code required to avoid total
218    alteration (e.g. comments)
219 \end{itemize}
220\end{frame}
221
222\begin{frame}[fragile]
223 \frametitle{Foreseen problems}
224 Strategy in CerCo:
225 \begin{enumerate}
226  \item We consider \alert{simple optimizations} that do not alter the control
227    flow (cfr. CompCert)\\
228    The study of control flow altering optimizations left as optional
229  \item Complex low level control flows \alert{encapsulated} in library
230    functions (if possible) or else \alert{precision loss} (not required yet)
231  \item \alert{Partial alteration of the source program} for justified reasons
232    (e.g. explicit CFs) and for temporary ones (reusal of the CIL suite)\\
233    \alert{To be refined in the next periods}
234 \end{enumerate}
235\end{frame}
236
237\begin{frame}[fragile]
238 \frametitle{Cost invariants: loose invariants}
239{\small
240\begin{Verbatim}[commandchars=\\\{\}]
241char search (char tab[], char size, char to_find) \{
242  char low = 0, high = size-1, i;
243  cost_incr(117);
244  \alert{/* @ label L}
245     \alert{@ invariant cost <= at(cost,L) +}
246      \alert{(77+103+98+88)*((at(high,L) - at(low,L))/(high - low))-1) */}
247  while (high >= low) \{
248    cost_incr(\alert{77});
249    i = (high+low) / 2;
250    if (tab[i] == to_find) \{cost_incr(\alert{30}); return i;\}
251    else cost_incr(\alert{103});
252    if (tab[i] > to_find) \{cost_incr(\alert{98}); high = i-1;\}
253    else cost_incr(\alert{85});
254    if (tab[i] < to_find) \{cost_incr(\alert{98}); low = i+1;\}
255    else cost_incr(\alert{88});
256  \}
257  cost_incr(43);
258  return (-1);
259\}
260\end{Verbatim}
261}
262\end{frame}
263
264\begin{frame}[fragile]
265 \frametitle{Cost invariants: precise invariants}
266 When needed the \alert{user} can also state a precise invariant:
267 \begin{Verbatim}[commandchars=\\\{\}]
268 \alert{cost = at(cost,L) +}
269   \alert{(77 + 103 + 98 + 85) * min(0,#iterations - 1) +}
270   \alert{if tab[(high+low)/2] == to_find then 30 else 103 +}
271   \alert{3 * #high_decremented}
272 \end{Verbatim}
273 where \verb+#high_decremented+ has a complex description.\\~\\
274
275 The more precise the invariant, the more knowledge is required on the
276 extensional semantics of the program.
277\end{frame}
278
279\begin{frame}[fragile]
280 \frametitle{Proof obligations for costs}
281 \alert{Proof obligations} are then generated from the cost invariants using standard
282 techniques (e.g. Weakest Precondition generators for Hoare logic)\\~\\
283
284 \begin{itemize}
285  \item Can use off-the-shelf WP generators
286  \item Ad-hoc tactics/proof strategies to handle the proof obligations will
287        probably help
288 \end{itemize}
289\end{frame}
290
291\begin{frame}
292 \frametitle{Other cost obligations}
293 The same technique applies to: space (stack, heap), energy, etc.\\~\\
294
295 But
296 \begin{center}
297   \alert{\Large space constraints have an effect on the\\extensional semantics too}\end{center}
298
299 Similarly
300 \begin{center}
301   \alert{\Large time constraints have an effect on the\\extensional semantics too when\\considering timers or I/O}\end{center}
302\end{frame}
303
304\begin{frame}
305 \frametitle{Other cost obligations and embedded systems}
306 In CerCo \alert{we have not committed} to other kinds of costs but time.\\~\\
307
308 \alert{Embedded and reactive systems} could greatly benefit from space
309 constraints and from time in presence of timers.\\~\\
310
311 Compatibly with the project timing and effort required, we would like to
312 experiment with other costs too.\\~\\
313
314 Otherwise, this will be left to \alert{future work}.
315\end{frame}
316
317\begin{frame}
318 \frametitle{Case study interaction diagram}
319 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
320\end{frame}
321
322\begin{frame}
323 \includegraphics[height=8cm]{figs/pert.pdf}
324\end{frame}
325
326\end{document}
Note: See TracBrowser for help on using the repository browser.