# Changeset 3368

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

..

File:
1 edited

### Legend:

Unmodified
 r3367 The plan of this paper is the following. In Section~\ref{sec:labelling} we sketch the labelling method and the problems derived from the application to languages with function calls. In Section~\ref{sec:semantics} we introduce a generic description of an unstructured imperative language and the corresponding structured fragments (the novel semantics). In Section~\ref{sec:simulation} we describe the forward simulation proof. summarize the labelling method. In Section~\ref{extension} we scale the method to unstructured languages with function calls. In Section~\ref{sec:simulation} we give the necessary condition for the correctness of the compiler (forward simulation proof). Section~\ref{sec:formalization} sketches the formalization of the datastructures and proofs in Matita. Conclusions and future works are in Section~\ref{sec:conclusions} \section{Extending the labelling approach to function calls} \label{extension} % Let's now consider a simple program written in C that contains a function contains the jump. \end{enumerate} One might wonder why $f$ and $\ell(f)$, that aways appear in this order, are not One might wonder why $f$ and $\ell(f)$, that always appear in this order, are not collapsed into a single observable. This would simplify some aspects of the formalisation at the price of others. For example, we should add special \label{thm:static} for all measurable fragment $M = s_0 \to^{*} s_n$,\\ $$\Delta_t := \verb+clock+_{s_n} - \verb+clock+_{s_0} = \Sigma_{o \in |T|} k(o)$$ $$\Delta_t := \verb+clock+_{s_n} - \verb+clock+_{s_0} = \Sigma_{o \in |M|} k(o)$$ \end{theorem} \emph{weakly trace equivalent} if their weak traces are equal. A compiler (pass) that preserves the program semantics also preserves weak traces and propagates measurability iff for every measurable A compiler (pass) that preserves the program semantics also \emph{preserves weak traces and propagates measurability} iff for every measurable fragment $M_1 = s_1 \to^{*} s_1'$ of the source code, the corresponding execution fragment $M_2 = s_2 \to^{*} s_2'$ of the object code is measurable \begin{theorem}\label{thm:preservation} Given a compiler that preserves weak traces and propagates measurability, for all measurable execution fragment $T_1 = s_1 \to^{*} s_1'$ of the source code such that $T_2 = s_2 \to^{*} s_2'$ is the corresponding fragment of the for all measurable execution fragment $M_1 = s_1 \to^{*} s_1'$ of the source code such that $M_2 = s_2 \to^{*} s_2'$ is the corresponding fragment of the object code, $$\Delta_t := \verb+clock+_{s_2'} - \verb+clock+_{s_2} = \Sigma_{o \in |T_2|} k(o) = \Sigma_{o \in |T_1|} k(o)$$ $$\Delta_t := \verb+clock+_{s_2'} - \verb+clock+_{s_2} = \Sigma_{o \in |M_2|} k(o) = \Sigma_{o \in |M_1|} k(o)$$ \end{theorem} \label{sec:simulation} Because of \autoref{thm:preservation}, to certify a compiler for the labelling approach we need to both prove that it respects the functional semantics of the program, and that it preserves weak traces and propagates measurability. We achieve this by independently proving the three properties for each compiler approach we need to prove that it respects the functional semantics of the program, preserves weak traces and propagates measurability. We achieve this by proving the three properties independently for each compiler pass. The first property is standard and can be proved by means of a forward simulation argument (see for example~\cite{compcert3}) that runs like this. \end{comment} \section{The formalisation} As we already explained, for the sake of presentation we explained the formal \label{sec:formalization} As we already explained, for the sake of presentation we presented the formal content of our results departing from the actual Matita formalisation. In this section we explain the basis of the Matita development, heavily based on from the material presented in the previous sections are the following. \begin{itemize} \item Rather than having a generic notion of fragment and a predicate of structuredness and measurability, we use inductive definitions internalising the conditions. Among other things this turns the proof of \autoref{thm:preservation} \item Rather than having a generic notion of fragment and predicates of structuredness and measurability, we use inductive definitions and dependent types to provide data types that satisfy the conditions by construction. Among other things this turns the proof of \autoref{thm:preservation} into a matter of structural induction, when it would require additional lemmas \begin{itemize} \item \verb+S : Type[0]+, the type of states. \item \verb+as_execute : S $\to$ S $\to$ Prop+, a the binary predicate modelling \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate modelling the execution. As in the previous sections, we write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$. \item \verb+as_classifier : S $\to$ classification+, a function tagging all We restored static predictability by introducing a new semantics for unstructured programs that single outs well structured executions. The latter are represented by structured traces, a generalisation of streams of observables that capture by structured execution fragments, a generalisation of streams of observables that capture several structural invariants of the execution, like well nesting of functions or the fact that every basic block must start with a code emission statement.