# Changeset 3344

Ignore:
Timestamp:
Jun 11, 2013, 10:31:46 PM (5 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r3343 \section{The labelling approach} \label{labelling} \section{A brief introduction to the labelling approach} \begin{figure} \begin{verbatim} EMIT L_1;                         EMIT L_1         cost += k_1; I_1;                              I_3              I_1; for (i=0; i<2; i++) {        l_1: COND l_2         for (i=0; i<2; i++) { EMIT L_2;                       EMIT L_2           cost += k_2; I_2;                            I_4                I_2; }                                GOTO l_1          } EMIT L_3;                    l_2: EMIT L_3         cost += k_3; \end{verbatim} \caption{The labelling approach applied to a simple program.\label{examplewhile}. The $I_i$ are sequences of instructions not containing jumps or loops. } \end{figure} We briefly explain the labelling approach on the example in Figure~\ref{examplewhile}. The user wants to analyse the execution time of the program made by the black lines in the r.h.s. of the figure. He compiles the program using a special compiler that first inserts in the code three label emission statements (\texttt{EMIT L$_i$}, in red) to mark the beginning of basic blocks; then the compiler compiles the code to machine code (in the middle of the figure), granting that the execution of the source and object code emits the same sequence of labels ($L_1; L_2; L_2; L_3$ in the example). This is achieved by keeping track of basic blocks during compilation, avoiding all optimizations that alter the control flow. The latter can be recovered with a more refined version of the labelling approach~\cite{tranquill}, but in the present paper we stick to this simple variant for simplicity. Once the object code is produced, the compiler runs a static code analyzer to associate to each label $L_1, \ldots, L_3$ the cost (in clock cycles) of the instructions that belong to the corresponding basic block. For example, the cost $k_1$ associated to $L_1$ is the number of cycles required to execute the block $I_3$ and $COND l_2$, while the cost $k_2$ associated to $L_2$ counts the cycles required by the block $I_4$ and $GOTO l_1$. The compiler also guarantees that every executed instruction is in the scope of some code emission label, that each scope does not contain loops (to associate a finite cost), and that both branches of a conditional statement are followed by a code emission statement. Under these assumptions it is true that the total execution cost of the program $\Delta_t$ is equal to the sum over the sequence of emitted labels of the cost associated to every label: $\Delta t = k(L_1; L_2; L_2; L_3) = k_1 + k_2 + k_2 + k_3$. Finally, the compiler emits an instrumented version of the source code (in the r.h.s. of the figure) where label emission statements are replaced by increments of a global variable cost that, before every increment, holds the exact number of clock cycles spent by the microprocessor so far: the difference $\Delta clock$ between the final and initial value of the variable clock is $\Delta clock = k_1 + k_2 + k_2 + k_3 = \Delta t$. Finally, the user can employ any available method (e.g. Hoare logic, invariant generators, abstract interpretation and automated provers) to certify that $\Delta clock$ never exceeds a certain bound~\cite{cerco}, which is now a functional property of the code. \section{The labelling approach in presence of loops} Let's now consider a simple program written in C that contains a function pointer call inside the scope of the cost label $L_1$. \begin{verbatim} main: EMIT L_1       g: EMIT L_3   EMIT L_1     g: EMIT L_3 I_1;              I_3;       I_4;            I_6; (*f)();           return;    CALL            RETURN I_2;                         I_5; EMIT L_2                     EMIT L_2 \end{verbatim} The labelling method works exactly as before, inserting code emission statements/\texttt{cost} variable increments at the beginning of every basic block and at the beginning of every function. The compiler still grants that the sequence of labels observed on the two programs are the same. A new difficulty happears when the compiler needs to statically analyze the object code to assign a cost to every label. What should the scope of the $L_1$ label be? After executing the $I_4$ block, the \texttt{CALL} statement passes control to a function that cannot be determined statically. Therefore the cost of executing the body must be paid by some other label (hence the requirement that every function starts with a code emission statement). What label should pay for the cost for the block $I_5$? The only reasonable answer is $L_1$, i.e. \emph{the scope of labels should extend to the next label emission statement, stepping over function calls}. The latter definition of scope is adeguate on the source level because C is a structured language that guarantees that every function call, if it returns, passes control to the first instruction that follows the call. However, this is not guaranteed for object code, the backend languages of a compiler and, more generally, for unstructured languages that use a writable control stack to store the return address of calls. For example, $I_6$ could increment by $1$ the return address on the stack so that the next \texttt{RETURN} would start at the second instruction of $I_5$. The compiler would still be perfectly correct if a random, dead code instruction was also added just after each \texttt{CALL}. More generally, \emph{there is no guarantee that a correct compiler that respects the functional behaviour of a program also respects the calling structure of the source code}. Without such an assumption, however, it may not be true that the execution cost of the program is the sum of the costs associated to the labels emitted. In our example, the cost of $I_5$ is paid by $L_1$, but in place of $I_5$ the processor could execute any other code after $g$ returns. Obviously, any reasonably written compiler produces object code that behaves as if the language was structured (i.e. by properly nesting function calls/returns and without tampering with the return addresses on the control stack). This property, however, is a property of the runs of object code programs, and not a property of the object code that can be easily statically verified (as the ones we required for the basic labelling method). Therefore, we now need to single out those runs whose cost behaviour can be statically predicted, and we need to prove that every run of programs generated by our compiler are of that type. We call them \emph{structured} since their main property is to respect properties that hold for free on the source code because the source language is structured. Moreover, in order to avoid proving too many preservation properties of our compiler, we drop the original requirements on the object code (all instructons must be in scope of some labels, no loops inside a scope, etc.) in favour of the corresponding requirement for structured runs (a structured run must start with a label emission, no instruction can be executed twice between two emissions, etc.). 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 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 observed; 3) we give unstructured languages a semantics in terms of structured traces; 4) we show that on the source code we can correctly compute the execution time of a program if the compiler produces object code whose runs are weakly similar to the source code runs. The notion of weak bisimulation for structured traces is a global property which is hard to prove formally and much more demanding than the simple forward simulation required for proofs of preservation of functional properties. Therefore in Section~\ref{XXX} we will present a set of local simulation conditions that refine the corresponding conditions for forward simulation and that are sufficient to grant the production of weakly similar traces. All the definitions and theorems presented in the paper have been formalized 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 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 simplification effort for 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. However the formalization is heavily commented to allow the reader to understand the technical details of the formalization. ==================================================== We briefly sketch here a simplified version of the labelling approach as introduced in~\cite{easylabelling}. The simplification strengthens the