Changeset 3359


Ignore:
Timestamp:
Jun 14, 2013, 5:48:01 PM (4 years ago)
Author:
tranquil
Message:

recuperato un po' della formalizzazione, ancora in fondo.

File:
1 edited

Legend:

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

    r3358 r3359  
    8383         ar/.style={-stealth, thick},
    8484         every join/.style={rev ar},
    85          labelled/.style={fill=white, label=above:$#1$},
    8685         vcenter/.style={baseline={([yshift=-.5ex]current bounding box)}},
    8786         every picture/.style={thick},
     
    8988         implies/.style={double, -implies, thin, double equal sign distance, shorten <=5pt, shorten >=5pt},
    9089         new/.style={densely dashed},
     90         newn/.style={solid, fill=white},
    9191         rel/.style={font=\scriptsize, fill=white, inner sep=2pt},
    9292         diag/.style={row sep={11mm,between origins},
     
    114114\newsavebox{\execbox}
    115115\savebox{\execbox}{\tikz[baseline=-.5ex]\draw [-stealth] (0,0) -- ++(1em, 0);}
    116 \newcommand{\exec}{\ensuremath{\mathrel{\usebox{\execbox}}}}
     116% \newcommand{\exec}{\ensuremath{\mathrel{\usebox{\execbox}}}}
     117\newcommand{\exec}{\to}
    117118\let\ar\triangleright
    118 \renewcommand{\verb}{\lstinline[mathescape,basicstyle=\tt\selectfont]}
    119 
    120 \let\class\triangleright
     119\renewcommand{\verb}{\lstinline[mathescape,basicstyle=\tt\selectfont,
     120                                identifierstyle=\texttt]}
     121
     122\let\class\colon
    121123\let\andalso\quad
    122124
     
    544546%
    545547% For example the following execution history of the program in \autoref{fig:esempio}
    546 % $$I_1; \verb+CALL f+; \verb+COND l+; \verb+EMIT $\ell_2$+; I_3; \verb+RET+; I_2; \verb+RET+$$
     548% $$I_1; \verb+CALL f+; \verb+COND l+; \verb+EMIT $L_2$+; I_3; \verb+RET+; I_2; \verb+RET+$$
    547549% emits the trace
    548550% $$\verb+main+, \verb+f+$$
     
    569571% \begin{lstlisting}
    570572% f: $\!$COND l
    571 %    EMIT $\ell_2$
     573%    EMIT $L_2$
    572574%    RET
    573 % l: $\!$EMIT $\ell_3$
     575% l: $\!$EMIT $L_3$
    574576%    $I_3$
    575577%    RET
     
    580582% f
    581583%
    582 % $\ell_2$
    583 %
    584 % $\ell_3$
    585 % $\ell_3$
     584% $L_2$
     585%
     586% $L_3$
     587% $L_3$
    586588% \end{lstlisting}
    587589% \end{minipage}
     
    14331435 $s_1\S s_2'$, otherwise if $L\notin\ell(\Functions)$ then $s_1\S s_2$.
    14341436\end{itemize}
     1437This relation captures the fact that synchronisation on labels can be decoupled from
     1438``semantic synchronisation'' (in particular at the start of functions). $s_1\L s_2$
     1439tells that the two state are synchronised as to labels, and $s_2$ will eventually
     1440synchronise semantically using only silent execution steps (apart from the very first
     1441emit).
    14351442
    14361443Given the relations $\S$ and $\C$, \autoref{fig:forwardsim} defines a set of
     
    14701477    \matrix [diag] (m) {%
    14711478         \node (s1) {s_1}; & \node (t1) {s_1'};\\
    1472          \node (s2) {s_2}; & \node (t2) {s_2'}; \\
     1479         \node (s2) {s_2}; & \node [newn] (t2) {s_2'}; \\
    14731480    };
    14741481    {[-stealth]
     
    15231530    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
    15241531    \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2);
    1525     \draw [new] (t1) to [bend right] node [rel] {$\C$} (c);
     1532    \draw [new] (s1) to [bend right] node [rel] {$\C$} (c);
    15261533\end{tikzpicture}
    15271534\qquad\qquad
     
    15501557
    15511558\begin{lemma}
    1552 If $S_1,S_2,\S,\C$ satisfy the diagrams in \autoref{fig:forwardsim},
     1559If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
    15531560$T_1=s_1\To s_1'$ is a structured fragment not starting with a $\ell(f)$ emission,
    15541561and $s_1\S s_2$, then there is $T_2=s_2\To s_2'$ with $T\approx T'$ and $s_1'\S s_2'$.
    15551562\end{lemma}
    15561563\begin{theorem}
    1557 If $S_1,S_2,\S,\C$ satisfy the diagrams in \autoref{fig:forwardsim},
    1558 $M_1:s_1\to^{*} s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that
    1559 $s_1\L s_2$, then there is $M_2:s_2\to^{*} s_2'$ with $M_1\approx M_2$.
     1564If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
     1565$M_1:s_1\MeasTo s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that
     1566$s_1\L s_2$, then there is $M_2:s_2\MeasTo s_2'$ with $M_1\approx M_2$. Moreover,
     1567there is a state $s_2''$ with $s_2'\to[\tau *]s_2''$ and $s_1'\S s_2''$.
    15601568\end{theorem}
    15611569@@@@@@@@@@@@@@@@@@@@@@@
     
    20312039source code in order to reason on it.
    20322040
     2041\section{The formalisation}
     2042As we already explained, for the sake of presentation we explained the formal
     2043content of our results departing from the actual Matita formalisation. In this
     2044section we explain the basis of the Matita development, heavily based on
     2045inductive definitions and dependent types.
     2046
     2047\paragraph*{The main differences.} The main points where the development diverges
     2048from the material presented in the previous sections are the following.
     2049\begin{itemize}
     2050 \item Rather than having a generic notion of fragment and a predicate of
     2051 structuredness and measurability, we use inductive definitions internalising
     2052 the conditions. Among other things this turns the proof of \autoref{preservation} a matter of
     2053 structural induction, when it would require more complex induction schemes
     2054 otherwise.
     2055 \item As we are dealing with a deterministic labelling transition system, we
     2056 purposedly blur the distinction between labelling the transitions and labelling
     2057 the states originating them, and opt in general for the latter in the actual
     2058 definitions.
     2059 \item ................. ALTRO?
     2060 \item A small difference lies in the naming conventions. In this paper we went
     2061 with the tradition of labelled transition systems and named sequences of states
     2062 and steps \emph{execution fragments}. In the development we named our structures
     2063 \emph{traces}. In the remainder of this section we will use both names.
     2064\end{itemize}
     2065
     2066\paragraph*{The main definitions.}
     2067The notion of deterministic labelled transition system is captured in the development
     2068via the abstract data type called $\verb+abstract_status+$. The fields
     2069of this record are the following.
     2070\begin{itemize}
     2071 \item \verb+S : Type[0]+, the type of states.
     2072 \item \verb+as_execute : S $\to$ S $\to$ Prop+, a the binary predicate modelling
     2073 the execution. As in the previous sections, we write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$.
     2074 \item \verb+as_classifier : S $\to$ classification+, a function tagging all
     2075 states with a class in
     2076 $\{$\verb+cl_return,cl_jump,cl_call,cl_other+$\}$, depending on the instruction
     2077 that is about to be executed (we omit tail-calls for simplicity). We will
     2078 use $s \class c$ as a shorthand for both $\verb+as_classifier+~s=c$
     2079 (if $c$ is a classification) and $\verb+as_classifier+~s\in c$
     2080 (if $c$ is a set of classifications). This partly replaces the labelling of execution
     2081 steps.
     2082 \item \verb+as_label : S $\to$ option label+, telling whether the
     2083 next instruction to be executed in $s$ is a cost emission statement,
     2084 and if yes returning the associated cost label. Our shorthand for this function
     2085 will be $L$, and we will also abuse the notation by using $L~s$ as a
     2086 predicate stating that $s$ is labelled.
     2087 \item \verb+as_call_ident : ($\Sigma$s:S. s $\class$ cl_call) $\to$ label+,
     2088 telling the identifier of the function which is being called in a
     2089 \verb+cl_call+ state. We will use the shorthand $s\uparrow f$ for
     2090 $\verb+as_call_ident+~s = f$.
     2091 \item \verb+as_after_return : ($\Sigma$s:S. s $\class$ cl_call) $\to$ S $\to$ Prop+,
     2092 which holds on the \verb+cl_call+ state $s_1$ and a state $s_2$ when the
     2093 instruction to be executed in $s_2$ follows the function call to be
     2094 executed in (the witness of the $\Sigma$-type) $s_1$, i.e. when $s_1\ar s_2$.
     2095\end{itemize}
     2096%
     2097% % \begin{alltt}
     2098% % record abstract_status := \{ S: Type[0];
     2099% %  as_execute: S \(\to\) S \(\to\) Prop;   as_classifier: S \(\to\) classification;
     2100% %  as_label: S \(\to\) option label;    as_called: (\(\Sigma\)s:S. c s = cl_call) \(\to\) label;
     2101% %  as_after_return: (\(\Sigma\)s:S. c s = cl_call) \(\to\) S \(\to\) Prop \}
     2102% % \end{alltt}
     2103%
     2104The inductive type for structured traces is actually made by three multiple
     2105inductive types with the following semantics:
     2106\begin{enumerate}
     2107 \item $(\verb+trace_label_return+~s_1~s_2)$ (shorthand $\verb+TLR+~s_1~s_2$)
     2108   is in fact what we called a measurable fragment ending in a return step.
     2109%    is a trace that begins in
     2110%    the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
     2111%    such that the instruction to be executed in $s_1$ is a label emission
     2112%    statement and the one to be executed in the state before $s_2$ is a return
     2113%    statement. Thus $s_2$ is the state after the return. The trace
     2114%    may contain other label emission statements. It captures the structure of
     2115%    the execution of function bodies: they must start with a cost emission
     2116%    statement and must end with a return; they are obtained by concatenating
     2117%    one or more basic blocks, all starting with a label emission
     2118%    (e.g. in case of loops).
     2119 \item $(\verb+trace_label_label+~b~s_1~s_2)$ (shorthand $\verb+TLL+~b~s_1~s_2$)
     2120   models basic blocks. It is the special case of a measurable fragment containing
     2121   only its first label emission.
     2122 \item $(\verb+trace_any_label+~b~s_1~s_2)$ (shorthand $\verb+TAL+~b~s_1~s_2$)
     2123   is a structured fragment, possibly with a return step appended to it, that
     2124   does not contain any label apart possibly from the first state.
     2125\end{enumerate}
     2126The above definition summarise the formal rules shown in \autoref{fig:traces}.
     2127\begin{figure}
     2128\begin{multicols}{3}
     2129\infrule[\verb+tlr_base+]
     2130 {\verb+TLL+~true~s_1~s_2}
     2131 {\verb+TLR+~s_1~s_2}
     2132
     2133\infrule[\verb+tlr_step+]
     2134 {\verb+TLL+~false~s_1~s_2 \andalso
     2135  \verb+TLR+~s_2~s_3
     2136 }
     2137 {\verb+TLR+~s_1~s_3}
     2138
     2139\infrule[\verb+tll_base+]
     2140 {\verb+TAL+~b~s_1~s_2 \andalso
     2141  L~s_1
     2142 }
     2143 {\verb+TLL+~b~s_1~s_2}
     2144\end{multicols}
     2145
     2146\infrule[\verb+tal_base_not_return+]
     2147 {s_1\exec s_2 \andalso
     2148  s_1\class\{\verb+cl_jump+, \verb+cl_other+\}\andalso
     2149  L~s_2
     2150 }
     2151 {\verb+TAL+~false~s_1~s_2}
     2152
     2153\infrule[\verb+tal_base_return+]
     2154 {s_1\exec s_2 \andalso
     2155  s_1 \class \verb+cl_return+
     2156 }
     2157 {\verb+TAL+~true~s_1~s_2}
     2158
     2159\infrule[\verb+tal_base_call+]
     2160 {s_1\exec s_2 \andalso
     2161  s_1 \class \verb+cl_call+ \andalso
     2162  s_1\ar s_3 \andalso
     2163  \verb+TLR+~s_2~s_3 \andalso
     2164  L~s_3
     2165 }
     2166 {\verb+TAL+~false~s_1~s_3}
     2167
     2168\infrule[\verb+tal_step_call+]
     2169 {s_1\exec s_2 \andalso
     2170  s_1 \class \verb+cl_call+ \andalso
     2171  s_1\ar s_3 \andalso
     2172  \verb+TLR+~s_2~s_3 \andalso
     2173  \verb+TAL+~b~s_3~s_4
     2174 }
     2175 {\verb+TAL+~b~s_1~s_4}
     2176
     2177\infrule[\verb+tal_step_default+]
     2178 {s_1\exec s_2 \andalso
     2179  \lnot L~s_2 \andalso
     2180  \verb+TAL+~b~s_2~s_3\andalso
     2181  s_1 \class \verb+cl_other+
     2182 }
     2183 {\verb+TAL+~b~s_1~s_3}
     2184\caption{The rules forming the inductive definitions of structured
     2185         traces.}
     2186\label{fig:traces}
     2187\end{figure}
     2188\begin{comment}
     2189\begin{verbatim}
     2190inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
     2191  | tlr_base:
     2192      ∀status_before: S.
     2193      ∀status_after: S.
     2194        trace_label_label S ends_with_ret status_before status_after →
     2195        trace_label_return S status_before status_after
     2196  | tlr_step:
     2197      ∀status_initial: S.
     2198      ∀status_labelled: S.
     2199      ∀status_final: S.
     2200        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
     2201        trace_label_return S status_labelled status_final →
     2202          trace_label_return S status_initial status_final
     2203with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
     2204  | tll_base:
     2205      ∀ends_flag: trace_ends_with_ret.
     2206      ∀start_status: S.
     2207      ∀end_status: S.
     2208        trace_any_label S ends_flag start_status end_status →
     2209        as_costed S start_status →
     2210          trace_label_label S ends_flag start_status end_status
     2211with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
     2212  (* Single steps within a function which reach a label.
     2213     Note that this is the only case applicable for a jump. *)
     2214  | tal_base_not_return:
     2215      ∀start_status: S.
     2216      ∀final_status: S.
     2217        as_execute S start_status final_status →
     2218        (as_classifier S start_status cl_jump ∨
     2219         as_classifier S start_status cl_other) →
     2220        as_costed S final_status →
     2221          trace_any_label S doesnt_end_with_ret start_status final_status
     2222  | tal_base_return:
     2223      ∀start_status: S.
     2224      ∀final_status: S.
     2225        as_execute S start_status final_status →
     2226        as_classifier S start_status cl_return →
     2227          trace_any_label S ends_with_ret start_status final_status
     2228  (* A call followed by a label on return. *)
     2229  | tal_base_call:
     2230      ∀status_pre_fun_call: S.
     2231      ∀status_start_fun_call: S.
     2232      ∀status_final: S.
     2233        as_execute S status_pre_fun_call status_start_fun_call →
     2234        ∀H:as_classifier S status_pre_fun_call cl_call.
     2235          as_after_return S «status_pre_fun_call, H» status_final →
     2236          trace_label_return S status_start_fun_call status_final →
     2237          as_costed S status_final →
     2238            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
     2239  (* A call followed by a non-empty trace. *)
     2240  | tal_step_call:
     2241      ∀end_flag: trace_ends_with_ret.
     2242      ∀status_pre_fun_call: S.
     2243      ∀status_start_fun_call: S.
     2244      ∀status_after_fun_call: S.
     2245      ∀status_final: S.
     2246        as_execute S status_pre_fun_call status_start_fun_call →
     2247        ∀H:as_classifier S status_pre_fun_call cl_call.
     2248          as_after_return S «status_pre_fun_call, H» status_after_fun_call →
     2249          trace_label_return S status_start_fun_call status_after_fun_call →
     2250          ¬ as_costed S status_after_fun_call →
     2251          trace_any_label S end_flag status_after_fun_call status_final →
     2252            trace_any_label S end_flag status_pre_fun_call status_final
     2253  | tal_step_default:
     2254      ∀end_flag: trace_ends_with_ret.
     2255      ∀status_pre: S.
     2256      ∀status_init: S.
     2257      ∀status_end: S.
     2258        as_execute S status_pre status_init →
     2259        trace_any_label S end_flag status_init status_end →
     2260        as_classifier S status_pre cl_other →
     2261        ¬ (as_costed S status_init) →
     2262          trace_any_label S end_flag status_pre status_end.
     2263\end{verbatim}
     2264\end{comment}
     2265
     2266
     2267The equivalent of $|T|$ on fragments can be easily defined by mutual recursion
     2268on the three types of traces defined in \autoref{fig:traces}.
     2269% There are three mutual structural recursive functions, one for each of
     2270% \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation
     2271% $|\,.\,|$: the \emph{flattening} of the traces. These functions
     2272% allow to extract from a structured trace the list of emitted cost labels.
     2273%  We only show here the type of one
     2274% of them:
     2275% \begin{alltt}
     2276% flatten_trace_label_return:
     2277%  \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\).
     2278%   trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S)
     2279% \end{alltt}
     2280%
     2281% \paragraph{Structured traces similarity and cost prediction invariance.}
     2282%
     2283% A compiler pass maps source to object code and initial states to initial
     2284% states. The source code and initial state uniquely determine the structured
     2285% trace of a program, if it exists. The structured trace fails to exists iff
     2286% the structural conditions are violated by the program execution (e.g. a function
     2287% body does not start with a cost emission statement). Let us assume that the
     2288% target structured trace exists.
     2289%
     2290% What is the relation between the source and target structured traces?
     2291% In general, the two traces can be arbitrarily different. However, we are
     2292% interested only in those compiler passes that maps a trace $\tau_1$ to a trace
     2293% $\tau_2$ such that
     2294% \begin{equation}|\tau_1| = |\tau_2|.\label{th2}\end{equation}
     2295% The reason is that the combination of~\eqref{th1} with~\eqref{th2} yields the
     2296% corollary
     2297% \begin{equation}\label{th3}
     2298% \forall s_1,s_2. \forall \tau: \verb+TLR+~s_1~s_2.~
     2299%   \verb+clock+~s_2 - \verb+clock+~s_1 =
     2300%   \Sigma_{\alpha \in |\tau_1|}\;k(\alpha) =
     2301%   \Sigma_{\alpha \in |\tau_2|}\;k(\alpha).
     2302% \end{equation}
     2303% This 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
     2304% transfer the cost model from the target to the source code and reason on the
     2305% source code only.
     2306%
     2307% We are therefore interested in conditions stronger than~\eqref{th2}.
     2308% Therefore we introduce here a similarity relation between traces with
     2309% the same structure. Theorem~\verb+tlr_rel_to_traces_same_flatten+
     2310% in the Matita formalisation shows that~\eqref{th2} holds for every pair
     2311% $(\tau_1,\tau_2)$ of similar traces.
     2312%
     2313% Intuitively, two traces are similar when one can be obtained from
     2314% the other by erasing or inserting silent steps, i.e. states that are
     2315% not \verb+as_costed+ and that are classified as \verb+cl_other+.
     2316% Silent steps do not alter the structure of the traces.
     2317% In particular,
     2318% the relation maps function calls to function calls to the same function,
     2319% label emission statements to emissions of the same label, concatenation of
     2320% subtraces to concatenation of subtraces of the same length and starting with
     2321% the same emission statement, etc.
     2322%
     2323% In the formalisation the three similarity relations --- one for each trace
     2324% kind --- are defined by structural recursion on the first trace and pattern
     2325% matching over the second. Here we turn
     2326% the definition into the inference rules shown in \autoref{fig:txx_rel}
     2327% for the sake of readability. We also omit from trace constructors all arguments,
     2328% but those that are traces or that
     2329% are used in the premises of the rules. By abuse of notation we denote all three
     2330% relations by infixing $\approx$.
     2331%
     2332% \begin{figure}
     2333% \begin{multicols}{2}
     2334% \infrule
     2335%  {tll_1\approx tll_2
     2336%  }
     2337%  {\verb+tlr_base+~tll_1 \approx \verb+tlr_base+~tll_2}
     2338%
     2339% \infrule
     2340%  {tll_1 \approx tll_2 \andalso
     2341%   tlr_1 \approx tlr_2
     2342%  }
     2343%  {\verb+tlr_step+~tll_1~tlr_1 \approx \verb+tlr_step+~tll_2~tlr_2}
     2344% \end{multicols}
     2345% \vspace{3ex}
     2346% \begin{multicols}{2}
     2347% \infrule
     2348%  {L~s_1 = L~s_2 \andalso
     2349%   tal_1\approx tal_2
     2350%  }
     2351%  {\verb+tll_base+~s_1~tal_1 \approx \verb+tll_base+~s_2~tal_2}
     2352%
     2353% \infrule
     2354%  {tal_1\approx tal_2
     2355%  }
     2356%  {\verb+tal_step_default+~tal_1 \approx tal_2}
     2357% \end{multicols}
     2358% \vspace{3ex}
     2359% \infrule
     2360%  {}
     2361%  {\verb+tal_base_not_return+\approx taa \append \verb+tal_base_not_return+}
     2362% \vspace{1ex}
     2363% \infrule
     2364%  {}
     2365%  {\verb+tal_base_return+\approx taa \append \verb+tal_base_return+}
     2366% \vspace{1ex}
     2367% \infrule
     2368%  {tlr_1\approx tlr_2 \andalso
     2369%   s_1 \uparrow f \andalso s_2\uparrow f
     2370%  }
     2371%  {\verb+tal_base_call+~s_1~tlr_1\approx taa \append \verb+tal_base_call+~s_2~tlr_2}
     2372% \vspace{1ex}
     2373% \infrule
     2374%  {tlr_1\approx tlr_2 \andalso
     2375%   s_1 \uparrow f \andalso s_2\uparrow f \andalso
     2376%   \verb+tal_collapsable+~tal_2
     2377%  }
     2378%  {\verb+tal_base_call+~s_1~tlr_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2)}
     2379% \vspace{1ex}
     2380% \infrule
     2381%  {tlr_1\approx tlr_2 \andalso
     2382%   s_1 \uparrow f \andalso s_2\uparrow f \andalso
     2383%   \verb+tal_collapsable+~tal_1
     2384%  }
     2385%  {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_base_call+~s_2~tlr_2)}
     2386% \vspace{1ex}
     2387% \infrule
     2388%  {tlr_1 \approx tlr_2 \andalso
     2389%   s_1 \uparrow f \andalso s_2\uparrow f\andalso
     2390%   tal_1 \approx tal_2 \andalso
     2391%  }
     2392%  {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2}
     2393% \caption{The inference rule for the relation $\approx$.}
     2394% \label{fig:txx_rel}
     2395% \end{figure}
     2396% %
     2397% \begin{comment}
     2398% \begin{verbatim}
     2399% let rec tlr_rel S1 st1 st1' S2 st2 st2'
     2400%   (tlr1 : trace_label_return S1 st1 st1')
     2401%   (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
     2402% match tlr1 with
     2403%   [ tlr_base st1 st1' tll1 ⇒
     2404%     match tlr2 with
     2405%     [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
     2406%     | _ ⇒ False
     2407%     ]
     2408%   | tlr_step st1 st1' st1'' tll1 tl1 ⇒
     2409%     match tlr2 with
     2410%     [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
     2411%       tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
     2412%     | _ ⇒ False
     2413%     ]
     2414%   ]
     2415% and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
     2416%  (tll1 : trace_label_label S1 fl1 st1 st1')
     2417%  (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
     2418%   match tll1 with
     2419%   [ tll_base fl1 st1 st1' tal1 H ⇒
     2420%     match tll2 with
     2421%     [ tll_base fl2 st2 st2 tal2 G ⇒
     2422%       as_label_safe … («?, H») = as_label_safe … («?, G») ∧
     2423%       tal_rel … tal1 tal2
     2424%     ]
     2425%   ]
     2426% and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
     2427%  (tal1 : trace_any_label S1 fl1 st1 st1')
     2428%  (tal2 : trace_any_label S2 fl2 st2 st2')
     2429%    on tal1 : Prop ≝
     2430%   match tal1 with
     2431%   [ tal_base_not_return st1 st1' _ _ _ ⇒
     2432%     fl2 = doesnt_end_with_ret ∧
     2433%     ∃st2mid,taa,H,G,K.
     2434%     tal2 ≃ taa_append_tal ? st2 ??? taa
     2435%       (tal_base_not_return ? st2mid st2' H G K)
     2436%   | tal_base_return st1 st1' _ _ ⇒
     2437%     fl2 = ends_with_ret ∧
     2438%     ∃st2mid,taa,H,G.
     2439%     tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
     2440%       (tal_base_return ? st2mid st2' H G)
     2441%   | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒
     2442%     fl2 = doesnt_end_with_ret ∧
     2443%     ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
     2444%     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
     2445%     (* we must allow a tal_base_call to be similar to a call followed
     2446%       by a collapsable trace (trace_any_any followed by a base_not_return;
     2447%       we cannot use trace_any_any as it disallows labels in the end as soon
     2448%       as it is non-empty) *)
     2449%     (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
     2450%       tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
     2451%     ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
     2452%     ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
     2453%       tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
     2454%       tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
     2455%   | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
     2456%     ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
     2457%     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
     2458%     (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
     2459%       tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
     2460%       tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
     2461%     ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
     2462%     ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
     2463%       tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
     2464%       tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
     2465%   | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
     2466%     tal_rel … tl1 tal2 (* <- this makes it many to many *)
     2467%   ].
     2468% \end{verbatim}
     2469% \end{comment}
     2470% %
     2471% In the preceding rules, a $taa$ is an inhabitant of the
     2472% $\verb+trace_any_any+~s_1~s_2$ (shorthand $\verb+TAA+~s_1~s_2$),
     2473% an inductive data type whose definition
     2474% is not in the paper for lack of space. It is the type of valid
     2475% prefixes (even empty ones) of \verb+TAL+'s that do not contain
     2476% any function call. Therefore it
     2477% is possible to concatenate (using ``$\append$'') a \verb+TAA+ to the
     2478% left of a \verb+TAL+. A \verb+TAA+ captures
     2479% a sequence of silent moves.
     2480% The \verb+tal_collapsable+ unary predicate over \verb+TAL+'s
     2481% holds when the argument does not contain any function call and it ends
     2482% with a label (not a return). The intuition is that after a function call we
     2483% can still perform a sequence of silent actions while remaining similar.
     2484%
     2485% As should be expected, even though the rules are asymmetric $\approx$ is in fact
     2486% an equivalence relation.
    20332487\bibliographystyle{splncs03}
    20342488\bibliography{ccexec}
Note: See TracChangeset for help on using the changeset viewer.