source: LTS/DICE2014/slides.tex @ 3467

Last change on this file since 3467 was 3467, checked in by piccolo, 6 years ago

slides

File size: 14.9 KB
Line 
1%%% \listfiles %%%%%%%%%%%%%%%%%% POWERDOT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2\documentclass[
3%% mode=present,
4%% mode=print,
5% mode=handout,
6% nopagebreaks,
7%paper=a4paper,
8paper=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]
114How 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)}
119The user writes the program
120\begin{lstlisting}
121I1;
122for(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}
129The program will be processed by a special pre-compiler which inserts some label emission statements
130\begin{lstlisting}
131EMIT L1;
132I1;
133for(int i=0;i<2;i++){ 
134  EMIT L2;
135  I2;
136}
137EMIT 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}
147EMIT L1;
148I1;
149for(int i=0;i<2;i++){ 
150  EMIT L2;
151  I2;
152}
153EMIT L3;
154\end{lstlisting}
155&$\qquad$&
156\begin{lstlisting}
157    EMIT L1;
158    I3
159l1: COND l1
160    EMIT L2
161    I4
162    GOTO l1
163l2: EMIT L3
164\end{lstlisting}
165\end{tabular}
166\end{center}
167\onslide*{2}{
168\begin{center}
169\begin{tabular}{|l|l|}
170\hline
171Label & Cost \\
172\hline
173L1 & $cost(I3) + cost(COND \ l1) = k_1$ \\
174L2 & $cost(I4) + cost(GOTO \ l1) = k_2$ \\
175L3 & $k_3$\\
176\hline
177\end{tabular}
178\end{center}
179}
180\end{wideslide}
181\begin{wideslide}[method=direct]{Labelling approach}
182The complier gives an instrumented version of the source code
183\begin{center}
184\begin{tabular}{l l l}
185\begin{lstlisting}
186cost += k_1
187instr 1;
188for(int i=0;i<2;i++){ 
189  cost += k_2
190  instr 2;
191}
192cost += k_3
193\end{lstlisting}
194&$\qquad$&
195\begin{lstlisting}
196    EMIT L1;
197    instr 3
198l1: COND l1
199    EMIT L2
200    instr 4
201    GOTO l1
202l2: 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]
213Precise 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}
221This 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}
250if(E){
251  EMIT L;
252  I;
253}
254\end{lstlisting}
255& $\qquad\qquad$ &
256\begin{lstlisting}
257    SJNEQ l1
258    JUMP l3
259l1: JUMP l2
260...
261l2: EMIT L
262    I;
263\end{lstlisting}
264& $\qquad\qquad$ &
265\begin{lstlisting}
266    SJNEQ l1
267    JUMP l3
268l1: EMIT L
269    JUMP l2
270...
271l2: 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]
282record 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}
299void main(){
300  EMIT L1;
301  I1;
302  (*f)();
303  I2;
304}
305
306void g(){
307  EMIT L2;
308  I3;
309}
310\end{lstlisting}
311& $\qquad\qquad$ &
312\begin{lstlisting}
313main :
314  EMIT L1
315  I4
316  CALL
317  I5
318  RETURN
319
320g :
321  EMIT L2
322  I6;
323  RETURN
324\end{lstlisting}
325\end{tabular}
326\end{center}
327What 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}
337The 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]
366inductive 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]
389theorem simulates_pre_mesurable:
390∀S : abstract_status.∀rel : relations S.∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
391simulation_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
407is lost in details.
408\item It does not solve the problem with stateful hardware, since the cost function is
409still requirred to be commutative.
410\end{itemize}
411\psshadowbox{
412\begin{minipage}{12cm}
413We 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}
426We 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]
428lemma 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'.
431state_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]
441lemma 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 →
449block_cost p prog…instr_m (pc…st1) (S (|(instructions…prog)|)) = return k →
450∀a1.rel_galois…good st1 a1 →
451let 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) ?)) →
454rel_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}
465Future 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}
Note: See TracBrowser for help on using the repository browser.