1 | %%% \listfiles %%%%%%%%%%%%%%%%%% POWERDOT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
2 | \documentclass[ |
---|
3 | %% mode=present, |
---|
4 | %% mode=print, |
---|
5 | % mode=handout, |
---|
6 | % nopagebreaks, |
---|
7 | %paper=a4paper, |
---|
8 | paper=screen, |
---|
9 | %% display=slidesnotes, |
---|
10 | %% size=11pt, |
---|
11 | %% size=12pt, |
---|
12 | %% size=14pt, |
---|
13 | %% size=17pt, |
---|
14 | %% size=20pt, |
---|
15 | style=simple, |
---|
16 | %% style=fyma, |
---|
17 | %% orient=portrait, |
---|
18 | %% blackslide, |
---|
19 | %% fleqn, |
---|
20 | % clock, |
---|
21 | ]{powerdot} |
---|
22 | %\documentclass[mode=handout,nopagebreaks,paper=a4paper]{powerdot} |
---|
23 | |
---|
24 | %\usepackage[latin1]{inputenc} |
---|
25 | \usepackage{pstricks,pst-node,pst-text,pst-tree} |
---|
26 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
27 | % Work around some bugs in marvosym with overwriting symbols: |
---|
28 | \let\labOrigRightarrow=\Rightarrow |
---|
29 | \RequirePackage{marvosym} |
---|
30 | \let\Rightarrow=\labOrigRightarrow |
---|
31 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
32 | %\usepackage{mathabx} |
---|
33 | \usepackage{amsmath} |
---|
34 | \usepackage{amsfonts} |
---|
35 | \usepackage{amsbsy} |
---|
36 | \usepackage{amssymb} |
---|
37 | \usepackage{latexsym} |
---|
38 | \usepackage[mathscr]{euscript} |
---|
39 | %\usepackage{framed} |
---|
40 | %\usepackage[framed]{ntheorem} |
---|
41 | \usepackage[all,color,dvips]{xy} |
---|
42 | %\UseCrayolaColors |
---|
43 | %\usepackage{amsfonts} |
---|
44 | %\usepackage{graphicx} |
---|
45 | %\usepackage{color} |
---|
46 | \usepackage{colortbl} |
---|
47 | \usepackage{stmaryrd} |
---|
48 | %\usepackage{mathabx} |
---|
49 | %\usepackage[bbgreekl]{mathbbol} |
---|
50 | %\usepackage{epic,eepic} |
---|
51 | %\usepackage{xcolor} |
---|
52 | %\usepackage{pifont} |
---|
53 | \usepackage{proof} |
---|
54 | \usepackage{cmll} |
---|
55 | |
---|
56 | |
---|
57 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
58 | % Personal VERBATIM and CODE |
---|
59 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
60 | %\usepackage{fancybox} |
---|
61 | %\usepackage{fancyvrb} |
---|
62 | %\usepackage{verbatim} |
---|
63 | %\usepackage{listings} |
---|
64 | %\lstnewenvironment{code}{% |
---|
65 | %\lstset{frame=single,escapeinside=`', |
---|
66 | % backgroundcolor=\color{yellow!20}, |
---|
67 | % language=lisp, |
---|
68 | % basicstyle=\footnotesize\ttfamily}}{} |
---|
69 | |
---|
70 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
71 | % Personal Definition of new colors |
---|
72 | \usepackage{crayola} |
---|
73 | %%%%% COLORI TRASPARENTI %%%%%%%%%%%%%%% |
---|
74 | %\usepackage{pstricks-add} |
---|
75 | % \defineTColor{TRed}{red} |
---|
76 | % \defineTColor{TGreen}{green} |
---|
77 | % \defineTColor{TBlue}{blue} |
---|
78 | % \defineTColor{TBlue}{blue} |
---|
79 | % \defineTColor{TLemon}{LemonChiffon} |
---|
80 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
81 | \usepackage{listings} |
---|
82 | \def\lstlanguagefiles{lst-grafite.tex} |
---|
83 | |
---|
84 | |
---|
85 | \def\tuple#1{\langle #1 \rangle} |
---|
86 | \input{unimacro.tex} |
---|
87 | %\newcommand\emslide[3]{\onslide*{#1}{#2}\onslide*{#3}{\psframebox[fillstyle=solid,fillcolor=Yellow,linecolor=Yellow]{#2}}} |
---|
88 | |
---|
89 | \title{\blue The Labelling Approach to Precise Resource Analysis on the Source Code, Revisited\\[3mm]} |
---|
90 | \author{ |
---|
91 | \hspace*{9mm} \begin{tabular}{l} |
---|
92 | {\red Mauro Piccolo} \\[1mm] |
---|
93 | %\href{http://www.di.unito.it/~paolini}{\red Luca Paolini} \\[1mm] |
---|
94 | %{\tt paolini@di.unito.it}\\[1mm] |
---|
95 | {Universit\`a di Torino}\\ |
---|
96 | {Dipartimento di Informatica}\\[3mm] |
---|
97 | {\red A joint work with Claudio Sacerdoti Coen and Paolo Tranquilli}\\[3mm] |
---|
98 | \end{tabular} |
---|
99 | } |
---|
100 | \date{\hspace*{9mm} DICE 2014 Grenoble, 6 April 2014} |
---|
101 | |
---|
102 | \begin{document} |
---|
103 | \maketitle |
---|
104 | \begin{wideslide}{Concrete and certified complexity} |
---|
105 | $\;$\\[-7mm] |
---|
106 | \includegraphics[width=\textwidth]{code.eps} |
---|
107 | \\[-5mm] |
---|
108 | \begin{itemize} |
---|
109 | \item Reasoning about the complexity is rather made on the source.\\[-2mm] |
---|
110 | \item Concrete execution costs are better guess on the binary code. |
---|
111 | \end{itemize} |
---|
112 | \begin{center} |
---|
113 | \\[-10mm] |
---|
114 | How can we {\blue lift} in a provably correct way information on the execution cost of the binary code to cost annotation on the source code? |
---|
115 | \end{center} |
---|
116 | \end{wideslide} |
---|
117 | |
---|
118 | \begin{wideslide}[method=direct,toc=Labelling approach]{Labelling approach (Ayache, Amadio and R\'egis-Gianas)} |
---|
119 | The user writes the program |
---|
120 | \begin{lstlisting} |
---|
121 | I1; |
---|
122 | for(int i=0;i<2;i++){ |
---|
123 | I2; |
---|
124 | } |
---|
125 | \end{lstlisting} |
---|
126 | \end{wideslide} |
---|
127 | |
---|
128 | \begin{wideslide}[method=direct,toc=Labelling approach]{Labelling approach} |
---|
129 | The program will be processed by a special pre-compiler which inserts some label emission statements |
---|
130 | \begin{lstlisting} |
---|
131 | EMIT L1; |
---|
132 | I1; |
---|
133 | for(int i=0;i<2;i++){ |
---|
134 | EMIT L2; |
---|
135 | I2; |
---|
136 | } |
---|
137 | EMIT L3; |
---|
138 | \end{lstlisting} |
---|
139 | \end{wideslide} |
---|
140 | |
---|
141 | \begin{wideslide}[method=file,toc=Labelling approach]{Labelling approach} |
---|
142 | \onslide*{1}{The program is then compiled into an object code emitting the same sequence of labels} |
---|
143 | \onslide*{2}{The object code is processed by a static code analyzer to determine the cost of each block of code} |
---|
144 | \begin{center} |
---|
145 | \begin{tabular}{l l l} |
---|
146 | \begin{lstlisting} |
---|
147 | EMIT L1; |
---|
148 | I1; |
---|
149 | for(int i=0;i<2;i++){ |
---|
150 | EMIT L2; |
---|
151 | I2; |
---|
152 | } |
---|
153 | EMIT L3; |
---|
154 | \end{lstlisting} |
---|
155 | &$\qquad$& |
---|
156 | \begin{lstlisting} |
---|
157 | EMIT L1; |
---|
158 | I3 |
---|
159 | l1: COND l1 |
---|
160 | EMIT L2 |
---|
161 | I4 |
---|
162 | GOTO l1 |
---|
163 | l2: EMIT L3 |
---|
164 | \end{lstlisting} |
---|
165 | \end{tabular} |
---|
166 | \end{center} |
---|
167 | \onslide*{2}{ |
---|
168 | \begin{center} |
---|
169 | \begin{tabular}{|l|l|} |
---|
170 | \hline |
---|
171 | Label & Cost \\ |
---|
172 | \hline |
---|
173 | L1 & $cost(I3) + cost(COND \ l1) = k_1$ \\ |
---|
174 | L2 & $cost(I4) + cost(GOTO \ l1) = k_2$ \\ |
---|
175 | L3 & $k_3$\\ |
---|
176 | \hline |
---|
177 | \end{tabular} |
---|
178 | \end{center} |
---|
179 | } |
---|
180 | \end{wideslide} |
---|
181 | \begin{wideslide}[method=direct]{Labelling approach} |
---|
182 | The complier gives an instrumented version of the source code |
---|
183 | \begin{center} |
---|
184 | \begin{tabular}{l l l} |
---|
185 | \begin{lstlisting} |
---|
186 | cost += k_1 |
---|
187 | instr 1; |
---|
188 | for(int i=0;i<2;i++){ |
---|
189 | cost += k_2 |
---|
190 | instr 2; |
---|
191 | } |
---|
192 | cost += k_3 |
---|
193 | \end{lstlisting} |
---|
194 | &$\qquad$& |
---|
195 | \begin{lstlisting} |
---|
196 | EMIT L1; |
---|
197 | instr 3 |
---|
198 | l1: COND l1 |
---|
199 | EMIT L2 |
---|
200 | instr 4 |
---|
201 | GOTO l1 |
---|
202 | l2: EMIT L3 |
---|
203 | \end{lstlisting} |
---|
204 | \end{tabular} |
---|
205 | \end{center} |
---|
206 | $\;$ \\ |
---|
207 | \psshadowbox{ |
---|
208 | \begin{minipage}{10.5cm} |
---|
209 | \centering We can make assertions on the variable cost which contains the {\red precise} cost of the computation. |
---|
210 | \end{minipage} |
---|
211 | } |
---|
212 | $\;$\\[3mm] |
---|
213 | Precise means that the predicted cost and the real one is bounded by a constant $\delta$ that depends only on the program (not on the input!). |
---|
214 | \end{wideslide} |
---|
215 | |
---|
216 | \begin{wideslide}{Certified complexity} |
---|
217 | $\;$\\[-9mm] |
---|
218 | \begin{center} |
---|
219 | \includegraphics[width=7cm]{cerco.eps} |
---|
220 | \end{center} |
---|
221 | This talk: |
---|
222 | \psshadowbox{ |
---|
223 | \begin{minipage}{12cm} |
---|
224 | \begin{itemize} |
---|
225 | \item There are some hidden assumption and limitations of labelling approach: {\red instructions with multiple predecessors} and {\red function calls}. |
---|
226 | \item We present a {\red revisitation of labelling approach} able to cope the above mentioned limitations. |
---|
227 | \item All the presented results have been formalized in the {\red Matita proof assistant}. |
---|
228 | \end{itemize} |
---|
229 | \end{minipage} |
---|
230 | } |
---|
231 | \end{wideslide} |
---|
232 | |
---|
233 | |
---|
234 | |
---|
235 | \begin{wideslide}[method=direct]{Conditional statements and multiple predecessors} |
---|
236 | $\;$\\[-4mm] |
---|
237 | {\red Assumptions:} |
---|
238 | \psshadowbox{ |
---|
239 | \begin{minipage}{12cm} |
---|
240 | \begin{itemize} |
---|
241 | \item Each object code instruction should fall into the scope of a label. |
---|
242 | \item Each object code instruction having multiple successors (e.g. conditionals) should pass control to basic blocks starting with a label emission statement. |
---|
243 | \item The cost of the conditional instruction should be the same whatever branch is taken. |
---|
244 | \end{itemize} |
---|
245 | \end{minipage} |
---|
246 | } \\[4mm] |
---|
247 | {\red Problem!} \\ |
---|
248 | \begin{tabular}[t]{l l l l l} |
---|
249 | \begin{lstlisting} |
---|
250 | if(E){ |
---|
251 | EMIT L; |
---|
252 | I; |
---|
253 | } |
---|
254 | \end{lstlisting} |
---|
255 | & $\qquad\qquad$ & |
---|
256 | \begin{lstlisting} |
---|
257 | SJNEQ l1 |
---|
258 | JUMP l3 |
---|
259 | l1: JUMP l2 |
---|
260 | ... |
---|
261 | l2: EMIT L |
---|
262 | I; |
---|
263 | \end{lstlisting} |
---|
264 | & $\qquad\qquad$ & |
---|
265 | \begin{lstlisting} |
---|
266 | SJNEQ l1 |
---|
267 | JUMP l3 |
---|
268 | l1: EMIT L |
---|
269 | JUMP l2 |
---|
270 | ... |
---|
271 | l2: I; |
---|
272 | \end{lstlisting} |
---|
273 | \end{tabular} |
---|
274 | \end{wideslide} |
---|
275 | |
---|
276 | \begin{wideslide}[method=direct]{Solution: labelled transition system semantics} |
---|
277 | \begin{itemize} |
---|
278 | \item We incorporate label emission in the semantics of the instructions. |
---|
279 | \item No more label emission statements. |
---|
280 | \end{itemize} |
---|
281 | \begin{lstlisting}[language=Grafite] |
---|
282 | record abstract_status : Type[2] ≝ |
---|
283 | { as_status :> Type[0] |
---|
284 | ; as_execute : ActionLabel → relation as_status |
---|
285 | ; as_syntactical_succ : relation as_status |
---|
286 | ; as_classify : as_status → status_class |
---|
287 | ; as_initial : as_status → bool |
---|
288 | ; as_final : as_status → bool |
---|
289 | ; jump_emits : ∀s1,s2,l.as_classify ... s1 = cl_jump → |
---|
290 | as_execute l s1 s2 → is_non_silent_cost_act l |
---|
291 | }. |
---|
292 | \end{lstlisting} |
---|
293 | \end{wideslide} |
---|
294 | |
---|
295 | \begin{wideslide}[method=file]{Function calls} |
---|
296 | \begin{center} |
---|
297 | \begin{tabular}{l l l} |
---|
298 | \begin{lstlisting} |
---|
299 | void main(){ |
---|
300 | EMIT L1; |
---|
301 | I1; |
---|
302 | (*f)(); |
---|
303 | I2; |
---|
304 | } |
---|
305 | |
---|
306 | void g(){ |
---|
307 | EMIT L2; |
---|
308 | I3; |
---|
309 | } |
---|
310 | \end{lstlisting} |
---|
311 | & $\qquad\qquad$ & |
---|
312 | \begin{lstlisting} |
---|
313 | main : |
---|
314 | EMIT L1 |
---|
315 | I4 |
---|
316 | CALL |
---|
317 | I5 |
---|
318 | RETURN |
---|
319 | |
---|
320 | g : |
---|
321 | EMIT L2 |
---|
322 | I6; |
---|
323 | RETURN |
---|
324 | \end{lstlisting} |
---|
325 | \end{tabular} |
---|
326 | \end{center} |
---|
327 | What label should pay the cost for the block I5? \\ |
---|
328 | \onslide{2}{ |
---|
329 | {\red The only reasonable answer is L1!} |
---|
330 | } |
---|
331 | \end{wideslide} |
---|
332 | |
---|
333 | \begin{wideslide}{Label emission and function calls} |
---|
334 | $\;$ \\[-5mm] |
---|
335 | \psshadowbox{ |
---|
336 | \begin{minipage}{12cm} |
---|
337 | The scope of labels should extend to the next label emission statement or the end of the function, stepping over function calls. |
---|
338 | \end{minipage} |
---|
339 | }\\[3mm] |
---|
340 | {\red Assumptions:} |
---|
341 | \begin{itemize} |
---|
342 | \item All the instruction in the (static) block are reached during computation. |
---|
343 | \item The cost function should be commutative. |
---|
344 | \end{itemize} |
---|
345 | {\red Problems:} |
---|
346 | \begin{itemize} |
---|
347 | \item It does not work with {\blue non-commutative cost functions}. Because of stateful hardware components (cache, pipelines ...) this method does not scale to {\blue modern hardware}. |
---|
348 | \item It does not work with {\blue compiler that do not respect the calling structure} of the source code because it is not possible to statically predict {\blue which instruction will be executed after a function return}. |
---|
349 | \end{itemize} |
---|
350 | \end{wideslide} |
---|
351 | |
---|
352 | \begin{wideslide}[method=direct]{First solution: structured traces} |
---|
353 | \begin{itemize} |
---|
354 | \item The usual notion of {\red flat execution trace} is inadequate for a simulation argument. |
---|
355 | \item {\red Embed the call/return} into execution trace. |
---|
356 | \item Traces of called function are {\red nested}, invariants on position of costlabels are {\red enforced} and steps are grouped {\red according to costlabels}. |
---|
357 | \end{itemize} |
---|
358 | \begin{center} |
---|
359 | \includegraphics[width=8cm]{trace.eps} |
---|
360 | \end{center} |
---|
361 | \end{wideslide} |
---|
362 | |
---|
363 | \begin{wideslide}[method=direct]{Measurable traces} |
---|
364 | $\;$\\[-7mm] |
---|
365 | \begin{lstlisting}[language=Grafite] |
---|
366 | inductive pre_measurable_trace (S : abstract_status) : |
---|
367 | ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ |
---|
368 | | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base… st) |
---|
369 | | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel. |
---|
370 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
---|
371 | as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → |
---|
372 | pre_measurable_trace … (t_ind … prf … tl) |
---|
373 | ……… |
---|
374 | | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2. |
---|
375 | ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3. |
---|
376 | ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4. |
---|
377 | as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io |
---|
378 | → is_call_act l1 → ¬ is_call_post_label … st1 → |
---|
379 | pre_measurable_trace … t1 → pre_measurable_trace … t2 → |
---|
380 | as_syntactical_succ S st1 st4 → |
---|
381 | is_unlabelled_ret_act l2 → |
---|
382 | pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))). |
---|
383 | \end{lstlisting} |
---|
384 | \end{wideslide} |
---|
385 | |
---|
386 | \begin{wideslide}[method=direct]{Simulation statement} |
---|
387 | $\;$\\[-7mm] |
---|
388 | \begin{lstlisting}[language=Grafite] |
---|
389 | theorem simulates_pre_mesurable: |
---|
390 | ∀S : abstract_status.∀rel : relations S.∀s1,s1' : S. ∀t1: raw_trace S s1 s1'. |
---|
391 | simulation_conditions S rel → pre_measurable_trace … t1 → ∀s2 : S.as_classify … s2 ≠ cl_io → Srel … rel s1 s2 → ∃s2'. ∃t2: raw_trace … s2 s2'.pre_measurable_trace … t2 ∧ get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ Srel … rel s1' s2'. |
---|
392 | \end{lstlisting} |
---|
393 | \begin{itemize} |
---|
394 | \item Simulation conditions are local conditions for {\red sequential}, {\red conditional}, {\red call} and {\red return} steps. |
---|
395 | \begin{center} |
---|
396 | \includegraphics[width=5cm]{diag.eps} |
---|
397 | \end{center} |
---|
398 | \item The generated trace should contain {\red the same sequence of costlabels} (up to permutation) of the starting one. |
---|
399 | \end{itemize} |
---|
400 | \end{wideslide} |
---|
401 | |
---|
402 | \begin{wideslide}{Return instructions are labelled} |
---|
403 | $\;$\\[-7mm] |
---|
404 | {\red Problems} |
---|
405 | \begin{itemize} |
---|
406 | \item Local simulation condition are quite techical and the beauty of simulation argument |
---|
407 | is lost in details. |
---|
408 | \item It does not solve the problem with stateful hardware, since the cost function is |
---|
409 | still requirred to be commutative. |
---|
410 | \end{itemize} |
---|
411 | \psshadowbox{ |
---|
412 | \begin{minipage}{12cm} |
---|
413 | We ask every function call to be immediately followed by a label emission statement so the scope of a label no longer extends after a function call. |
---|
414 | \end{minipage} |
---|
415 | } |
---|
416 | $\;$\\ |
---|
417 | {\red Drawbacks} |
---|
418 | \begin{itemize} |
---|
419 | \item A lot of labels should be injected in the code! |
---|
420 | \item The value of the variable $\tt cost$ at the end of a block containing function-calls is the sum of the increments that occurs after every call. |
---|
421 | \item A proof of termination is requirred! |
---|
422 | \end{itemize} |
---|
423 | \end{wideslide} |
---|
424 | |
---|
425 | \begin{wideslide}[method=direct]{Return post label pass} |
---|
426 | We define a {\blue sound and precise} translation to a program having all return instructions that are followed by a label emission. |
---|
427 | \begin{lstlisting}[language=Grafite] |
---|
428 | lemma correctness : ∀p,p',prog.no_duplicates_labels … prog → let 〈t_prog,m,keep〉 ≝ trans_prog … prog in ∀s1,s2,s1' : state p.∀abs_top,abs_tail. |
---|
429 | ∀t : raw_trace (operational_semantics…p' prog) s1 s2.pre_measurable_trace…t → state_rel…m keep abs_top abs_tail s1 s1' → ∃abs_top',abs_tail'.∃s2'. |
---|
430 | ∃t' : raw_trace (operational_semantics…p' t_prog) s1' s2'. |
---|
431 | state_rel…m keep abs_top' abs_tail' s2 s2' ∧ is_permutation … ∧ len…t = len…t' ∧ pre_measurable_trace…t'. |
---|
432 | \end{lstlisting} |
---|
433 | \begin{itemize} |
---|
434 | \item {\blue Benefits}: the user can reason with smaller blocks and simpler costs and the compiler do not need to care about extra invariant. |
---|
435 | \item {\red Drawbacks}: This pass is not always possible in case of non commutative costs. |
---|
436 | \end{itemize} |
---|
437 | \end{wideslide} |
---|
438 | |
---|
439 | \begin{wideslide}[method=direct]{Static/dynamic correctness} |
---|
440 | \begin{lstlisting}[language=Grafite] |
---|
441 | lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog. |
---|
442 | ∀abs_t : abstract_transition_sys (m…p').∀instr_m. |
---|
443 | ∀good : static_galois…(asm_static_analisys_data p p' prog abs_t instr_m). |
---|
444 | ∀mT,map1.∀EQmap : static_analisys p ? instr_m mT prog = return map1. |
---|
445 | ∀st1,st2 : vm_state p p'. |
---|
446 | ∀ter : terminated_trace (asm_operational_semantics p p' prog) st2. |
---|
447 | ∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. |
---|
448 | ∀k.pre_measurable_trace…t → |
---|
449 | block_cost p prog…instr_m (pc…st1) (S (|(instructions…prog)|)) = return k → |
---|
450 | ∀a1.rel_galois…good st1 a1 → |
---|
451 | let stop_state ≝ match R_post_step…ter with [None ⇒ st2 | Some x ⇒ \snd x ] in |
---|
452 | ∀costs.costs = dependent_map CostLabel ? (get_costlabels_of_trace…t) |
---|
453 | (λlbl,prf.(opt_safe…(get_map…map1 lbl) ?)) → |
---|
454 | rel_galois…good stop_state (act_abs…abs_t (big_op…costs) (act_abs…abs_t k a1)). |
---|
455 | \end{lstlisting} |
---|
456 | \end{wideslide} |
---|
457 | |
---|
458 | \begin{wideslide}{Conclusion} |
---|
459 | \begin{itemize} |
---|
460 | \item We present an improvement of the labelling approach for a precise resource analisys of the source code. |
---|
461 | \item We extend labelling approach to cope hidden assumptions on conditional instructions and function calls. |
---|
462 | \item We are able (almost always) to deal with non commutative costs. |
---|
463 | \item The usual assumption that compilation preserves the structure of basic blocks is still present. |
---|
464 | \end{itemize} |
---|
465 | Future works |
---|
466 | \begin{itemize} |
---|
467 | \item Abandoning SOS semantics. |
---|
468 | \item We would like to extend our framework to compilation process that does not preserve basic block structure as in [Tranquilli13QPLAS]. |
---|
469 | \end{itemize} |
---|
470 | \end{wideslide} |
---|
471 | \end{document} |
---|