Changeset 2611 for Papers


Ignore:
Timestamp:
Feb 6, 2013, 2:21:23 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r2610 r2611  
    55\usepackage{listings}
    66\usepackage{bcprules}
     7\usepackage{verbatim}
    78
    89% NB: might be worth removing this if changing class in favour of
     
    382383   a basic block.
    383384\end{enumerate}
     385
     386\infrule[\texttt{tlr\_base}]
     387 {\texttt{trace\_label\_label}~true~s_1~s_2}
     388 {\texttt{trace\_label\_return}~s_1~s_2}
     389
     390\infrule[\texttt{tlr\_step}]
     391 {\texttt{trace\_label\_label}~false~s_1~s_2 \andalso
     392  \texttt{trace\_label\_return}~s_2~s_3
     393 }
     394 {\texttt{trace\_label\_return}~s_1~s_3}
     395
     396\infrule[\texttt{tll\_base}]
     397 {\texttt{trace\_any\_label}~b~s_1~s_2 \andalso
     398  \texttt{as\_costed}~s_1
     399 }
     400 {\texttt{trace\_label\_label}~b~s_1~s_2}
     401
     402\infrule[\texttt{tal\_base\_not\_return}]
     403 {\texttt{as\_execute}~s_1~s_2 \andalso
     404  \texttt{as\_classifier}~s_1~k \\
     405  k \in \{\texttt{cl\_jump,cl\_other}\} \andalso
     406  \texttt{as\_costed}~s_2
     407 }
     408 {\texttt{trace\_any\_label}~false~s_1~s_2}
     409
     410\infrule[\texttt{tal\_base\_return}]
     411 {\texttt{as\_execute}~s_1~s_2 \andalso
     412  \texttt{as\_classifier}~s_1~\texttt{cl\_return} \\
     413 }
     414 {\texttt{trace\_any\_label}~true~s_1~s_2}
     415
     416\infrule[\texttt{tal\_base\_call}]
     417 {\texttt{as\_execute}~s_1~s_2 \andalso
     418  \texttt{as\_classifier}~s_1~\texttt{cl\_call} \\
     419  \texttt{as\_after\_return}~s_1~s_3 \andalso
     420  \texttt{trace\_label\_return}~s_2~s_3 \andalso
     421  \texttt{as\_costed}~s_3
     422 }
     423 {\texttt{trace\_any\_label}~false~s_1~s_3}
     424
     425\infrule[\texttt{tal\_step\_call}]
     426 {\texttt{as\_execute}~s_1~s_2 \andalso
     427  \texttt{as\_classifier}~s_1~\texttt{cl\_call} \\
     428  \texttt{as\_after\_return}~s_1~s_3 \andalso
     429  \texttt{trace\_label\_return}~s_2~s_3 \\
     430  \lnot \texttt{as\_costed}~s_3 \andalso
     431  \texttt{trace\_any\_label}~b~s_3~s_4
     432 }
     433 {\texttt{trace\_any\_label}~b~s_1~s_4}
     434
     435\infrule[\texttt{tal\_step\_default}]
     436 {\texttt{as\_execute}~s_1~s_2 \andalso
     437  \texttt{trace\_any\_label}~b~s_2~s_3
     438  \texttt{as\_classifier}~s_1~\texttt{cl\_other} \\
     439  \lnot \texttt{as\_costed}~s_2
     440 }
     441 {\texttt{trace\_any\_label}~b~s_1~s_3}
     442
     443
     444\begin{comment}
    384445\begin{verbatim}
    385446inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
     
    457518          trace_any_label S end_flag status_pre status_end.
    458519\end{verbatim}
     520\end{comment}
    459521A \texttt{trace\_label\_return} is isomorphic to a list of
    460522\texttt{trace\_label\_label}s that end with a cost emission followed by a
Note: See TracChangeset for help on using the changeset viewer.