Changeset 3211


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3203 r3211  
    504504these passes.
    505505
    506 TODO: both give one-step-sim-by-many forward sim results; switch
    507 removal tricky, uses aux var to keep result of expr, not central to
    508 intensional correctness so curtailed proof effort once reasonable
    509 level of confidence in code gained; labelling much simpler; don't care
    510 what the labels are at this stage, just need to know when to go
    511 through extra steps.  Rolled up into a single result with a cofixpoint
    512 to obtain coinductive statement of equivalence (show).
     506\subsection{Switch removal}
     507
     508The intermediate languages of the front-end have no jump tables.
     509Hence, we have to compile the \lstinline[language=C]'switch'
     510constructs away before going from \textsf{Clight} to \textsf{Cminor}.
     511Note that this transformation does not necessarily deteriorate the
     512efficiency of the generated code. For instance, compilers such as GCC
     513introduce balanced trees of ``if-then-else'' constructs for small
     514switches. However, our implementation strategy is much simpler. Let
     515us consider the following input statement.
     516
     517\begin{lstlisting}[language=C]
     518   switch(e) {
     519   case v1:
     520     stmt1;
     521   case v2:
     522     stmt2;
     523   default:
     524     stmt_default;
     525   }
     526\end{lstlisting}
     527
     528Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default}
     529may contain \lstinline[language=C]'break' statements, which have the
     530effect of exiting the switch statement. In the absence of break, the
     531execution falls through each case sequentially. In our current implementation,
     532we produce an equivalent sequence of ``if-then'' chained by gotos:
     533\begin{lstlisting}[language=C]
     534   fresh = e;
     535   if(fresh == v1) {
     536     $\llbracket$stmt1$\rrbracket$;
     537     goto lbl_case2;
     538   };
     539   if(fresh == v2) {
     540     lbl_case2:
     541     $\llbracket$stmt2;$\rrbracket$
     542     goto lbl_case2;
     543   };
     544   $\llbracket$stmt_default$\rrbracket$;
     545   exit_label:
     546\end{lstlisting}
     547
     548The proof had to tackle the following points:
     549\begin{itemize}
     550\item the source and target memories are not the same (cf. fresh variable),
     551\item the flow of control is changed in a non-local way (e.g. \textbf{goto}
     552  instead of \textbf{break}).
     553\end{itemize}
     554
     555In order to tackle the first point, we implemented a version of memory
     556extensions similar to Compcert's. What has been done is the simulation proof
     557for all ``easy'' cases, that do not interact with the switch removal per se,
     558plus a bit of the switch case. This comprises propagating the memory extension
     559through  each statement (except switch), as well as various invariants that
     560are needed for the switch case (in particular, freshness hypotheses). The
     561details of the evaluation process for the source switch statement and its
     562target counterpart can be found in the file \textbf{switchRemoval.ma},
     563along more details on the transformation itself.
     564
     565Proving the correctness of the second point would require reasoning on the
     566semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight}
     567semantics, this is implemented as a function-wide lookup of the target label.
     568The invariant we would need is the fact that a global label lookup on a freshly
     569created goto is equivalent to a local lookup. This would in turn require the
     570propagation of some freshness hypotheses on labels. For reasons expressed above,
     571we decided to omit this part of the correctness proof.
     572
     573\subsection{Cost labelling}
     574
     575The simulation for the cost labelling pass is the simplest in the
     576front-end.  The main argument is that any step of the source program
     577is simulated by the same step of the labelled one, plus any extra
     578steps for the added cost labels.  The extra instructions do not change
     579the memory or local environments, although we have to keep track of
     580the extra instructions in continuations.
     581
     582We do not attempt to capture any cost properties of the labelling in
     583the simulation proof, allowing the proof to be oblivious to the choice
     584of cost labels.  Hence we do not have to reason about the threading of
     585name generation through the labelling function, greatly reducing the
     586amount of effort required.  We describe how the cost properties are
     587established in Section~\ref{sec:costchecks}.
     588
     589%TODO: both give one-step-sim-by-many forward sim results; switch
     590%removal tricky, uses aux var to keep result of expr, not central to
     591%intensional correctness so curtailed proof effort once reasonable
     592%level of confidence in code gained; labelling much simpler; don't care
     593%what the labels are at this stage, just need to know when to go
     594%through extra steps.  Rolled up into a single result with a cofixpoint
     595%to obtain coinductive statement of equivalence (show).
    513596
    514597\section{Finding corresponding measurable subtraces}
     
    649732\subsection{Simulation results for each pass}
    650733
    651 \todo{don't use loop structures from CompCert, go straight to jumps}
    652 
    653734\paragraph{Cast simplification.}
    654735
     
    720801both the implementation and the proof.
    721802\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language}
    722 
    723 \paragraph{Switch removal.}
    724 
    725 The intermediate languages of the front-end have no jump tables.
    726 Hence, we have to compile the \lstinline[language=C]'switch'
    727 constructs away before going from \textsf{Clight} to \textsf{Cminor}.
    728 Note that this transformation does not necessarily deteriorate the
    729 efficiency of the generated code. For instance, compilers such as GCC
    730 introduce balanced trees of ``if-then-else'' constructs for small
    731 switches. However, our implementation strategy is much simpler. Let
    732 us consider the following input statement.
    733 
    734 \begin{lstlisting}[language=C]
    735    switch(e) {
    736    case v1:
    737      stmt1;
    738    case v2:
    739      stmt2;
    740    default:
    741      stmt_default;
    742    }
    743 \end{lstlisting}
    744 
    745 Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default}
    746 may contain \lstinline[language=C]'break' statements, which have the
    747 effect of exiting the switch statement. In the absence of break, the
    748 execution falls through each case sequentially. In our current implementation,
    749 we produce an equivalent sequence of ``if-then'' chained by gotos:
    750 \begin{lstlisting}[language=C]
    751    fresh = e;
    752    if(fresh == v1) {
    753      $\llbracket$stmt1$\rrbracket$;
    754      goto lbl_case2;
    755    };
    756    if(fresh == v2) {
    757      lbl_case2:
    758      $\llbracket$stmt2;$\rrbracket$
    759      goto lbl_case2;
    760    };
    761    $\llbracket$stmt_default$\rrbracket$;
    762    exit_label:
    763 \end{lstlisting}
    764 
    765 The proof had to tackle the following points:
    766 \begin{itemize}
    767 \item the source and target memories are not the same (cf. fresh variable),
    768 \item the flow of control is changed in a non-local way (e.g. \textbf{goto}
    769   instead of \textbf{break}).
    770 \end{itemize}
    771 
    772 In order to tackle the first point, we implemented a version of memory
    773 extensions similar to Compcert's. What has been done is the simulation proof
    774 for all ``easy'' cases, that do not interact with the switch removal per se,
    775 plus a bit of the switch case. This comprises propagating the memory extension
    776 through  each statement (except switch), as well as various invariants that
    777 are needed for the switch case (in particular, freshness hypotheses). The
    778 details of the evaluation process for the source switch statement and its
    779 target counterpart can be found in the file \textbf{switchRemoval.ma},
    780 along more details on the transformation itself.
    781 
    782 Proving the correctness of the second point would require reasoning on the
    783 semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight}
    784 semantics, this is implemented as a function-wide lookup of the target label.
    785 The invariant we would need is the fact that a global label lookup on a freshly
    786 created goto is equivalent to a local lookup. This would in turn require the
    787 propagation of some freshness hypotheses on labels. For reasons expressed above,
    788 we decided to omit this part of the correctness proof.
    789803
    790804\paragraph{Clight to Cminor.}
Note: See TracChangeset for help on using the changeset viewer.