# Changeset 3211 for Deliverables

Ignore:
Timestamp:
Apr 29, 2013, 5:24:37 PM (7 years ago)
Message:

Put switch removal in correct place; describe cost labelling sim.

File:
1 edited

### Legend:

Unmodified
 r3203 these passes. TODO: both give one-step-sim-by-many forward sim results; switch removal tricky, uses aux var to keep result of expr, not central to intensional correctness so curtailed proof effort once reasonable level of confidence in code gained; labelling much simpler; don't care what the labels are at this stage, just need to know when to go through extra steps.  Rolled up into a single result with a cofixpoint to obtain coinductive statement of equivalence (show). \subsection{Switch removal} The intermediate languages of the front-end have no jump tables. Hence, we have to compile the \lstinline[language=C]'switch' constructs away before going from \textsf{Clight} to \textsf{Cminor}. Note that this transformation does not necessarily deteriorate the efficiency of the generated code. For instance, compilers such as GCC introduce balanced trees of if-then-else'' constructs for small switches. However, our implementation strategy is much simpler. Let us consider the following input statement. \begin{lstlisting}[language=C] switch(e) { case v1: stmt1; case v2: stmt2; default: stmt_default; } \end{lstlisting} Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default} may contain \lstinline[language=C]'break' statements, which have the effect of exiting the switch statement. In the absence of break, the execution falls through each case sequentially. In our current implementation, we produce an equivalent sequence of if-then'' chained by gotos: \begin{lstlisting}[language=C] fresh = e; if(fresh == v1) { $\llbracket$stmt1$\rrbracket$; goto lbl_case2; }; if(fresh == v2) { lbl_case2: $\llbracket$stmt2;$\rrbracket$ goto lbl_case2; }; $\llbracket$stmt_default$\rrbracket$; exit_label: \end{lstlisting} The proof had to tackle the following points: \begin{itemize} \item the source and target memories are not the same (cf. fresh variable), \item the flow of control is changed in a non-local way (e.g. \textbf{goto} instead of \textbf{break}). \end{itemize} In order to tackle the first point, we implemented a version of memory extensions similar to Compcert's. What has been done is the simulation proof for all easy'' cases, that do not interact with the switch removal per se, plus a bit of the switch case. This comprises propagating the memory extension through  each statement (except switch), as well as various invariants that are needed for the switch case (in particular, freshness hypotheses). The details of the evaluation process for the source switch statement and its target counterpart can be found in the file \textbf{switchRemoval.ma}, along more details on the transformation itself. Proving the correctness of the second point would require reasoning on the semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight} semantics, this is implemented as a function-wide lookup of the target label. The invariant we would need is the fact that a global label lookup on a freshly created goto is equivalent to a local lookup. This would in turn require the propagation of some freshness hypotheses on labels. For reasons expressed above, we decided to omit this part of the correctness proof. \subsection{Cost labelling} The simulation for the cost labelling pass is the simplest in the front-end.  The main argument is that any step of the source program is simulated by the same step of the labelled one, plus any extra steps for the added cost labels.  The extra instructions do not change the memory or local environments, although we have to keep track of the extra instructions in continuations. We do not attempt to capture any cost properties of the labelling in the simulation proof, allowing the proof to be oblivious to the choice of cost labels.  Hence we do not have to reason about the threading of name generation through the labelling function, greatly reducing the amount of effort required.  We describe how the cost properties are established in Section~\ref{sec:costchecks}. %TODO: both give one-step-sim-by-many forward sim results; switch %removal tricky, uses aux var to keep result of expr, not central to %intensional correctness so curtailed proof effort once reasonable %level of confidence in code gained; labelling much simpler; don't care %what the labels are at this stage, just need to know when to go %through extra steps.  Rolled up into a single result with a cofixpoint %to obtain coinductive statement of equivalence (show). \section{Finding corresponding measurable subtraces} \subsection{Simulation results for each pass} \todo{don't use loop structures from CompCert, go straight to jumps} \paragraph{Cast simplification.} both the implementation and the proof. \todo{Make this a particular case of the more general statement on baking more invariants in the Clight language} \paragraph{Switch removal.} The intermediate languages of the front-end have no jump tables. Hence, we have to compile the \lstinline[language=C]'switch' constructs away before going from \textsf{Clight} to \textsf{Cminor}. Note that this transformation does not necessarily deteriorate the efficiency of the generated code. For instance, compilers such as GCC introduce balanced trees of if-then-else'' constructs for small switches. However, our implementation strategy is much simpler. Let us consider the following input statement. \begin{lstlisting}[language=C] switch(e) { case v1: stmt1; case v2: stmt2; default: stmt_default; } \end{lstlisting} Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default} may contain \lstinline[language=C]'break' statements, which have the effect of exiting the switch statement. In the absence of break, the execution falls through each case sequentially. In our current implementation, we produce an equivalent sequence of if-then'' chained by gotos: \begin{lstlisting}[language=C] fresh = e; if(fresh == v1) { $\llbracket$stmt1$\rrbracket$; goto lbl_case2; }; if(fresh == v2) { lbl_case2: $\llbracket$stmt2;$\rrbracket$ goto lbl_case2; }; $\llbracket$stmt_default$\rrbracket$; exit_label: \end{lstlisting} The proof had to tackle the following points: \begin{itemize} \item the source and target memories are not the same (cf. fresh variable), \item the flow of control is changed in a non-local way (e.g. \textbf{goto} instead of \textbf{break}). \end{itemize} In order to tackle the first point, we implemented a version of memory extensions similar to Compcert's. What has been done is the simulation proof for all easy'' cases, that do not interact with the switch removal per se, plus a bit of the switch case. This comprises propagating the memory extension through  each statement (except switch), as well as various invariants that are needed for the switch case (in particular, freshness hypotheses). The details of the evaluation process for the source switch statement and its target counterpart can be found in the file \textbf{switchRemoval.ma}, along more details on the transformation itself. Proving the correctness of the second point would require reasoning on the semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight} semantics, this is implemented as a function-wide lookup of the target label. The invariant we would need is the fact that a global label lookup on a freshly created goto is equivalent to a local lookup. This would in turn require the propagation of some freshness hypotheses on labels. For reasons expressed above, we decided to omit this part of the correctness proof. \paragraph{Clight to Cminor.}