Changeset 3367


Ignore:
Timestamp:
Jun 17, 2013, 7:16:15 PM (4 years ago)
Author:
tranquil
Message:

...

File:
1 edited

Legend:

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

    r3366 r3367  
    237237The statement of the generic proof is based on a new semantics
    238238for imperative unstructured languages that is based on \emph{structured
    239 traces} and that restores the preservation of structure in the observables of
     239execution fragments} and that restores the preservation of structure in the observables of
    240240the semantics. The generic proof allows to almost completely split the
    241241part of the simulation that deals with functional properties only from the
     
    246246to languages with function calls. In Section~\ref{sec:semantics} we introduce
    247247a generic description of an unstructured imperative language and the
    248 corresponding structured traces (the novel semantics). In
     248corresponding structured fragments (the novel semantics). In
    249249Section~\ref{sec:simulation} we describe the forward simulation proof.
    250250Conclusions and future works are in Section~\ref{sec:conclusions}
     
    444444We will therefore proceed as follows. In the following section
    4454451) we formally introduce the notion of
    446 structured trace, which captures structured runs in the style of labelled
     446structured execution fragment, which captures structured runs in the style of labelled
    447447transition systems; 2) we show that on the object code we can correctly
    448448compute the execution time of a structured run from the sequence of labels
     
    460460in the interactive theorem prover Matita and are being used to certify
    461461the complexity preserving compiler developed in the CerCo project~\cite{cerco}.
    462 The formalization can be
    463 found at~\ref{YYY} and it heavily relies on algebraic and dependent types for
    464 both structured traces and the definition of weak similarity. In the paper
     462The formalization heavily relies on algebraic and dependent types. In the
     463first part of the paper
    465464we did not try to stay close to the formalization. On the contrary,
    466465the definitions given in the paper are the result of a significant
     
    468467the sake of presentation and to make easier the re-implementation of the
    469468concepts in a proof assistant which is not based on the Calculus of Inductive
    470 Constructions. In any case the formalization is heavily commented to allow the
     469Constructions. In any case the formalization, briefly presented at the end of
     470the paper, is heavily commented to allow the
    471471reader to understand the technical details of the formalization.
    472472
     
    707707% in the semantics. This is the topic of the next section.
    708708
    709 \subsection{Structured traces}
     709\subsection{Structured execution fragments}
    710710\label{sec:semantics}
    711711
     
    767767   of a server implemented as an unbounded loop whose body waits for an
    768768   input, process it and performs an output before looping: the processing
    769    steps form a structured execution fragment.
     769   steps form a structured fragment.
    770770 \item The number of $RET$'s in the fragment is equal to the number of
    771771   calls performed. In combination with the previous condition, this ensures
    772    well-backeting of function calls.
     772   well-bracketing of function calls.
    773773 \item
    774774   \label{req3}
     
    802802\begin{theorem}
    803803 \label{thm:static}
    804  for all measurable fragment $T = s_0 \to^{*} s_n$,\\
     804 for all measurable fragment $M = s_0 \to^{*} s_n$,\\
    805805 $$\Delta_t := \verb+clock+_{s_n} - \verb+clock+_{s_0} = \Sigma_{o \in |T|} k(o)$$
    806806\end{theorem}
     
    840840A compiler (pass) that preserves the program semantics also preserves weak
    841841traces and propagates measurability iff for every measurable
    842 fragment $T_1 = s_1 \to^{*} s_1'$ of the source code, the corresponding
    843 execution fragment $T_2 = s_2 \to^{*} s_2'$ of the object code is measurable
    844 and $T_1$ and $T_2$ are weakly trace equivalent. The very intuitive notion of
     842fragment $M_1 = s_1 \to^{*} s_1'$ of the source code, the corresponding
     843execution fragment $M_2 = s_2 \to^{*} s_2'$ of the object code is measurable
     844and $M_1$ and $M_2$ are weakly trace equivalent. The very intuitive notion of
    845845``corresponding fragment'' is made clear in the forward simulation proof of
    846846preservation of the semantics of the program by saying that $s_2$ and $s_1$
     
    878878the two resulting states are synchronized again according to the relation.
    879879No requirements are imposed on the intermediate target states.
    880 Finally, the lemma is iterated over the execution trace to establish the
     880Finally, the lemma is iterated over the execution fragment to establish the
    881881final result.
    882882
     
    888888preserving translation of every instruction. In order to produce structured
    889889traces, however, code emission cannot be fully compositional any longer,
    890 and requirements need to be enforced on intermediate target states.
     890and requirements need to be enforced on intermediate target states too.
    891891
    892892For example, consider~requirement \ref{req3} that asks every function body
     
    905905need to translate a function call to a function call followed by some
    906906instructions (for example to restore caller-saved registers in the pass that
    907 sets the parameter convenction). In the forward simulation proof, these
     907sets the parameter convention). In the forward simulation proof, these
    908908instructions are taken care of when simulating the \texttt{RETURN} step:
    909909the state just after the return in the source code is matched by the state $s_2$
     
    14451445\end{definition}
    14461446We will require all pairs of states that return from related calls to be
    1447 $\R$-related. This, in combinantion with a dual requirement on function calls,
     1447$\R$-related. This, in combination with a dual requirement on function calls,
    14481448will grant that calls return exactly where they are supposed to be.
    14491449On the other hand the $\LS$ relation captures the fact that synchronisation on labels can be decoupled from
     
    19741974content of our results departing from the actual Matita formalisation. In this
    19751975section we explain the basis of the Matita development, heavily based on
    1976 inductive definitions and dependent types.
     1976inductive definitions and dependent types. The development consists of 3369 lines
     1977of code and can be downloaded from
     1978\begin{center}\url{http://cerco.cs.unibo.it/attachment/wiki/WikiStart/CPP2013.tar.gz}\end{center}
    19771979
    19781980\paragraph*{The main differences.} The main points where the development diverges
     
    19811983 \item Rather than having a generic notion of fragment and a predicate of
    19821984 structuredness and measurability, we use inductive definitions internalising
    1983  the conditions. Among other things this turns the proof of \autoref{thm:preservation} a matter of
    1984  structural induction, when it would require more complex induction schemes
     1985 the conditions. Among other things this turns the proof of \autoref{thm:preservation}
     1986 into a matter of
     1987 structural induction, when it would require additional lemmas
    19851988 otherwise.
    19861989 \item As we are dealing with a deterministic labelling transition system, we
    1987  purposedly blur the distinction between labelling the transitions and labelling
     1990 purposely blur the distinction between labelling the transitions and labelling
    19881991 the states originating them, and opt in general for the latter in the actual
    19891992 definitions.
    1990  \item ................. ALTRO?
     1993 \item As object code cannot have a separate emission instruction, we allow
     1994 any instruction to be labelled, which implies that labels can be emitted
     1995 alongside other observable events.
    19911996 \item A small difference lies in the naming conventions. In this paper we went
    19921997 with the tradition of labelled transition systems and named sequences of states
     
    24562461
    24572462Finally, we identified measurable execution fragments that are those whose
    2458 execution time (once compiled) can be exactly computed looking at the object
    2459 code weak execution traces only. A final instrumentation pass on the source
     2463execution time (once compiled) can be exactly computed looking only at the
     2464weak execution traces of the object
     2465code. A final instrumentation pass on the source
    24602466code can then be used to turn the non functional property of having a certain
    2461 cost into the functional property of granting that a certain global variable
     2467cost into the functional property that a certain global variable
    24622468incremented at the beginning of every block according to the induced cost model
    24632469has a certain value.
     
    24702476the CerCo compiler exploiting the main theorem of this paper. An alternative approach
    24712477to the same problem that we would like to investigate consists in labelling
    2472 every instruction that follows a call. This would still require a form of structured
    2473 execution fragments, stating that no only calls but also returns are always followed
    2474 by an emission. The main downside is the pollution of the instrumented code
     2478every instruction that follows a call.
     2479This would reduce the requirements of the proofs, with
     2480% This would still require a form of structured
     2481% execution fragments, stating that both returns and calls are always followed
     2482% by a label emission.
     2483the downside of polluting the instrumented code
    24752484with many cost annotations.
    24762485
Note: See TracChangeset for help on using the changeset viewer.