Changeset 3211 for Deliverables/D3.4/Report/report.tex
 Timestamp:
 Apr 29, 2013, 5:24:37 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.4/Report/report.tex
r3203 r3211 504 504 these passes. 505 505 506 TODO: both give onestepsimbymany 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 508 The intermediate languages of the frontend have no jump tables. 509 Hence, we have to compile the \lstinline[language=C]'switch' 510 constructs away before going from \textsf{Clight} to \textsf{Cminor}. 511 Note that this transformation does not necessarily deteriorate the 512 efficiency of the generated code. For instance, compilers such as GCC 513 introduce balanced trees of ``ifthenelse'' constructs for small 514 switches. However, our implementation strategy is much simpler. Let 515 us 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 528 Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default} 529 may contain \lstinline[language=C]'break' statements, which have the 530 effect of exiting the switch statement. In the absence of break, the 531 execution falls through each case sequentially. In our current implementation, 532 we produce an equivalent sequence of ``ifthen'' 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 548 The 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 nonlocal way (e.g. \textbf{goto} 552 instead of \textbf{break}). 553 \end{itemize} 554 555 In order to tackle the first point, we implemented a version of memory 556 extensions similar to Compcert's. What has been done is the simulation proof 557 for all ``easy'' cases, that do not interact with the switch removal per se, 558 plus a bit of the switch case. This comprises propagating the memory extension 559 through each statement (except switch), as well as various invariants that 560 are needed for the switch case (in particular, freshness hypotheses). The 561 details of the evaluation process for the source switch statement and its 562 target counterpart can be found in the file \textbf{switchRemoval.ma}, 563 along more details on the transformation itself. 564 565 Proving the correctness of the second point would require reasoning on the 566 semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight} 567 semantics, this is implemented as a functionwide lookup of the target label. 568 The invariant we would need is the fact that a global label lookup on a freshly 569 created goto is equivalent to a local lookup. This would in turn require the 570 propagation of some freshness hypotheses on labels. For reasons expressed above, 571 we decided to omit this part of the correctness proof. 572 573 \subsection{Cost labelling} 574 575 The simulation for the cost labelling pass is the simplest in the 576 frontend. The main argument is that any step of the source program 577 is simulated by the same step of the labelled one, plus any extra 578 steps for the added cost labels. The extra instructions do not change 579 the memory or local environments, although we have to keep track of 580 the extra instructions in continuations. 581 582 We do not attempt to capture any cost properties of the labelling in 583 the simulation proof, allowing the proof to be oblivious to the choice 584 of cost labels. Hence we do not have to reason about the threading of 585 name generation through the labelling function, greatly reducing the 586 amount of effort required. We describe how the cost properties are 587 established in Section~\ref{sec:costchecks}. 588 589 %TODO: both give onestepsimbymany 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). 513 596 514 597 \section{Finding corresponding measurable subtraces} … … 649 732 \subsection{Simulation results for each pass} 650 733 651 \todo{don't use loop structures from CompCert, go straight to jumps}652 653 734 \paragraph{Cast simplification.} 654 735 … … 720 801 both the implementation and the proof. 721 802 \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 frontend 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 the729 efficiency of the generated code. For instance, compilers such as GCC730 introduce balanced trees of ``ifthenelse'' constructs for small731 switches. However, our implementation strategy is much simpler. Let732 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 the747 effect of exiting the switch statement. In the absence of break, the748 execution falls through each case sequentially. In our current implementation,749 we produce an equivalent sequence of ``ifthen'' 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 nonlocal 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 memory773 extensions similar to Compcert's. What has been done is the simulation proof774 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 extension776 through each statement (except switch), as well as various invariants that777 are needed for the switch case (in particular, freshness hypotheses). The778 details of the evaluation process for the source switch statement and its779 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 the783 semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight}784 semantics, this is implemented as a functionwide lookup of the target label.785 The invariant we would need is the fact that a global label lookup on a freshly786 created goto is equivalent to a local lookup. This would in turn require the787 propagation of some freshness hypotheses on labels. For reasons expressed above,788 we decided to omit this part of the correctness proof.789 803 790 804 \paragraph{Clight to Cminor.}
Note: See TracChangeset
for help on using the changeset viewer.