Changeset 1786 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 27, 2012, 6:40:46 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1785 r1786 468 468 \label{subsect.rtlabs.rtl.translation} 469 469 470 \subsubsection*{Translation of values and memory} 471 470 472 The RTLabs to RTL translation pass marks the frontier between the two memory models used in the CerCo project. 471 473 As a result, we require some method of translating between the values that the two memory models permit. … … 559 561 property of $\sigma$ to be proved. 560 562 563 \subsubsection*{Translation of RTLabs states} 561 564 RTLabs states come in three flavours: 562 565 \begin{displaymath} … … 637 640 \end{figure} 638 641 642 \subsubsection*{The forward simulation proof} 639 643 The forward simulation proof for all steps that do not involve function calls are lengthy, but routine. 640 644 They consist of simulating a frontend operation on frontend pseudoregisters and the frontend memory with sequences of backend operations on the backend pseudoregisters and backend memory. … … 644 648 We sketch here what happens on the source code and on its translation. 645 649 650 \subparagraph{Function call/return in RTLabs} 651 646 652 \begin{displaymath} 647 653 \begin{array}{rcl} 648 \mathtt{Call(id,\ args,\ dst,\ pc) ,\State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\649 & & \mathtt{PUSH(Frame[ PC:= after\_return])}654 \mathtt{Call(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\ 655 & & \mathtt{PUSH(Frame[pc := after\_return])} 650 656 \end{array} 651 657 \end{displaymath} … … 659 665 \begin{array}{rcl} 660 666 \mathtt{Call(M(args), dst)}, & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\ 661 \mathtt{PUSH(current\_frame[ PC:= after\_return])} & &667 \mathtt{PUSH(current\_frame[pc := after\_return])} & & 662 668 \end{array} 663 669 \end{displaymath} … … 674 680 \begin{displaymath} 675 681 \begin{array}{rcl} 676 \mathtt{Call(M(args), dst)} & \longrightarrow & \mathtt{ SP= alloc,\ regs = \emptyset[ := params]} \\677 \mathtt{PUSH(current\_frame[ PC:= after\_return])} & & \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)}682 \mathtt{Call(M(args), dst)} & \longrightarrow & \mathtt{sp = alloc,\ regs = \emptyset[ := params]} \\ 683 \mathtt{PUSH(current\_frame[pc := after\_return])} & & \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)} 678 684 \end{array} 679 685 \end{displaymath} 680 Here, execution of the \texttt{Call} state first pushes the current frame with the program counter set to the address following the function call. 681 The stack pointer allocates more space, the register map is initialized first to the empty map, assigning an undefined value to all register, before the value of the parameters is inserted into the map into the argument registers, and a new \texttt{State} follows. 682 After this, the stack pointer is freed and a \texttt{Return} state is entered: 686 A new stack frame is allocated and its address is stored in the stack pointer. 687 The register map is initialized first to the empty map, assigning an undefined value to all register, before the value of the parameters is inserted into the map into the argument registers, and a new \texttt{State} follows. 688 689 690 Eventually, a Return instruction is faced, 691 the return value is fetched from the registers map, 692 the stack frame is deallocated 693 and a Return state is entered: 683 694 \begin{displaymath} 684 695 \begin{array}{rcl} 685 \mathtt{ sp = alloc,\ regs = \emptyset[ := PARAMS]} & \longrightarrow & \mathtt{free(sp)} \\686 \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)}& & \mathtt{Return(M(ret\_val), dst, Frames)}696 \mathtt{Return(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{free(sp)} \\ 697 & & \mathtt{Return(M(ret\_val), dst, Frames)} 687 698 \end{array} 688 699 \end{displaymath} 700 689 701 Then the return state restores the program counter by popping the stack, and execution proceeds in a new \texttt{State}, like the case for external functions: 690 702 \begin{displaymath} … … 695 707 \end{displaymath} 696 708 697 Translation from RTLabs to RTL states proceeds as follows. 698 Return states are translated as is:709 \subparagraph{The RTLabs to RTL translation for function calls} 710 Return instructions are translated to return instructions: 699 711 \begin{displaymath} 700 712 \mathtt{Return} \longrightarrow \mathtt{Return} 701 713 \end{displaymath} 702 714 703 \texttt{Call} states are translated to \texttt{Call\_ID} states: 704 \begin{displaymath} 705 \mathtt{Call(id,\ args,\ dst,\ pc)} \longrightarrow \mathtt{Call\_ID(id,\ \sigma'(args),\ \sigma(dst),\ pc)} 706 \end{displaymath} 707 Here, $\sigma$ and $\sigma'$ are two maps to be defined between pseudoregisters and lists of pseudoregisters, of the type: 708 709 \begin{displaymath} 710 \sigma: \mathtt{register} \rightarrow \mathtt{list\ register} 711 \end{displaymath} 712 713 and: 714 715 \begin{displaymath} 716 \sigma': \mathtt{list\ register} \rightarrow \mathtt{list\ register} 717 \end{displaymath} 718 719 where $\sigma'$ is implemented as: 720 721 \begin{displaymath} 722 \sigma' = \mathtt{flatten} \circ \sigma 723 \end{displaymath} 715 \texttt{Call} instructions are translated to \texttt{Call\_ID} instructions: 716 \begin{displaymath} 717 \mathtt{Call(id,\ args,\ dst,\ pc)} \longrightarrow \mathtt{CALL\_ID(id,\ \Sigma'(args),\ \Sigma(dst),\ pc)} 718 \end{displaymath} 719 Here $\Sigma$ is the map, computed by the compiler, 720 that translate pseudoregisters holding frontend values to list of 721 pseudoregisters holding the chunks for the frontend values. 722 The specification for $\Sigma$ is that for every state $s$, 723 $$\sigma(s(r)) = (\sigma(s))(\Sigma(r))$$ 724 725 \subparagraph{Function call/return in RTL} 724 726 725 727 In the case of RTL, execution proceeds as follows. … … 727 729 Then a case split occurs depending on whether we are executing an internal or an external function, as in the RTLabs case: 728 730 \begin{displaymath} 731 \hspace{3.5cm} 729 732 \begin{diagram} 730 733 & & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\ 731 734 & \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\ 732 \skull & & & & \mathtt{regs} = [\mathtt{params}/] \\ 733 & & & & \mathtt{sp} = \mathtt{ALLOC} \\ 734 & & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\ 735 \skull & & & & 736 \begin{array}{l} 737 \mathtt{sp = alloc,\ regs = \emptyset[ := params]} \\ 738 \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} 739 \end{array} 735 740 \end{diagram} 736 741 \end{displaymath} … … 747 752 Note, in particular, that this final act of pushing a frame on the stack leaves us in an identical state to the RTLabs case, where the instruction 748 753 \begin{displaymath} 749 \mathtt{PUSH(current\_frame[PC := after\_return])} 750 \end{displaymath} 751 752 was executed. 754 \mathtt{PUSH(current\_frame[pc := after\_return])} 755 \end{displaymath} 756 was executed. To summarize, up to the different numer of transitions required 757 to do the job, the RTL code for internal function calls closely simulates 758 the RTLabs code. 753 759 754 760 The execution of \texttt{Return} in RTL is similarly straightforward, with the return address, stack pointer, and so on, being computed by popping off the top of the stack, and the return value computed by the function being retrieved from memory: 755 761 \begin{align*} 756 762 \mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\ 757 v * & := M(\mathtt{rv\_regs}) \\763 v^* & := M(\mathtt{rv\_regs}) \\ 758 764 \mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\ 759 \mathtt{regs}[v * / \mathtt{dst}] \\765 \mathtt{regs}[v^* / \mathtt{dst}] \\ 760 766 \end{align*} 767 768 To summarize, the forward simulation diagrams for function call/return 769 XXX 770 761 771 762 772 Translation and execution must satisfy a pair of commutation properties for the \texttt{Return} and \texttt{Call} cases. … … 832 842 \subsection{The ERTL to LTL translation} 833 843 \label{subsect.ertl.ltl.translation} 844 During the ERTL to LTL translation pseudoregisters are stored in hardware 845 registers or spilled on to the stack frame. The decision is based on liveness 846 analysis of the ERTL code to determine what pair of pseudoregisters are live 847 at the same time at a given location. A coloring algorithm is then used to 848 choose where to store the pseudoregisters, allowing pseudoregisters that 849 are never live at the same time to share the same location. 850 851 We will not certify any coloring algorithm or control flow analysis. 852 Instead, we axiomatically assume the existence of solutions to the 853 coloring and liveness problems. In a later phase we plan to validate the 854 solutions by writing and certifying the code of a validator. 855 856 We describe the liveness analysis and colouring analysis first and then 857 the ERTL to LTL translation. 858 859 Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$ and hardware ones with $\mathtt{hdwregister}$. 860 \subsubsection{Liveness analysis} 834 861 \newcommand{\declsf}[1]{\expandafter\newcommand\expandafter{\csname #1\endcsname}{\mathop{\mathsf{#1}}\nolimits}} 835 862 \declsf{Livebefore} … … 839 866 \declsf{Eliminable} 840 867 \declsf{StatementSem} 841 Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$842 and hardware ones with $\mathtt{hdwregister}$.843 868 844 869 For the liveness analysis, we aim at a map … … 855 880 is the type of sets of registers\footnote{More precisely, it is the lattice 856 881 of pairs of sets of pseudoregisters and sets of hardware registers, 857 with pointwise operations.} , we also have have the following882 with pointwise operations.}), we also have have the following 858 883 predicates: 859 884 $$ … … 920 945 \end{equation} 921 946 922 We mark a certain colouring with a subscript if we want to specify in which923 internal function it is taken.924 947 \subsubsection{The translation} 925 948 For example: … … 968 991 (with appropriate costlabelled trace preservation which we omit). We will call $S\mathrel \sigma T$ 969 992 the inductive hypothsis, as it will be such in the complete proof by induction on the trace of the program. 970 As usual, this step bedone by cases993 As usual, this step is done by cases 971 994 on the statement at $\ell(S)$ and how it is translated. We carry out in some detail a single case, the one of 972 995 a binary operation on registers. … … 1272 1295 Total & 14630 & 3.75 \permil & 49.30 & 54.0 \\ 1273 1296 \end{tabular} 1274 \caption{\label{table} Estimated effort}1297 \caption{\label{table} Estimated effort} 1275 1298 \end{table} 1276 1299 … … 1288 1311 are relative to an early version of CompCert) we computed the ratio between 1289 1312 men months and lines of code in CompCert for each CerCo pass. This is shown 1290 in the third column of Table~\ref{ wildguess}. For those CerCo passes that1313 in the third column of Table~\ref{table}. For those CerCo passes that 1291 1314 have no correspondence in CompCert (like the optimizing assembler) or where 1292 1315 we have insufficient data, we have used the average of the ratios computed
Note: See TracChangeset
for help on using the changeset viewer.