Changeset 2622


Ignore:
Timestamp:
Feb 6, 2013, 6:11:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r2616 r2622  
    66\usepackage{bcprules}
    77\usepackage{verbatim}
     8\usepackage{alltt}
    89
    910% NB: might be worth removing this if changing class in favour of
     
    278279\texttt{f(g(x));}. We need to inject an emission statement/instrumentation
    279280instruction just after the execution of \texttt{g}. The only way to do that
    280 is to rewrite the code as \texttt{y = g(x); emit L$_1$; f(y);} for some fresh
     281is to rewrite the code as \texttt{y = g(x); emit L; f(y);} for some fresh
    281282variable \texttt{y}. It is pretty clear how in certain situations the obtained
    282283code would be more obfuscated and then more difficult to manually reason on.
    283284
    284285For the previous reasons, in this paper and in the CerCo project we adopt a
    285 different approach. We do not inject any more emission statement after every
     286different approach. We do not inject emission statements after every
    286287function call. However, we want to propagate a strong additional invariant in
    287288the forward simulation proof. The invariant is the propagation of the structure
     
    293294
    294295In the original labelling approach of~\cite{easylabelling}, the second property
    295 was granted statically (syntactically) as a property of the generated code.
    296 In our revised approach, instead, we will grant the property dinamically:
    297 it will be possible to generate code that does not respect it, as soon as
    298 all execution traces do respect it. For instance, dead code will no longer
     296was granted syntactically as a property of the generated code.
     297In our revised approach, instead, we will impose the property on the runs:
     298it will be possible to generate code that does not respect the syntactic
     299property, as soon as all possible runs respect it. For instance, dead code will no longer
    299300be required to have all basic blocks correctly labelled. The switch is suggested
    300301from the fact that the first of the two properties --- that related to
    301 function calls/returns --- can only be defined as a dinamic property, i.e.
    302 as a property of execution traces, not of the static code. The switch is
     302function calls/returns --- can only be defined as property of runs,
     303not of the static code. The switch is
    303304beneficial to the proof because the original proof was made of two parts:
    304305the forward simulation proof and the proof that the static property was granted.
     
    308309In order to capture the structure semantics so that it is preserved
    309310by a forward simulation argument, we need to make the structure observable
    310 in the semantics. This is the topic of the next Section.
     311in the semantics. This is the topic of the next section.
    311312
    312313\section{Structured traces}
     
    324325
    325326We present here a new definition of semantics where the structure of execution,
    326 as defined in the previous Section, is now observable. The idea is to replace
     327as defined in the previous section, is now observable. The idea is to replace
    327328the stream of observables with a structured data type that makes explicit
    328329function call and returns and that grants some additional invariants by
     
    337338we abstract the type of structure traces over an abstract data type of
    338339abstract statuses:
    339 \begin{verbatim}
    340 record abstract_status := {
    341    S: Type[0]
    342 ;  as_execute: S -> S -> Prop
    343 ;  as_classify: S -> classification
    344 ;  as_costed: S -> Prop
    345 ;  as_label: \forall s. as_costed S s -> label
    346 ;  as_call_ident: \forall s. as_classify S s = cl_call -> label
    347 ;  as_after_return:
    348     (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
    349  
    350 }
    351 \end{verbatim}
     340\begin{alltt}
     341record abstract_status := \{ S: Type[0];
     342 as_execute: S \(\to\) S \(\to\) Prop;     as_classify: S \(\to\) classification;
     343 as_costed: S \(\to\) Prop;      as_label: \(\forall\) s. as_costed S s \(\to\) label;
     344 as_call_ident: \(\forall\) s. as_classify S s = cl_call \(\to\) label;
     345 as_after_return:
     346  (\(\Sigma\)s:as_status. as_classify s = Some ? cl_call) \(\to\) as_status \(\to\) Prop \}
     347\end{alltt}
    352348The predicate $\texttt{as\_execute}~s_1~s_2$ holds if $s_1$ evolves into
    353 $s_2$ in one step; $\texttt{as\_classify}~s~c$ holds if the next instruction
     349$s_2$ in one step;\\ $\texttt{as\_classify}~s~c$ holds if the next instruction
    354350to be executed in $s$ is classified according to $c \in
    355 \{\texttt{return,jump,call,other}\}$ (we omit tailcalls for simplicity);
     351\{\texttt{cl\_return,cl\_jump,cl\_call,cl\_other}\}$ (we omit tailcalls for simplicity);
    356352the predicate $\texttt{as\_costed}~s$ holds if the next instruction to be
    357353executed in $s$ is a cost emission statement (also classified
    358 as \texttt{other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds
     354as \texttt{cl\_other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds
    359355if the next instruction to be executed in $s_2$ follows the function call
    360356to be executed in (the witness of the $\Sigma$-type) $s_1$.
Note: See TracChangeset for help on using the changeset viewer.