Changeset 3356


Ignore:
Timestamp:
Jun 14, 2013, 4:21:50 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Papers/itp-2013/ccexec2.tex

    r3355 r3356  
    238238\label{labelling}
    239239% \subsection{A brief introduction to the labelling approach}
    240 We briefly explain the labelling approach on the example in \autoref{examplewhile}.
     240We briefly explain the labelling approach as introduced in~\cite{easylabelling}
     241on the example in \autoref{examplewhile}.
    241242The user wants to analyse the execution time of the program (the black lines in
    242243\autoref{subfig:example_input}). He compiles the program using
    243244a special compiler that first inserts in the code three label emission
    244 statements (\verb+EMIT L_i+) to mark the beginning of basic blocks;
     245statements (\verb+EMIT L_i+) to mark the beginning of basic blocks
     246(\autoref{subfig:example_input});
    245247then the compiler compiles the code to machine code (\autoref{subfig:example_oc}),
    246248granting that the execution of the source and object
    … …  
    248250This is achieved by keeping track of basic blocks during compilation, avoiding
    249251all optimizations that alter the control flow. The latter can be recovered with
    250 a more refined version of the labelling approach~\cite{tranquill}, but in the
     252a more refined version of the labelling approach~\cite{loopoptimizations}, but in the
    251253present paper we stick to this simple variant for simplicity. Once the object
    252254code is produced, the compiler runs a static code analyzer to associate to
    … …  
    273275never exceeds a certain bound~\cite{cerco}, which is now a functional property
    274276of the code.
    275 \begin{figure}
     277
     278\vspace{-0.5cm}
     279\begin{figure}[!h]
    276280\begin{subfigure}[t]{.32\linewidth}
    277281\begin{lstlisting}[moredelim={[is][\color{red}]{|}{|}}]
    … …  
    327331\end{figure}
    328332
    329 \subsection{The labelling approach in presence of calls}
     333\section{Extending the labelling approach to function calls}
    330334%
    331335Let's now consider a simple program written in C that contains a function
    … …  
    351355\begin{lstlisting}[xleftmargin=20pt]
    352356void main() {
    353   EMIT L_1;
     357  EMIT $L_1$;
    354358  $I_1$;
    355359  (*f)();
    356360  $I_2$;
    357361}
     362
    358363void g() {
    359   EMIT L_2;
     364  EMIT $L_2$;
    360365  $I_3$;
    361366}
    … …  
    369374\begin{lstlisting}[xleftmargin=20pt]
    370375main:
    371   EMIT L_1
     376  EMIT $L_1$
    372377  $I_4$
    373378  CALL
    374379  $I_5$
    375380  RETURN
     381
    376382g:
    377   EMIT L_2
     383  EMIT $L_2$
    378384  $I_6$
    379385  RETURN
    … …  
    397403stack so that the next \verb+RETURN+ would start at the second instruction
    398404of $I_5$. The compiler would still be perfectly correct if a random, dead
    399 code instruction was also added just after each \verb+CALL+. More generally,
     405code instruction was added after the \verb+CALL+ as the first instruction of $I_5$. More generally,
    400406\emph{there is no guarantee that a correct compiler that respects the functional
    401407behaviour of a program also respects the calling structure of the source code}.
    … …  
    409415stack). This property, however, is a property of the runs of object code
    410416programs, and not a property of the object code that can be easily statically
    411 verified (as the ones we required for the basic labelling method).
     417verified (as the ones required in \autoref{labelling} in absence of function calls).
    412418Therefore, we now need to single out those runs whose cost behaviour can be
    413419statically predicted, and we need to prove that every run of programs generated
    … …  
    426432transition systems; 2) we show that on the object code we can correctly
    427433compute the execution time of a structured run from the sequence of labels
    428 observed; 3) we give unstructured languages a semantics in terms of structured
    429 traces; 4) we show that on the source code we can correctly compute the
     434observed; 3) we show that on the source code we can correctly compute the
    430435execution time of a program if the compiler produces object code whose
    431 runs are weakly similar to the source code runs.
    432 
    433 The notion of weak simulation for structured traces is a global property
    434 which is hard to prove formally and much more demanding than the simple forward
    435 simulation required for proofs of preservation of functional properties.
    436 Therefore in \autoref{simulation} we will present a set of local simulation
    437 conditions that refine the corresponding conditions for forward simulation and
    438 that are sufficient to grant the production of weakly similar traces.
     436runs are weakly similar to the source code runs and structured.
     437
     438The proof of correctness of such a compiler is harder than a traditional
     439proof of preservation of functional properties, and a standard forward
     440simulation argument does not work. In \autoref{simulation} we present
     441a refinement of forward simulation that grants all required correctness
     442properties.
    439443
    440444All the definitions and theorems presented in the paper have been formalized
    … …  
    688692% in the semantics. This is the topic of the next section.
    689693
    690 \section{Structured traces}
     694\subsection{Structured traces}
    691695\label{semantics}
    692696
    … …  
    695699deterministic labelled transition system~\cite{LTS} $(S,\Lambda,\to)$
    696700that refines the
    697 SOS by observing function calls and the beginning of basic blocks.
     701SOS by observing function calls/returns and the beginning of basic blocks.
    698702$S$ is the set of states of the program and
    699703$\Lambda = \{ \tau, RET \} \cup \Labels \cup \Functions$
    … …  
    771775cases when the fragment starts at the beginning of a function body
    772776(e.g. the one of \texttt{main}) because in that case nobody would have emitted
    773 the observable $\ell(f)$.
     777the observable $\ell(f)$. We plan to compare the two approaches in the future.
    774778
    775779\paragraph{Measurable execution fragments and their cost prediction.}
    776 The first main theorem of CerCo deals with programs written in object code.
     780The first main theorem of CerCo deals with the object code.
    777781It states that the execution cost of
    778782certain execution fragments, that we call \emph{measurable fragments}, can be
    … …  
    799803$s_0 \To s_n$ and $s_n$ must be a label emission statement.
    800804
    801 \textbf{CSC: PROVA----------------------}
     805%\textbf{CSC: PROVA----------------------}
    802806% The theorem is proved by structural induction over the structured
    803807% trace, and is based on the invariant that
    … …  
    832836accurate for the object code, we get as a corollary that it is also accurate
    833837for the source code if the compiler preserves weak traces and
    834 propagates measurability. Thus it becomes possible to compute cost models
     838propagates measurability. Thus, as prescribed by the CerCo's methodology~\cite{fopara}, it becomes possible to compute cost models
    835839on the object code, transfer it to the source code and then reason comfortably
    836840on the source code only.
    … …  
    845849\end{theorem}
    846850
    847 \section{Forward simulation}
     851\section{Proving the compiler correctness}
    848852\label{simulation}
    849853Because of \autoref{preservation}, to certify a compiler for the labelling
    850854approach we need to both prove that it respects the functional semantics of the
    851855program, and that it preserves weak traces and propagates measurability.
     856We achieve this by independently proving the three properties for each compiler
     857pass.
    852858The first property is standard and can be proved by means of a forward simulation argument (see for example~\cite{compcert}) that runs like this.
    853859First a relation between the corresponding
    854 source and target states is established. Then a lemma establishes
     860source and target states is defined. Then a lemma establishes
    855861a local simulation condition: given two states in relation, if the source
    856862one performs one step then the target one performs zero or more steps and
    857863the two resulting states are synchronized again according to the relation.
     864No requirements are imposed on the intermediate target states.
    858865Finally, the lemma is iterated over the execution trace to establish the
    859866final result.
    … …  
    865872kind of local or global analysis of the code followed by a compositional, order
    866873preserving translation of every instruction. In order to produce structured
    867 traces, however, code emission cannot be fully compositional any longer.
     874traces, however, code emission cannot be fully compositional any longer,
     875and requirements need to be enforced on intermediate target states.
    868876
    869877For example, consider~requirement \ref{req3} that asks every function body
    … …  
    886894the state just after the return in the source code is matched by the state $s_2$
    887895after these steps in the object code. However, the aforementioned requirement
    888 does not involve $s_2$, but the state reached after the return in the object
    889 code, that preceeds $s_2$ in the execution fragment. Therefore the requirement
     896does not involve $s_2$, but the intermediate state reached after the return in the object
     897code. Therefore this requirement too
    890898cannot be enforced with the standard forward simulation argument.
    891899
    … …  
    13641372% an equivalence relation.
    13651373
    1366 \textbf{----------------------------}
    1367 
    1368 We summarise here the results of the previous sections. Each intermediate
    1369 unstructured language can be given a semantics based on structured traces,
    1370 that single out those runs that respect a certain number of invariants.
    1371 A cost model can be computed on the object code and it can be used to predict
    1372 the execution costs of runs that produce structured traces. The cost model
    1373 can be lifted from the target to the source code of a pass if the pass maps
    1374 structured traces to similar structured traces. The latter property is called
    1375 a \emph{forward simulation}.
    1376 
    1377 As for labelled transition systems, in order to establish the forward
    1378 simulation we are interested in (preservation of observables), we are
    1379 forced to prove a stronger notion of forward simulation that introduces
    1380 an explicit relation between states. The classical notion of a 1-to-many
    1381 forward simulation is the existence of a relation $\S$ over states such that
    1382 if $s_1 \S s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
    1383 $s_2 \to^* s_2'$ and $s_1' \S s_2'$. In our context, we need to replace the
    1384 one and multi step transition relations $\to^n$ with the existence of
    1385 a structured trace between the two states, and we need to add the request that
    1386 the two structured traces are similar. Thus what we would like to state is
    1387 something like:\\
    1388 for all $s_1,s_2,s_1'$ such that there is a $\tau_1$ from
    1389 $s_1$ to $s_1'$ and $s_1 \S s_2$ there exists an $s_2'$ such that
    1390 $s_1' \S s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
    1391 $\tau_1$ is similar to $\tau_2$. We call this particular form of forward
    1392 simulation \emph{trace reconstruction}.
    1393 
    1394 The statement just introduced, however, is too simplistic and not provable
    1395 in the general case. To understand why, consider the case of a function call
    1396 and the pass that fixes the parameter passing conventions. A function
    1397 call in the source code takes in input an arbitrary number of pseudo-registers (the actual parameters to pass) and returns an arbitrary number of pseudo-registers (where the result is stored). A function call in the target language has no
    1398 input nor output parameters. The pass must add explicit code before and after
    1399 the function call to move the pseudo-registers content from/to the hardware
    1400 registers or the stack in order to implement the parameter passing strategy.
    1401 Similarly, each function body must be augmented with a preamble and a postamble
    1402 to complete/initiate the parameter passing strategy for the call/return phase.
    1403 Therefore what used to be a call followed by the next instruction to execute
    1404 after the function return, now becomes a sequence of instructions, followed by
    1405 a call, followed by another sequence. The two states at the beginning of the
    1406 first sequence and at the end of the second sequence are in relation with
    1407 the status before/after the call in the source code, like in an usual forward
    1408 simulation. How can we prove however the additional condition for function calls
    1409 that asks that when the function returns the instruction immediately after the
    1410 function call is called? To grant this invariant, there must be another relation
    1411 between the address of the function call in the source and in the target code.
    1412 This additional relation is to be used in particular to relate the two stacks.
    1413 
    1414 Another example is given by preservation of code emission statements. A single
    1415 code emission instruction can be simulated by a sequence of steps, followed
    1416 by a code emission, followed by another sequence. Clearly the initial and final
    1417 statuses of the sequence are to be in relation with the status before/after the
    1418 code emission in the source code. In order to preserve the structured traces
    1419 invariants, however, we must consider a second relation between states that
    1420 traces the preservation of the code emission statement.
     1374@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
    14211375
    14221376Therefore we now introduce an abstract notion of relation set between abstract
    … …  
    14411395Therefore we have successfully splitted as much as possible the proof of
    14421396preservation of functional properties from that of non-functional ones.
    1443 Secondly, combined with the results in the previous section, it implies
    1444 that the cost model can be computed on the object code and lifted to the
    1445 source code to reason on non-functional properties, assuming that
    1446 the 1-to-many forward simulation conditions are fulfilled for every
    1447 compiler pass.
     1397
     1398@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
    14481399
    14491400\paragraph{Relation sets.}
    1450 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
    14511401Let $S_1$ and $S_2$ be two deterministic labelled transition systems as described
    14521402in \autoref{semantics}. We introduce now the four relations $\mathcal{S,C,R,L}\subseteq S_1\times S_2$
    … …  
    14681418Two states
    14691419$s_1$ and $s_2$ are $\R$-related if every time $s_1$ is the
    1470 successor of a call state that is $\C$-related to a call state
     1420successor of a call state $s_1'$ that is $\C$-related to a call state
    14711421$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally:
    14721422$$s_1\R s_2 \iffdef \forall s_1',s_2'.s_1'\C s_2' \to s_1'\ar s_1 \to s_2' \ar s_2.$$
    14731423We will require all pairs of states that return from related calls to be
    1474 $\R$-related. This is the fundamental requirement granting
    1475 that the target trace is well structured, \emph{i.e.}\ that calls are well
    1476 nested and returning where they are supposed to.
     1424$\R$-related. This, in combinantion with a dual requirement on function calls,
     1425will grant that calls return exactly where they are supposed to be.
    14771426
    14781427We say states in $s_1\in S_1$ and $s_2\in S_2$ are label-related
    … …  
    14851434\end{itemize}
    14861435
    1487 The results that follow all rely on common hypotheses to hold for the
    1488 systems $S_1$ and $S_2$ endowed with the relations $\S$ and $\C$. These hypotheses
    1489 are depicted by the diagrams in \autoref{fig:forwardsim}.
     1436Given the relations $\S$ and $\C$, \autoref{fig:forwardsim} defines a set of
     1437local simulation conditions that are sufficient to grant the correctness of
     1438the compiler.
     1439
    14901440\begin{figure}
    14911441\centering
    … …  
    15931543    \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
    15941544\end{tikzpicture}
    1595 \caption{The hypotheses of ???. Dashed relations are implied by solid ones.}
     1545\caption{Local simulation conditions. Each one states that the existence of
     1546states in~XXX such that the dashed relations holds is implied by the assumptions
     1547drawn as solid lines.}
    15961548\label{fig:forwardsim}
    15971549\end{figure}
    15981550
    15991551\begin{lemma}
    1600 If $S_1$, $S_2$,$\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
    1601 $T_1:s_1\To s_1'$ is a structured fragment not starting with a $\ell(f)$ emission,
    1602 and $s_1\S s_2$, then there is $T_2:s_2\To s_2'$ with $T\approx T'$ and $s_1'\S s_2$.
     1552If $S_1,S_2,\S,\C$ satisfy the diagrams in \autoref{fig:forwardsim},
     1553$T_1=s_1\To s_1'$ is a structured fragment not starting with a $\ell(f)$ emission,
     1554and $s_1\S s_2$, then there is $T_2=s_2\To s_2'$ with $T\approx T'$ and $s_1'\S s_2'$.
    16031555\end{lemma}
    16041556\begin{theorem}
    1605 If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
    1606 $M_1:s_1\MeasTo s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that
    1607 $s_1\L s_2$, then there is $M_2:s_2\MeasTo s_2'$ with $M_1\approx M_2$.
     1557If $S_1,S_2,\S,\C$ satisfy the diagrams in \autoref{fig:forwardsim},
     1558$M_1:s_1\to^{*} s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that
     1559$s_1\L s_2$, then there is $M_2:s_2\to^{*} s_2'$ with $M_1\approx M_2$.
    16081560\end{theorem}
    16091561@@@@@@@@@@@@@@@@@@@@@@@
    … …  
    20061958can be computed precisely on the source.
    20071959
    2008 In this paper we scale the labelling approach to cover a programming language
    2009 with function calls. This introduces new difficulties only when the language
     1960In this paper we scaled the labelling approach to cover a programming language
     1961with function calls. This introduces new difficulties when the language
    20101962is unstructured, i.e. it allows function calls to return anywhere in the code,
    20111963destroying the hope of a static prediction of the cost of basic blocks.
    2012 We restore static predictability by introducing a new semantics for unstructured
     1964We restored static predictability by introducing a new semantics for unstructured
    20131965programs that single outs well structured executions. The latter are represented
    20141966by structured traces, a generalisation of streams of observables that capture
    20151967several structural invariants of the execution, like well nesting of functions
    20161968or the fact that every basic block must start with a code emission statement.
    2017 We show that structured traces are sufficiently structured to statically compute
    2018 a precise cost model on the object code.
    2019 
    2020 We introduce a similarity relation on structured traces that must hold between
    2021 source and target traces. When the relation holds for every program, we prove
    2022 that the cost model can be lifted from the object to the source code.
    2023 
    2024 In order to prove that similarity holds, we present a generic proof of forward
    2025 simulation that is aimed at pulling apart as much as possible the part of the
    2026 simulation related to non-functional properties (preservation of structure)
    2027 from that related to functional properties. In particular, we reduce the
    2028 problem of preservation of structure to that of showing a 1-to-many
    2029 forward simulation that only adds a few additional proof obligations to those
    2030 of a traditional, function properties only, proof.
     1969We showed that structured traces are sufficiently well behaved to statically compute a precise cost model on the object code.
     1970
     1971We also proved that the cost model computed on the object code is also valid
     1972on the source code if the compiler respects two requirements: the weak execution
     1973traces of the source and target code must be the same and the object
     1974code execution fragments are structured.
     1975
     1976To prove that a compiler respects the requirement we extended the notion
     1977of forward simulation proof for a labelled transition system to grant
     1978preservation of structured fragments. If the source language of the compiler
     1979is structured, all its execution fragments are, allowing to deduce from
     1980preservation of structure that object code fragments are structured too.
     1981
     1982Finally, we identified measurable execution fragments that are those whose
     1983execution time (once compiled) can be exactly computed looking at the object
     1984code weak execution traces only. A final instrumentation pass on the source
     1985code can then be used to turn the non functional property of having a certain
     1986cost into the functional property of granting that a certain global variable
     1987incremented at the beginning of every block according to the induced cost model
     1988has a certain value.
    20311989
    20321990All results presented in the paper are part of a larger certification of a
    … …  
    20562014insensible to the resource being measured. Indeed, any cost model computed on
    20572015the object code can be lifted to the source code (e.g. stack space used,
    2058 energy consumed, etc.). On the contrary, clock functions only talk about
     2016energy consumed, etc.) simply re-proving an analogue of~\autoref{static}.
     2017For example, in CerCo we transported to the source level not only the execution
     2018time cost model, but also the amount of stack used by function calls.
     2019On the contrary, clock functions only talk about
    20592020number of transition steps. In order to extend the approach with clock functions
    20602021to other resources, additional functions must be introduced. Moreover, the
Note: See TracChangeset for help on using the changeset viewer.