# Changeset 3367 for Papers/itp-2013

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

...

File:
1 edited

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

 r3366 The statement of the generic proof is based on a new semantics for imperative unstructured languages that is based on \emph{structured traces} and that restores the preservation of structure in the observables of execution fragments} and that restores the preservation of structure in the observables of the semantics. The generic proof allows to almost completely split the part of the simulation that deals with functional properties only from the to languages with function calls. In Section~\ref{sec:semantics} we introduce a generic description of an unstructured imperative language and the corresponding structured traces (the novel semantics). In corresponding structured fragments (the novel semantics). In Section~\ref{sec:simulation} we describe the forward simulation proof. Conclusions and future works are in Section~\ref{sec:conclusions} We will therefore proceed as follows. In the following section 1) we formally introduce the notion of structured trace, which captures structured runs in the style of labelled structured execution fragment, which captures structured runs in the style of labelled transition systems; 2) we show that on the object code we can correctly compute the execution time of a structured run from the sequence of labels in the interactive theorem prover Matita and are being used to certify the complexity preserving compiler developed in the CerCo project~\cite{cerco}. The formalization can be found at~\ref{YYY} and it heavily relies on algebraic and dependent types for both structured traces and the definition of weak similarity. In the paper The formalization heavily relies on algebraic and dependent types. In the first part of the paper we did not try to stay close to the formalization. On the contrary, the definitions given in the paper are the result of a significant the sake of presentation and to make easier the re-implementation of the concepts in a proof assistant which is not based on the Calculus of Inductive Constructions. In any case the formalization is heavily commented to allow the Constructions. In any case the formalization, briefly presented at the end of the paper, is heavily commented to allow the reader to understand the technical details of the formalization. % in the semantics. This is the topic of the next section. \subsection{Structured traces} \subsection{Structured execution fragments} \label{sec:semantics} of a server implemented as an unbounded loop whose body waits for an input, process it and performs an output before looping: the processing steps form a structured execution fragment. steps form a structured fragment. \item The number of $RET$'s in the fragment is equal to the number of calls performed. In combination with the previous condition, this ensures well-backeting of function calls. well-bracketing of function calls. \item \label{req3} \begin{theorem} \label{thm:static} for all measurable fragment $T = s_0 \to^{*} s_n$,\\ 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)$$ \end{theorem} A compiler (pass) that preserves the program semantics also preserves weak traces and propagates measurability iff for every measurable fragment $T_1 = s_1 \to^{*} s_1'$ of the source code, the corresponding execution fragment $T_2 = s_2 \to^{*} s_2'$ of the object code is measurable and $T_1$ and $T_2$ are weakly trace equivalent. The very intuitive notion of 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 and $M_1$ and $M_2$ are weakly trace equivalent. The very intuitive notion of corresponding fragment'' is made clear in the forward simulation proof of preservation of the semantics of the program by saying that $s_2$ and $s_1$ the two resulting states are synchronized again according to the relation. No requirements are imposed on the intermediate target states. Finally, the lemma is iterated over the execution trace to establish the Finally, the lemma is iterated over the execution fragment to establish the final result. preserving translation of every instruction. In order to produce structured traces, however, code emission cannot be fully compositional any longer, and requirements need to be enforced on intermediate target states. and requirements need to be enforced on intermediate target states too. For example, consider~requirement \ref{req3} that asks every function body need to translate a function call to a function call followed by some instructions (for example to restore caller-saved registers in the pass that sets the parameter convenction). In the forward simulation proof, these sets the parameter convention). In the forward simulation proof, these instructions are taken care of when simulating the \texttt{RETURN} step: the state just after the return in the source code is matched by the state $s_2$ \end{definition} We will require all pairs of states that return from related calls to be $\R$-related. This, in combinantion with a dual requirement on function calls, $\R$-related. This, in combination with a dual requirement on function calls, will grant that calls return exactly where they are supposed to be. On the other hand the $\LS$ relation captures the fact that synchronisation on labels can be decoupled from content of our results departing from the actual Matita formalisation. In this section we explain the basis of the Matita development, heavily based on inductive definitions and dependent types. inductive definitions and dependent types. The development consists of 3369 lines of code and can be downloaded from \begin{center}\url{http://cerco.cs.unibo.it/attachment/wiki/WikiStart/CPP2013.tar.gz}\end{center} \paragraph*{The main differences.} The main points where the development diverges \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} a matter of structural induction, when it would require more complex induction schemes the conditions. Among other things this turns the proof of \autoref{thm:preservation} into a matter of structural induction, when it would require additional lemmas otherwise. \item As we are dealing with a deterministic labelling transition system, we purposedly blur the distinction between labelling the transitions and labelling purposely blur the distinction between labelling the transitions and labelling the states originating them, and opt in general for the latter in the actual definitions. \item ................. ALTRO? \item As object code cannot have a separate emission instruction, we allow any instruction to be labelled, which implies that labels can be emitted alongside other observable events. \item A small difference lies in the naming conventions. In this paper we went with the tradition of labelled transition systems and named sequences of states Finally, we identified measurable execution fragments that are those whose execution time (once compiled) can be exactly computed looking at the object code weak execution traces only. A final instrumentation pass on the source execution time (once compiled) can be exactly computed looking only at the weak execution traces of the object code. A final instrumentation pass on the source code can then be used to turn the non functional property of having a certain cost into the functional property of granting that a certain global variable cost into the functional property that a certain global variable incremented at the beginning of every block according to the induced cost model has a certain value. the CerCo compiler exploiting the main theorem of this paper. An alternative approach to the same problem that we would like to investigate consists in labelling every instruction that follows a call. This would still require a form of structured execution fragments, stating that no only calls but also returns are always followed by an emission. The main downside is the pollution of the instrumented code every instruction that follows a call. This would reduce the requirements of the proofs, with % This would still require a form of structured % execution fragments, stating that both returns and calls are always followed % by a label emission. the downside of polluting the instrumented code with many cost annotations.
Note: See TracChangeset for help on using the changeset viewer.