Changeset 3368


Ignore:
Timestamp:
Jun 17, 2013, 10:34:38 PM (4 years ago)
Author:
sacerdot
Message:

..

File:
1 edited

Legend:

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

    r3367 r3368  
    243243
    244244The plan of this paper is the following. In Section~\ref{sec:labelling} we
    245 sketch the labelling method and the problems derived from the application
    246 to languages with function calls. In Section~\ref{sec:semantics} we introduce
    247 a generic description of an unstructured imperative language and the
    248 corresponding structured fragments (the novel semantics). In
    249 Section~\ref{sec:simulation} we describe the forward simulation proof.
     245summarize the labelling method. In Section~\ref{extension} we scale
     246the method to unstructured languages with function calls. In
     247Section~\ref{sec:simulation} we give the necessary condition for the
     248correctness of the compiler (forward simulation proof).
     249Section~\ref{sec:formalization} sketches the formalization of the
     250datastructures and proofs in Matita.
    250251Conclusions and future works are in Section~\ref{sec:conclusions}
    251252
     
    347348
    348349\section{Extending the labelling approach to function calls}
     350\label{extension}
    349351%
    350352Let's now consider a simple program written in C that contains a function
     
    785787   contains the jump.
    786788\end{enumerate}
    787 One might wonder why $f$ and $\ell(f)$, that aways appear in this order, are not
     789One might wonder why $f$ and $\ell(f)$, that always appear in this order, are not
    788790collapsed into a single observable. This would simplify some aspects of the
    789791formalisation at the price of others. For example, we should add special
     
    803805 \label{thm:static}
    804806 for all measurable fragment $M = s_0 \to^{*} s_n$,\\
    805  $$\Delta_t := \verb+clock+_{s_n} - \verb+clock+_{s_0} = \Sigma_{o \in |T|} k(o)$$
     807 $$\Delta_t := \verb+clock+_{s_n} - \verb+clock+_{s_0} = \Sigma_{o \in |M|} k(o)$$
    806808\end{theorem}
    807809
     
    838840\emph{weakly trace equivalent} if their weak traces are equal.
    839841
    840 A compiler (pass) that preserves the program semantics also preserves weak
    841 traces and propagates measurability iff for every measurable
     842A compiler (pass) that preserves the program semantics also \emph{preserves weak
     843traces and propagates measurability} iff for every measurable
    842844fragment $M_1 = s_1 \to^{*} s_1'$ of the source code, the corresponding
    843845execution fragment $M_2 = s_2 \to^{*} s_2'$ of the object code is measurable
     
    857859\begin{theorem}\label{thm:preservation}
    858860Given a compiler that preserves weak traces and propagates measurability,
    859 for all measurable execution fragment $T_1 = s_1 \to^{*} s_1'$ of the source
    860 code such that $T_2 = s_2 \to^{*} s_2'$ is the corresponding fragment of the
     861for all measurable execution fragment $M_1 = s_1 \to^{*} s_1'$ of the source
     862code such that $M_2 = s_2 \to^{*} s_2'$ is the corresponding fragment of the
    861863object code,
    862864
    863 $$\Delta_t := \verb+clock+_{s_2'} - \verb+clock+_{s_2} = \Sigma_{o \in |T_2|} k(o) = \Sigma_{o \in |T_1|} k(o)$$
     865$$\Delta_t := \verb+clock+_{s_2'} - \verb+clock+_{s_2} = \Sigma_{o \in |M_2|} k(o) = \Sigma_{o \in |M_1|} k(o)$$
    864866\end{theorem}
    865867
     
    867869\label{sec:simulation}
    868870Because of \autoref{thm:preservation}, to certify a compiler for the labelling
    869 approach we need to both prove that it respects the functional semantics of the
    870 program, and that it preserves weak traces and propagates measurability.
    871 We achieve this by independently proving the three properties for each compiler
     871approach we need to prove that it respects the functional semantics of the
     872program, preserves weak traces and propagates measurability.
     873We achieve this by proving the three properties independently for each compiler
    872874pass.
    873875The first property is standard and can be proved by means of a forward simulation argument (see for example~\cite{compcert3}) that runs like this.
     
    19711973\end{comment}
    19721974\section{The formalisation}
    1973 As we already explained, for the sake of presentation we explained the formal
     1975\label{sec:formalization}
     1976As we already explained, for the sake of presentation we presented the formal
    19741977content of our results departing from the actual Matita formalisation. In this
    19751978section we explain the basis of the Matita development, heavily based on
     
    19811984from the material presented in the previous sections are the following.
    19821985\begin{itemize}
    1983  \item Rather than having a generic notion of fragment and a predicate of
    1984  structuredness and measurability, we use inductive definitions internalising
    1985  the conditions. Among other things this turns the proof of \autoref{thm:preservation}
     1986 \item Rather than having a generic notion of fragment and predicates of
     1987 structuredness and measurability, we use inductive definitions and
     1988 dependent types to provide data types that satisfy the
     1989 conditions by construction.
     1990 Among other things this turns the proof of \autoref{thm:preservation}
    19861991 into a matter of
    19871992 structural induction, when it would require additional lemmas
     
    20072012\begin{itemize}
    20082013 \item \verb+S : Type[0]+, the type of states.
    2009  \item \verb+as_execute : S $\to$ S $\to$ Prop+, a the binary predicate modelling
     2014 \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate modelling
    20102015 the execution. As in the previous sections, we write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$.
    20112016 \item \verb+as_classifier : S $\to$ classification+, a function tagging all
     
    24442449We restored static predictability by introducing a new semantics for unstructured
    24452450programs that single outs well structured executions. The latter are represented
    2446 by structured traces, a generalisation of streams of observables that capture
     2451by structured execution fragments, a generalisation of streams of observables that capture
    24472452several structural invariants of the execution, like well nesting of functions
    24482453or the fact that every basic block must start with a code emission statement.
Note: See TracChangeset for help on using the changeset viewer.