Changeset 1786


Ignore:
Timestamp:
Feb 27, 2012, 6:40:46 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1785 r1786  
    468468\label{subsect.rtlabs.rtl.translation}
    469469
     470\subsubsection*{Translation of values and memory}
     471
    470472The RTLabs to RTL translation pass marks the frontier between the two memory models used in the CerCo project.
    471473As a result, we require some method of translating between the values that the two memory models permit.
     
    559561property of $\sigma$ to be proved.
    560562
     563\subsubsection*{Translation of RTLabs states}
    561564RTLabs states come in three flavours:
    562565\begin{displaymath}
     
    637640\end{figure}
    638641
     642\subsubsection*{The forward simulation proof}
    639643The forward simulation proof for all steps that do not involve function calls are lengthy, but routine.
    640644They consist of simulating a front-end operation on front-end pseudo-registers and the front-end memory with sequences of back-end operations on the back-end pseudo-registers and back-end memory.
     
    644648We sketch here what happens on the source code and on its translation.
    645649
     650\subparagraph{Function call/return in RTLabs}
     651
    646652\begin{displaymath}
    647653\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])}
    650656\end{array}
    651657\end{displaymath}
     
    659665\begin{array}{rcl}
    660666\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])} &                                                            &
    662668\end{array}
    663669\end{displaymath}
     
    674680\begin{displaymath}
    675681\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)}
    678684\end{array}
    679685\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:
     686A new stack frame is allocated and its address is stored in the stack pointer.
     687The 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
     690Eventually, a Return instruction is faced,
     691the return value is fetched from the registers map,
     692the stack frame is deallocated
     693and a Return state is entered:
    683694\begin{displaymath}
    684695\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)}
    687698\end{array}
    688699\end{displaymath}
     700
    689701Then 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:
    690702\begin{displaymath}
     
    695707\end{displaymath}
    696708
    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}
     710Return instructions are translated to return instructions:
    699711\begin{displaymath}
    700712\mathtt{Return} \longrightarrow \mathtt{Return}
    701713\end{displaymath}
    702714
    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 pseudo-registers and lists of pseudo-registers, 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}
     719Here $\Sigma$ is the map, computed by the compiler,
     720that translate pseudo-registers holding front-end values to list of
     721pseudo-registers holding the chunks for the front-end values.
     722The 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}
    724726
    725727In the case of RTL, execution proceeds as follows.
     
    727729Then a case split occurs depending on whether we are executing an internal or an external function, as in the RTLabs case:
    728730\begin{displaymath}
     731\hspace{-3.5cm}
    729732\begin{diagram}
    730733& & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\
    731734& \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}
    735740\end{diagram}
    736741\end{displaymath}
     
    747752Note, 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
    748753\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}
     756was executed. To summarize, up to the different numer of transitions required
     757to do the job, the RTL code for internal function calls closely simulates
     758the RTLabs code.
    753759
    754760The 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:
    755761\begin{align*}
    756762\mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
    757 v*                    & := M(\mathtt{rv\_regs}) \\
     763v^*                    & := M(\mathtt{rv\_regs}) \\
    758764\mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
    759 \mathtt{regs}[v* / \mathtt{dst}] \\
     765\mathtt{regs}[v^* / \mathtt{dst}] \\
    760766\end{align*}
     767
     768To summarize, the forward simulation diagrams for function call/return
     769XXX
     770
    761771
    762772Translation and execution must satisfy a pair of commutation properties for the \texttt{Return} and \texttt{Call} cases.
     
    832842\subsection{The ERTL to LTL translation}
    833843\label{subsect.ertl.ltl.translation}
     844During the ERTL to LTL translation pseudo-registers are stored in hardware
     845registers or spilled on to the stack frame. The decision is based on liveness
     846analysis of the ERTL code to determine what pair of pseudoregisters are live
     847at the same time at a given location. A coloring algorithm is then used to
     848choose where to store the pseudo-registers, allowing pseudo-registers that
     849are never live at the same time to share the same location.
     850
     851We will not certify any coloring algorithm or control flow analysis.
     852Instead, we axiomatically assume the existence of solutions to the
     853coloring and liveness problems. In a later phase we plan to validate the
     854solutions by writing and certifying the code of a validator.
     855
     856We describe the liveness analysis and colouring analysis first and then
     857the ERTL to LTL translation.
     858
     859Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$ and hardware ones with $\mathtt{hdwregister}$.
     860\subsubsection{Liveness analysis}
    834861\newcommand{\declsf}[1]{\expandafter\newcommand\expandafter{\csname #1\endcsname}{\mathop{\mathsf{#1}}\nolimits}}
    835862\declsf{Livebefore}
     
    839866\declsf{Eliminable}
    840867\declsf{StatementSem}
    841 Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$
    842 and hardware ones with $\mathtt{hdwregister}$.
    843868
    844869For the liveness analysis, we aim at a map
     
    855880is the type of sets of registers\footnote{More precisely, it is the lattice
    856881of pairs of sets of pseudo-registers and sets of hardware registers,
    857 with pointwise operations.}, we also have have the following
     882with pointwise operations.}), we also have have the following
    858883predicates:
    859884$$
     
    920945\end{equation}
    921946
    922 We mark a certain colouring with a subscript if we want to specify in which
    923 internal function it is taken.
    924947\subsubsection{The translation}
    925948For example:
     
    968991(with appropriate cost-labelled trace preservation which we omit). We will call $S\mathrel \sigma T$
    969992the inductive hypothsis, as it will be such in the complete proof by induction on the trace of the program.
    970 As usual, this step be done by cases
     993As usual, this step is done by cases
    971994on the statement at $\ell(S)$ and how it is translated. We carry out in some detail a single case, the one of
    972995a binary operation on registers.
     
    12721295Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
    12731296\end{tabular}
    1274 \caption{\label{table}Estimated effort}
     1297\caption{\label{table} Estimated effort}
    12751298\end{table}
    12761299
     
    12881311are relative to an early version of CompCert) we computed the ratio between
    12891312men 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 that
     1313in the third column of Table~\ref{table}. For those CerCo passes that
    12911314have no correspondence in CompCert (like the optimizing assembler) or where
    12921315we have insufficient data, we have used the average of the ratios computed
Note: See TracChangeset for help on using the changeset viewer.