Changeset 3305


Ignore:
Timestamp:
May 29, 2013, 6:25:11 PM (4 years ago)
Author:
tranquil
Message:

messo qualche figura, e molte notazioni

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r3222 r3305  
    44\usepackage{color}
    55\usepackage{listings}
    6 \usepackage{bcprules}
     6\usepackage{bcprules}%\bcprulessavespace
    77\usepackage{verbatim}
    88\usepackage{alltt}
     9\usepackage{subcaption}
     10\usepackage{listings}
     11\usepackage{amssymb}
     12% \usepackage{amsmath}
     13\usepackage{multicol}
     14
     15\providecommand{\eqref}[1]{(\ref{#1})}
    916
    1017% NB: might be worth removing this if changing class in favour of
     
    2936        showspaces=false,showstringspaces=false,
    3037        xleftmargin=1em}
     38
     39\usepackage{tikz}
     40\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes}
     41\makeatletter
     42\pgfutil@ifundefined{pgf@arrow@code@implies}{% supply for lack of double arrow special arrow tip if it is not there%
     43  \pgfarrowsdeclare{implies}{implies}%
     44  {%
     45  \pgfarrowsleftextend{2.2pt}%
     46  \pgfarrowsrightextend{2.2pt}%
     47  }%
     48  {%
     49    \pgfsetdash{}{0pt} % do not dash%
     50    \pgfsetlinewidth{.33pt}%
     51    \pgfsetroundjoin   % fix join%
     52    \pgfsetroundcap    % fix cap%
     53    \pgfpathmoveto{\pgfpoint{-1.5pt}{2.5pt}}%
     54    \pgfpathcurveto{\pgfpoint{-.75pt}{1.5pt}}{\pgfpoint{0.5pt}{.5pt}}{\pgfpoint{2pt}{0pt}}%
     55    \pgfpathcurveto{\pgfpoint{0.5pt}{-.5pt}}{\pgfpoint{-.75pt}{-1.5pt}}{\pgfpoint{-1.5pt}{-2.5pt}}%
     56    \pgfusepathqstroke%
     57  }%
     58}{}%
     59\makeatother
     60
     61\tikzset{state/.style={inner sep = 0, outer sep = 2pt, draw, fill},
     62         every node/.style={inner sep=2pt},
     63         every on chain/.style = {inner sep = 0, outer sep = 2pt},
     64         join all/.style = {every on chain/.append style={join}},
     65         on/.style={on chain={#1}, state},
     66         m/.style={execute at begin node=$, execute at end node=$},
     67         node distance=3mm,
     68         is other/.style={circle, minimum size = 3pt, state},
     69         other/.style={on, is other},
     70         is jump/.style={diamond, minimum size = 6pt, state},
     71         jump/.style={on, is jump},
     72         is call/.style={regular polygon, regular polygon sides=3, minimum size=5pt, state},
     73         call/.style={on=going below, is call, node distance=6mm, label=above left:$#1$},
     74         is ret/.style={regular polygon, regular polygon sides=3, minimum size=5pt, shape border rotate=180, state},
     75         ret/.style={on=going above, is ret, node distance=6mm},
     76         chain/.style={start chain=#1 going left},
     77         rev ar/.style={stealth-, thick},
     78         ar/.style={-stealth, thick},
     79         every join/.style={rev ar},
     80         labelled/.style={fill=white, label=above:$#1$},
     81         vcenter/.style={baseline={([yshift=-.5ex]current bounding box)}},
     82         every picture/.style={thick},
     83         double equal sign distance/.prefix style={double distance=1.5pt}, %% if already defined (newest version of pgf) it should be ignored%}
     84         implies/.style={double, -implies, thin, double equal sign distance, shorten <=5pt, shorten >=5pt},
     85         new/.style={densely dashed},
     86         rel/.style={font=\scriptsize, fill=white, inner sep=2pt},
     87         diag/.style={row sep={11mm,between origins},
     88                      column sep={11mm,between origins},
     89                      every node/.style={draw, is other}},
     90         small vgap/.style={row sep={7mm,between origins}},
     91}
     92
     93\def\L{\mathrel{\mathcal L}}
     94\def\S{\mathrel{\mathcal S}}
     95\def\R{\mathrel{\mathcal R}}
     96\def\C{\mathrel{\mathcal C}}
     97
     98\newsavebox{\execbox}
     99\savebox{\execbox}{\tikz[baseline=-.5ex]\draw [-stealth] (0,0) -- ++(1em, 0);}
     100\newcommand{\exec}{\ensuremath{\mathrel{\usebox{\execbox}}}}
     101\let\ar\rightsquigarrow
     102\renewcommand{\verb}{\lstinline[mathescape]}
     103
     104\let\class\triangleright
     105\let\andalso\quad
     106
     107\newcommand{\append}{\mathbin{@}}
    31108
    32109\begin{document}
     
    56133
    57134\section{Introduction}
    58 
    59135The \emph{labelling approach} has been introduced in~\cite{easylabelling} as
    60136a technique to \emph{lift} cost models for non-functional properties of programs
     
    338414In order to have a definition that works on multiple intermediate languages,
    339415we abstract the type of structure traces over an abstract data type of
    340 abstract statuses:
    341 \begin{alltt}
    342 record abstract_status := \{ S: Type[0];
    343  as_execute: S \(\to\) S \(\to\) Prop;     as_classify: S \(\to\) classification;
    344  as_costed: S \(\to\) Prop;      as_label: \(\forall\) s. as_costed S s \(\to\) label;
    345  as_call_ident: \(\forall\) s. as_classify S s = cl_call \(\to\) label;
    346  as_after_return:
    347   (\(\Sigma\)s:as_status. as_classify s = Some ? cl_call) \(\to\) as_status \(\to\) Prop \}
    348 \end{alltt}
    349 The predicate $\texttt{as\_execute}~s_1~s_2$ holds if $s_1$ evolves into
    350 $s_2$ in one step;\\ $\texttt{as\_classify}~s~c$ holds if the next instruction
    351 to be executed in $s$ is classified according to $c \in
    352 \{\texttt{cl\_return,cl\_jump,cl\_call,cl\_other}\}$ (we omit tail-calls for simplicity);
    353 the predicate $\texttt{as\_costed}~s$ holds if the next instruction to be
    354 executed in $s$ is a cost emission statement (also classified
    355 as \texttt{cl\_other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds
    356 if the next instruction to be executed in $s_2$ follows the function call
    357 to be executed in (the witness of the $\Sigma$-type) $s_1$. The two functions
    358 \texttt{as\_label} and \texttt{as\_cost\_ident} are used to extract the
    359 cost label/function call target from states whose next instruction is
    360 a cost emission/function call statement.
    361 
     416abstract statuses, which we aptly call $\texttt{abstract\_status}$. The fields
     417of this record are the following.
     418\begin{itemize}
     419 \item \verb+S : Type[0]+, the type of states.
     420 \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate stating
     421 an execution step. We write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$.
     422 \item \verb+as_classifier : S $\to$ classification+, a function tagging all
     423 states with a class in
     424 $\{\texttt{cl\_return,cl\_jump,cl\_call,cl\_other}\}$, depending on the instruction
     425 that is about to be executed (we omit tail-calls for simplicity). We will
     426 use $s \class c$ as a shorthand for both $\texttt{as\_classifier}~s=c$
     427 (if $c$ is a classification) and $\texttt{as\_classifier}~s\in c$
     428 (if $c$ is a set of classifications).
     429 \item \verb+as_label : S $\to$ option label+, telling whether the
     430 next instruction to be executed in $s$ is a cost emission statement,
     431 and if yes returning the associated cost label. Our shorthand for this function
     432 will be $\ell$, and we will also abuse the notation by using $\ell~s$ as a
     433 predicate stating that $s$ is labelled.
     434 \item \verb+as_call_ident : ($\Sigma$s:S. s $\class$ cl_call) $\to$ label+,
     435 telling the identifier of the function which is being called in a
     436 \verb+cl_call+ state. We will use the shorthand $s\uparrow f$ for
     437 $\verb+as_call_ident+~s = f$.
     438 \item \verb+as_after_return : ($\Sigma$s:S. s $\class$ cl_call) $\to$ S $\to$ Prop+,
     439 which holds on the \verb+cl_call+ state $s_1$ and a state $s_2$ when the
     440 instruction to be executed in $s_2$ follows the function call to be
     441 executed in (the witness of the $\Sigma$-type) $s_1$. We will use the notation
     442 $s_1\ar s_2$ for this relation.
     443\end{itemize}
     444
     445% \begin{alltt}
     446% record abstract_status := \{ S: Type[0];
     447%  as_execute: S \(\to\) S \(\to\) Prop;   as_classifier: S \(\to\) classification;
     448%  as_label: S \(\to\) option label;    as_called: (\(\Sigma\)s:S. c s = cl_call) \(\to\) label;
     449%  as_after_return: (\(\Sigma\)s:S. c s = cl_call) \(\to\) S \(\to\) Prop \}
     450% \end{alltt}
    362451
    363452The inductive type for structured traces is actually made by three multiple
    364453inductive types with the following semantics:
    365454\begin{enumerate}
    366  \item $(\texttt{trace\_label\_return}~s_1~s_2)$ is a trace that begins in
     455 \item $(\texttt{trace\_label\_return}~s_1~s_2)$ (shorthand $\verb+TLR+~s_1~s_2$)
     456   is a trace that begins in
    367457   the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
    368458   such that the instruction to be executed in $s_1$ is a label emission
     
    374464   one or more basic blocks, all starting with a label emission
    375465   (e.g. in case of loops).
    376  \item $(\texttt{trace\_any\_label}~b~s_1~s_2)$ is a trace that begins in
     466 \item $(\texttt{trace\_any\_label}~b~s_1~s_2)$ (shorthand $\verb+TAL+~b~s_1~s_2$)
     467   is a trace that begins in
    377468   the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
    378469   such that the instruction to be executed in $s_2$/in the state before
     
    381472   any label emission statement. It captures the notion of a suffix of a
    382473   basic block.
    383  \item $(\texttt{trace\_label\_label}~b~s_1~s_2)$ is the special case of
    384    $(\texttt{trace\_any\_label}~b~s_1~s_2)$ such that the instruction to be
     474 \item $(\texttt{trace\_label\_label}~b~s_1~s_2)$ (shorthand $\verb+TLL+~b~s_1~s_2$ is the special case of
     475   $\verb+TAL+~b~s_1~s_2)$ such that the instruction to be
    385476   executed in $s_1$ is a label emission statement. It captures the notion of
    386477   a basic block.
    387478\end{enumerate}
    388479
    389 \infrule[\texttt{tlr\_base}]
    390  {\texttt{trace\_label\_label}~true~s_1~s_2}
    391  {\texttt{trace\_label\_return}~s_1~s_2}
    392 
    393 \infrule[\texttt{tlr\_step}]
    394  {\texttt{trace\_label\_label}~false~s_1~s_2 \andalso
    395   \texttt{trace\_label\_return}~s_2~s_3
     480\begin{multicols}{3}
     481\infrule[\verb+tlr_base+]
     482 {\texttt{TLL}~true~s_1~s_2}
     483 {\texttt{TLR}~s_1~s_2}
     484
     485\infrule[\verb+tlr_step+]
     486 {\texttt{TLL}~false~s_1~s_2 \andalso
     487  \texttt{TLR}~s_2~s_3
    396488 }
    397  {\texttt{trace\_label\_return}~s_1~s_3}
    398 
    399 \infrule[\texttt{tll\_base}]
    400  {\texttt{trace\_any\_label}~b~s_1~s_2 \andalso
    401   \texttt{as\_costed}~s_1
     489 {\texttt{TLR}~s_1~s_3}
     490
     491\infrule[\verb+tll_base+]
     492 {\texttt{TAL}~b~s_1~s_2 \andalso
     493  \ell~s_1
    402494 }
    403  {\texttt{trace\_label\_label}~b~s_1~s_2}
    404 
    405 \infrule[\texttt{tal\_base\_not\_return}]
    406  {\texttt{as\_execute}~s_1~s_2 \andalso
    407   \texttt{as\_classify}~s_1 \in \{\texttt{cl\_jump,cl\_other}\} \andalso
    408   \texttt{as\_costed}~s_2
     495 {\texttt{TLL}~b~s_1~s_2}
     496\end{multicols}
     497
     498\infrule[\verb+tal_base_not_return+]
     499 {s_1\exec s_2 \andalso
     500  s_1\class\{\verb+cl_jump+, \verb+cl_other+\}\andalso
     501  \ell~s_2
    409502 }
    410  {\texttt{trace\_any\_label}~false~s_1~s_2}
    411 
    412 \infrule[\texttt{tal\_base\_return}]
    413  {\texttt{as\_execute}~s_1~s_2 \andalso
    414   \texttt{as\_classify}~s_1 = \texttt{cl\_return} \\
     503 {\texttt{TAL}~false~s_1~s_2}
     504
     505\infrule[\verb+tal_base_return+]
     506 {s_1\exec s_2 \andalso
     507  s_1 \class \texttt{cl\_return}
    415508 }
    416  {\texttt{trace\_any\_label}~true~s_1~s_2}
    417 
    418 \infrule[\texttt{tal\_base\_call}]
    419  {\texttt{as\_execute}~s_1~s_2 \andalso
    420   \texttt{as\_classify}~s_1 = \texttt{cl\_call} \\
    421   \texttt{as\_after\_return}~s_1~s_3 \andalso
    422   \texttt{trace\_label\_return}~s_2~s_3 \andalso
    423   \texttt{as\_costed}~s_3
     509 {\texttt{TAL}~true~s_1~s_2}
     510
     511\infrule[\verb+tal_base_call+]
     512 {s_1\exec s_2 \andalso
     513  s_1 \class \texttt{cl\_call} \andalso
     514  s_1\ar s_3 \andalso
     515  \texttt{TLR}~s_2~s_3 \andalso
     516  \ell~s_3
    424517 }
    425  {\texttt{trace\_any\_label}~false~s_1~s_3}
    426 
    427 \infrule[\texttt{tal\_step\_call}]
    428  {\texttt{as\_execute}~s_1~s_2 \andalso
    429   \texttt{as\_classify}~s_1 = \texttt{cl\_call} \\
    430   \texttt{as\_after\_return}~s_1~s_3 \andalso
    431   \texttt{trace\_label\_return}~s_2~s_3 \\
    432   \lnot \texttt{as\_costed}~s_3 \andalso
    433   \texttt{trace\_any\_label}~b~s_3~s_4
     518 {\texttt{TAL}~false~s_1~s_3}
     519
     520\infrule[\verb+tal_step_call+]
     521 {s_1\exec s_2 \andalso
     522  s_1 \class \texttt{cl\_call} \andalso
     523  s_1\ar s_3 \andalso
     524  \texttt{TLR}~s_2~s_3 \andalso
     525  \texttt{TAL}~b~s_3~s_4
    434526 }
    435  {\texttt{trace\_any\_label}~b~s_1~s_4}
    436 
    437 \infrule[\texttt{tal\_step\_default}]
    438  {\texttt{as\_execute}~s_1~s_2 \andalso
    439   \lnot \texttt{as\_costed}~s_2 \\
    440   \texttt{trace\_any\_label}~b~s_2~s_3
    441   \texttt{as\_classify}~s_1 = \texttt{cl\_other}
     527 {\texttt{TAL}~b~s_1~s_4}
     528
     529\infrule[\verb+tal_step_default+]
     530 {s_1\exec s_2 \andalso
     531  \lnot \ell~s_2 \andalso
     532  \texttt{TAL}~b~s_2~s_3\andalso
     533  s_1 \class \texttt{cl\_other}
    442534 }
    443  {\texttt{trace\_any\_label}~b~s_1~s_3}
    444 
    445 
     535 {\texttt{TAL}~b~s_1~s_3}
    446536\begin{comment}
    447537\begin{verbatim}
     
    549639\end{enumerate}
    550640
    551 The three mutual structural recursive functions \texttt{flatten\_trace\_label\_return, flatten\_trace\_label\_label} and \texttt{flatten\_trance\_any\_label}
    552 allow to extract from a structured trace the list of states whose next
    553 instruction is a cost emission statement. We only show here the type of one
    554 of them:
    555 \begin{alltt}
    556 flatten_trace_label_return:
    557  \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\).
    558   trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S)
    559 \end{alltt}
    560 
    561 \paragraph{Cost prediction on structured traces}
     641There are three mutual structural recursive functions, one for each of
     642\verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation
     643$|\,.\,|$: the \emph{flattening} of the traces. These functions
     644allow to extract from a structured trace the list of emitted cost labels.
     645%  We only show here the type of one
     646% of them:
     647% \begin{alltt}
     648% flatten_trace_label_return:
     649%  \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\).
     650%   trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S)
     651% \end{alltt}
     652
     653\paragraph{Cost prediction on structured traces.}
    562654
    563655The first main theorem of CerCo about traces
     
    568660Simplifying a bit, it states that
    569661\begin{equation}\label{th1}
    570 \begin{array}{l}\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~
    571   \texttt{clock}~s_2 = \texttt{clock}~s_1 + \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau)}\;k(\mathcal{L}(s))
     662\begin{array}{l}\forall s_1,s_2. \forall \tau: \texttt{TLR}~s_1~s_2.~
     663  \texttt{clock}~s_2 = \texttt{clock}~s_1 +
     664  \Sigma_{\alpha \in |\tau|}\;k(\alpha)
    572665\end{array}
    573666\end{equation}
    574 where $\mathcal{L}$ maps a labelled state to its emitted label, and the
    575 cost model $k$ is statically computed from the object code
    576 by associating to each label \texttt{L} the sum of the cost of the instructions
    577 in the basic block that starts at \texttt{L} and ends before the next labelled
     667where the cost model $k$ is statically computed from the object code
     668by associating to each label $\alpha$ the sum of the cost of the instructions
     669in the basic block that starts at $\alpha$ and ends before the next labelled
    578670instruction. The theorem is proved by structural induction over the structured
    579671trace, and is based on the invariant that
     
    582674the structured trace starts with $s_1$, then eventually it will contain also
    583675$s_2$. When $s_1$ is not a function call, the result holds trivially because
    584 of the $(\texttt{as\_execute}~s_1~s_2)$ condition obtained by inversion on
     676of the $s_1\exec s_2$ condition obtained by inversion on
    585677the trace. The only non
    586678trivial case is the one of function calls: the cost model computation function
     
    590682this state.
    591683
    592 \paragraph{Structured traces similarity and cost prediction invariance}
     684\paragraph{Structured traces similarity and cost prediction invariance.}
    593685
    594686A compiler pass maps source to object code and initial states to initial
     
    603695interested only in those compiler passes that maps a trace $\tau_1$ to a trace
    604696$\tau_2$ such that
    605 \begin{equation}\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2\label{condition1}\label{th2}\end{equation}
    606 The reason is that the combination of~\ref{th1} with~\ref{th2} yields the
     697\begin{equation}|\tau_1| = |\tau_2|.\label{th2}\end{equation}
     698The reason is that the combination of~\eqref{th1} with~\eqref{th2} yields the
    607699corollary
    608 \begin{equation}\begin{array}{l}\label{th3}
    609 \forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~~~~\;
    610   clock~s_2 - clock~s_1\\~ = \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau_1)}\;k(\mathcal{L}(s))\\~ = \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau_2)}\;k(\mathcal{L}(s))
    611 \end{array}\end{equation}
     700\begin{equation}\label{th3}
     701\forall s_1,s_2. \forall \tau: \texttt{TLR}~s_1~s_2.~
     702  \texttt{clock}~s_2 - \texttt{clock}~s_1 =
     703  \Sigma_{\alpha \in |\tau_1|}\;k(\alpha) =
     704  \Sigma_{\alpha \in |\tau_2|}\;k(\alpha).
     705\end{equation}
    612706This corollary states that the actual execution time of the program can be computed equally well on the source or target language. Thus it becomes possible to
    613707transfer the cost model from the target to the source code and reason on the
    614708source code only.
    615709
    616 We are therefore interested in conditions stronger than~\ref{condition1}.
     710We are therefore interested in conditions stronger than~\eqref{th2}.
    617711Therefore we introduce here a similarity relation between traces with
    618712the same structure. Theorem~\texttt{tlr\_rel\_to\_traces\_same\_flatten}
    619 in the Matita formalisation shows that~\ref{th2} holds for every pair
     713in the Matita formalisation shows that~\eqref{th2} holds for every pair
    620714$(\tau_1,\tau_2)$ of similar traces.
    621715
    622716Intuitively, two traces are similar when one can be obtained from
    623717the other by erasing or inserting silent steps, i.e. states that are
    624 not \texttt{as\_costed} and that are classified as \texttt{other}.
     718not \texttt{as\_costed} and that are classified as \texttt{cl\_other}.
    625719Silent steps do not alter the structure of the traces.
    626720In particular,
     
    635729the definition into inference rules for the sake of readability. We also
    636730omit from trace constructors all arguments, but those that are traces or that
    637 are used in the premises of the rules.
    638 
     731are used in the premises of the rules. By abuse of notation we denote all three
     732relations by infixing $\approx$
     733
     734\begin{multicols}{2}
    639735\infrule
    640  {\texttt{tll\_rel}~tll_1~tll_2
     736 {tll_1\approx tll_2
    641737 }
    642  {\texttt{tlr\_rel}~(\texttt{tlr\_base}~tll_1)~(\texttt{tlr\_base}~tll_2)}
     738 {\texttt{tlr\_base}~tll_1 \approx \texttt{tlr\_base}~tll_2}
    643739
    644740\infrule
    645  {\texttt{tll\_rel}~tll_1~tll_2 \andalso
    646   \texttt{tlr\_rel}~tlr_1~tlr_2
     741 {tll_1 \approx tll_2 \andalso
     742  tlr_1 \approx tlr_2
    647743 }
    648  {\texttt{tlr\_rel}~(\texttt{tlr\_step}~tll_1~tlr_1)~(\texttt{tlr\_step}~tll_2~tlr_2)}
     744 {\texttt{tlr\_step}~tll_1~tlr_1 \approx \texttt{tlr\_step}~tll_2~tlr_2}
     745\end{multicols}
    649746
    650747\infrule
    651  {\texttt{as\_label}~H_1 = \texttt{as\_label}~H_2 \andalso
    652   \texttt{tal\_rel}~tal_1~tal_2
     748 {\ell~s_1 = \ell~s_2 \andalso
     749  tal_1\approx tal_2
    653750 }
    654  {\texttt{tll\_rel}~(\texttt{tll\_base}~tal_1~H_1)~(\texttt{tll\_base}~tal_2~H_2)}
     751 {\texttt{tll\_base}~s_1~tal_1 \approx \texttt{tll\_base}~s_2~tal_2}
    655752
    656753\infrule
    657754 {}
    658  {\texttt{tal\_rel}~\texttt{tal\_base\_not\_return}~(taa @ \texttt{tal\_base\_not\_return}}
     755 {\texttt{tal\_base\_not\_return}\approx taa \append \texttt{tal\_base\_not\_return}}
    659756
    660757\infrule
    661758 {}
    662  {\texttt{tal\_rel}~\texttt{tal\_base\_return}~(taa @ \texttt{tal\_base\_return}}
     759 {\texttt{tal\_base\_return}\approx taa \append \texttt{tal\_base\_return}}
    663760
    664761\infrule
    665  {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
    666   \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2
     762 {tlr_1\approx tlr_2 \andalso
     763  s_1 \uparrow f \andalso s_2\uparrow f
    667764 }
    668  {\texttt{tal\_rel}~(\texttt{tal\_base\_call}~H_1~tlr_1)~(taa @ \texttt{tal\_base\_call}~H_2~tlr_2)}
     765 {\texttt{tal\_base\_call}~s_1~tlr_1\approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2}
    669766
    670767\infrule
    671  {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
    672   \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2 \andalso
     768 {tlr_1\approx tlr_2 \andalso
     769  s_1 \uparrow f \andalso s_2\uparrow f \andalso
    673770  \texttt{tal\_collapsable}~tal_2
    674771 }
    675  {\texttt{tal\_rel}~(\texttt{tal\_base\_call}~tlr_1)~(taa @ \texttt{tal\_step\_call}~tlr_2~tal_2)}
     772 {\texttt{tal\_base\_call}~s_1~tlr_1 \approx taa \append \texttt{tal\_step\_call}~s_2~tlr_2~tal_2)}
    676773
    677774\infrule
    678  {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
    679   \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2 \andalso
     775 {tlr_1\approx tlr_2 \andalso
     776  s_1 \uparrow f \andalso s_2\uparrow f \andalso
    680777  \texttt{tal\_collapsable}~tal_1
    681778 }
    682  {\texttt{tal\_rel}~(\texttt{tal\_step\_call}~tlr_1~tal_1)~(taa @ \texttt{tal\_base\_call}~tlr_2)}
     779 {\texttt{tal\_step\_call}~s_1~tlr_1~tal_1 \approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2)}
    683780
    684781\infrule
    685  {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
    686   \texttt{tal\_rel}~tal_1~tal_2 \andalso
    687   \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2
     782 {tlr_1 \approx tlr_2 \andalso
     783  s_1 \uparrow f \andalso s_2\uparrow f
     784  tal_1 \approx tal_2 \andalso
    688785 }
    689  {\texttt{tal\_rel}~(\texttt{tal\_step\_call}~tlr_1~tal_1)~(taa @ \texttt{tal\_step\_call}~tlr_2~tal_2)}
     786 {\texttt{tal\_step\_call}~s_1~tlr_1~tal_1 \approx taa \append \texttt{tal\_step\_call}~s_2~tlr_2~tal_2}
    690787
    691788\infrule
    692  {\texttt{tal\_rel}~tal_1~tal_2
     789 {tal_1\approx tal_2
    693790 }
    694  {\texttt{tal\_rel}~(\texttt{tal\_step\_default}~tal_1)~tal_2}
     791 {\texttt{tal\_step\_default}~tal_1 \approx tal_2}
    695792\begin{comment}
    696793\begin{verbatim}
     
    768865
    769866In the preceding rules, a $taa$ is an inhabitant of the
    770 $\texttt{trace\_any\_any}~s_1~s_2$ inductive data type whose definition
     867$\texttt{trace\_any\_any}~s_1~s_2$ (shorthand $\texttt{TAA}~s_1~s_2$),
     868an inductive data type whose definition
    771869is not in the paper for lack of space. It is the type of valid
    772 prefixes (even empty ones) of \texttt{trace\_any\_label}s that do not contain
     870prefixes (even empty ones) of \texttt{TAL}'s that do not contain
    773871any function call. Therefore it
    774 is possible to concatenate (using ``$@$'') a \texttt{trace\_any\_any} to the
    775 left of a \texttt{trace\_any\_label}. A \texttt{trace\_any\_any} captures
     872is possible to concatenate (using ``$\append$'') a \texttt{TAA} to the
     873left of a \texttt{TAL}. A \texttt{TAA} captures
    776874a sequence of silent moves.
    777875
    778 The \texttt{tal\_collapsable} unary predicate over \texttt{trace\_any\_label}s
     876The \texttt{tal\_collapsable} unary predicate over \texttt{TAL}'s
    779877holds when the argument does not contain any function call and it ends
    780878with a label (not a return). The intuition is that after a function call we
     
    865963compiler pass.
    866964
    867 \paragraph{Relation sets}
     965\paragraph{Relation sets.}
    868966
    869967We introduce now the four relations $\mathcal{S,C,L,R}$ between abstract
     
    9061004\end{alltt}
    9071005
    908 \paragraph{1-to-0-or-many forward simulation conditions}
     1006\begin{figure}
     1007\centering
     1008\begin{tabular}{@{}c@{}c@{}}
     1009\begin{subfigure}{.475\linewidth}
     1010\centering
     1011\begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1012                            every label/.style=overlay, node distance=10mm]
     1013    \matrix [diag] (m) {%
     1014         \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
     1015         \node (s2) {}; & \node (t2) {}; \\
     1016    };
     1017    \node [above=0 of t1, overlay] {$\alpha$};
     1018    {[-stealth]
     1019    \draw (s1) -- (t1);
     1020    \draw [new] (s2) -- node [above] {$*$} (t2);
     1021    }
     1022    \draw (s1) to node [rel] {$\S$} (s2);
     1023    \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
     1024\end{tikzpicture}
     1025\caption{The \texttt{cl\_jump} case.}
     1026\label{subfig:cl_jump}
     1027\end{subfigure}
     1028&
     1029\begin{subfigure}{.475\linewidth}
     1030\centering
     1031\begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1032                            every label/.style=overlay, node distance=10mm]
     1033    \matrix [diag] (m) {%
     1034         \node (s1) {}; & \node (t1) {};\\
     1035         \node (s2) {}; & \node (t2) {}; \\
     1036    };
     1037    {[-stealth]
     1038    \draw (s1) -- (t1);
     1039    \draw [new] (s2) -- node [above] {$*$} (t2);
     1040    }
     1041    \draw (s1) to node [rel] {$\S$} (s2);
     1042    \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
     1043\end{tikzpicture}
     1044\caption{The \texttt{cl\_oher} case.}
     1045\label{subfig:cl_other}
     1046\end{subfigure}
     1047\\
     1048\begin{subfigure}{.475\linewidth}
     1049\centering
     1050\begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1051                            every label/.style=overlay, node distance=10mm]
     1052    \matrix [diag, small vgap] (m) {%
     1053        \node (t1) {}; \\
     1054         \node (s1) [is call] {}; \\
     1055         & \node (l) {}; & \node (t2) {};\\
     1056         \node (s2) {}; & \node (c) [is call] {};\\   
     1057    };
     1058    {[-stealth]
     1059    \draw (s1) -- node [left] {$f$} (t1);
     1060    \draw [new] (s2) -- node [above] {$*$} (c);
     1061    \draw [new] (c) -- node [right] {$f$} (l);
     1062    \draw [new] (l) -- node [above] {$*$} (t2);
     1063    }
     1064    \draw (s1) to node [rel] {$\S$} (s2);
     1065    \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2);
     1066    \draw [new] (t1) to [bend left] node [rel] {$\L$} (l);
     1067    \draw [new] (t1) to node [rel] {$\C$} (c);
     1068    \end{tikzpicture}
     1069\caption{The \texttt{cl\_call} case.}
     1070\label{subfig:cl_call}
     1071\end{subfigure}
     1072&
     1073\begin{subfigure}{.475\linewidth}
     1074\centering
     1075\begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1076                            every label/.style=overlay, node distance=10mm]
     1077    \matrix [diag, small vgap] (m) {%
     1078        \node (s1) [is ret] {}; \\
     1079        \node (t1) {}; \\
     1080        \node (s2) {}; & \node (c) [is ret] {};\\
     1081        & \node (r) {}; & \node (t2) {}; \\   
     1082    };
     1083    {[-stealth]
     1084    \draw (s1) -- (t1);
     1085    \draw [new] (s2) -- node [above] {$*$} (c);
     1086    \draw [new] (c) -- (r);
     1087    \draw [new] (r) -- node [above] {$*$} (t2);
     1088    }
     1089    \draw (s1) to [bend right=45] node [rel] {$\S$} (s2);
     1090    \draw [new, overlay] (t1) to [bend left=90, looseness=1] node [rel] {$\S,\L$} (t2);
     1091    \draw [new, overlay] (t1) to [bend left=90, looseness=1.2] node [rel] {$\R$} (r);
     1092\end{tikzpicture}
     1093\caption{The \texttt{cl\_return} case.}
     1094\label{subfig:cl_return}
     1095\end{subfigure}
     1096\end{tabular}
     1097\caption{The hypotheses for the preservation of structured traces, simplified.
     1098         Dashed lines
     1099         and arrows indicates how the diagrams must be closed when solid relations
     1100         are present.}
     1101\label{fig:forwardsim}
     1102\end{figure}
     1103
     1104\paragraph{1-to-0-or-many forward simulation conditions.}
    9091105\begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}]
    910  For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and
    911  $\texttt{as\_execute}~s_1~s_1'$, and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ or $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ and
    912 $\texttt{as\_costed}~s_1'$, there exists an $s_2'$ and a $\texttt{trace\_any\_any\_free}~s_2~s_2'$ called $taaf$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
     1106 For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
     1107 $s_1\exec s_1'$, and either $s_1 \class \texttt{cl\_other}$ or
     1108 both $s_1\class\texttt{cl\_other}\}$ and $\ell~s_1'$,
     1109 there exists an $s_2'$ and a $\texttt{trace\_any\_any\_free}~s_2~s_2'$ called $taaf$
     1110 such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
    9131111$taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}.
    9141112\end{condition}
    9151113
    916 In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ is an
     1114In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ (which from now on
     1115will be shorthanded as \verb+TAAF+) is an
    9171116inductive type of structured traces that do not contain function calls or
    918 cost emission statements. Differently from a \texttt{trace\_any\_any}, the
     1117cost emission statements. Differently from a \verb+TAA+, the
    9191118instruction to be executed in the lookahead state $s_2$ may be a cost emission
    9201119statement.
     
    9231122preserves the relation between the data and if the two final statuses are
    9241123labelled in the same way. Moreover, we must take special care of the empty case
    925 to avoid collapsing two consecutive states that emit the same label to just
    926 one state, missing one of the two emissions.
     1124to avoid collapsing two consecutive states that emit a label, missing one of the two emissions.
    9271125
    9281126\begin{condition}[Case \texttt{cl\_call}]
    929  For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$ and
    930  $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a
    931 $\texttt{trace\_any\_any}~s_2~s_b$, and a
    932 $\texttt{trace\_any\_any\_free}~s_a~s_2'$ such that:
    933 $s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of
    934 the two call states are the same, $s_1 \mathcal{C} s_b$,
    935 $\texttt{as\_execute}~s_b~s_a$ holds, $s_1' \mathcal{L} s_b$ and
    936 $s_1' \mathcal{S} s_2'$.
     1127 For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and
     1128 $s_1\exec s_1'$ and $s_1 \class \texttt{cl\_call}$, there exists $s_a, s_b, s_2'$, a
     1129$\verb+TAA+~s_2~s_a$, and a
     1130$\verb+TAAF+~s_b~s_2'$ such that:
     1131$s_a\class\texttt{cl\_call}$, the \texttt{as\_call\_ident}'s of
     1132the two call states are the same, $s_1 \mathcal{C} s_a$,
     1133$s_a\exec s_b$, $s_1' \L s_b$ and
     1134$s_1' \S s_2'$.
    9371135\end{condition}
    9381136
     
    9451143
    9461144\begin{condition}[Case \texttt{cl\_return}]
    947  For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$,
    948  $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a
    949 $\texttt{trace\_any\_any}~s_2~s_b$, a
    950 $\texttt{trace\_any\_any\_free}~s_a~s_2'$ called $taaf$ such that:
     1145 For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$,
     1146 $s_1\exec s_1'$ and $s_1 \class \texttt{cl\_return}$, there exists $s_a, s_b, s_2'$, a
     1147$\verb+TAA+~s_2~s_a$, a
     1148$\verb+TAAF+~s_b~s_2'$ called $taaf$ such that:
    9511149$s_a$ is classified as a \texttt{cl\_return},
    952 $s_1 \mathcal{C} s_b$, the predicate
    953 $\texttt{as\_execute}~s_b~s_a$ holds,
    954 $s_1' \mathcal{R} s_a$ and
    955 $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
    956 $taaf$ is non empty, or $s_a$ is not \texttt{as\_costed}.
     1150$s_a\exec s_b$,
     1151$s_1' \R s_b$ and
     1152$s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
     1153$taaf$ is non empty, or $\lnot \ell~s_a$.
    9571154\end{condition}
    9581155
     
    10671264\begin{theorem}[\texttt{status\_simulation\_produce\_tlr}]
    10681265For every $s_1,s_1',s_{2_b},s_2$ s.t.
    1069 there is a $\texttt{trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and a
    1070 $\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and
    1071 $s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t.
    1072 there is a $\texttt{trace\_label\_return}~s_{2_b}~s_{2_m}$ called $tlr_2$ and
    1073 there is a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taaf$
    1074 s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$,
    1075 and $\texttt{tlr\_rel}~tlr_1~tlr_2$
    1076 and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
    1077 $s_1' \mathcal{R} s_{2_m}$.
     1266there is a $\texttt{TLR}~s_1~s_1'$ called $tlr_1$ and a
     1267$\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
     1268$s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
     1269there is a $\texttt{TLR}~s_{2_b}~s_{2_m}$ called $tlr_2$ and
     1270there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$
     1271s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$,
     1272and $tlr_1\approx tlr_2$
     1273and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1274$s_1' \R s_{2_m}$.
    10781275\end{theorem}
    10791276
    10801277The theorem states that a \texttt{trace\_label\_return} in the source code
    10811278together with a precomputed preamble of silent states
    1082 (the \texttt{trace\_any\_any}) in the target code induces a
    1083 similar \texttt{trace\_label\_return} trace in the target code which can be
     1279(the \verb+TAA+) in the target code induces a
     1280similar \texttt{trace\_label\_return} in the target code which can be
    10841281followed by a sequence of silent states. Note that the statement does not
    1085 require the produced \texttt{trace\_label\_return} trace to start with the
     1282require the produced \texttt{trace\_label\_return} to start with the
    10861283precomputed preamble, even if this is likely to be the case in concrete
    10871284implementations. The preamble in input is necessary for compositionality, e.g.
     
    10921289\begin{theorem}[\texttt{status\_simulation\_produce\_tll}]
    10931290For every $s_1,s_1',s_{2_b},s_2$ s.t.
    1094 there is a $\texttt{trace\_label\_label}~b~s_1~s_1'$ called $tll_1$ and a
    1095 $\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and
    1096 $s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t.
     1291there is a $\texttt{TLL}~b~s_1~s_1'$ called $tll_1$ and a
     1292$\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
     1293$s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
    10971294\begin{itemize}
    10981295 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
    1099        and a trace $\texttt{trace\_label\_label}~b~s_{2_b}~s_{2_m}$ called $tll_2$
    1100        and a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t.
    1101        $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
    1102        $s_1' \mathcal{R} s_{2_m}$ and
    1103        $\texttt{tll\_rel}~tll_1~tll_2$ and
    1104        if $taa_2$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$
     1296       and a trace $\texttt{TLL}~b~s_{2_b}~s_{2_m}$ called $tll_2$
     1297       and a $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
     1298       $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1299       $s_1' \R s_{2_m}$ and
     1300       $tll_1\approx tll_2$ and
     1301       if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
    11051302 \item else there exists $s_2'$ and a
    1106        $\texttt{trace\_label\_label}~b~s_{2_b}~s_2'$ called $tll_2$ such that
    1107        $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
    1108        $\texttt{tll\_rel}~tll_1~tll_2$.
     1303       $\texttt{TLL}~b~s_{2_b}~s_2'$ called $tll_2$ such that
     1304       $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1305       $tll_1\approx tll_2$.
    11091306\end{itemize}
    11101307\end{theorem}
     
    11181315\begin{theorem}[\texttt{status\_simulation\_produce\_tal}]
    11191316For every $s_1,s_1',s_2$ s.t.
    1120 there is a $\texttt{trace\_any\_label}~b~s_1~s_1'$ called $tal_1$ and
     1317there is a $\texttt{TAL}~b~s_1~s_1'$ called $tal_1$ and
    11211318$s_1 \mathcal{S} s_2$
    11221319\begin{itemize}
    11231320 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
    1124    and a trace $\texttt{trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a
    1125    $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t.
    1126    $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
    1127    $s_1' \mathcal{R} s_{2_m}$ and
    1128    $\texttt{tal\_rel}~tal_1~tal_2$ and
    1129    if $taa_2$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$
     1321   and a trace $\texttt{TAL}~b~s_2~s_{2_m}$ called $tal_2$ and a
     1322   $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
     1323   $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1324   $s_1' \R s_{2_m}$ and
     1325   $tal_1 \approx tal_2$ and
     1326   if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
    11301327 \item else there exists $s_2'$ and a
    1131    $\texttt{trace\_any\_label}~b~s_2~s_2'$ called $tal_2$ such that
    1132    either $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
    1133        $\texttt{tal\_rel}~tal_1~tal_2$
    1134    or $s_1' (\mathcal{S} \cap \mathcal{L}) s_2$ and
    1135    $\texttt{tal\_collapsable}~tal_1$ and $\lnot (\texttt{as\_costed}~s_1)$
     1328   $\texttt{TAL}~b~s_2~s_2'$ called $tal_2$ such that
     1329   either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1330       $tal_1\approx tal_2$
     1331   or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and
     1332   $\texttt{tal\_collapsable}~tal_1$ and $\lnot \ell~s_1$.
    11361333\end{itemize}
    11371334\end{theorem}
     
    12291426the CerCo compiler exploiting the main theorem of this paper.
    12301427
    1231 \paragraph{Related works}
     1428\paragraph{Related works.}
    12321429CerCo is the first project that explicitly tries to induce a
    12331430precise cost model on the source code in order to establish non-functional
Note: See TracChangeset for help on using the changeset viewer.