Changeset 1786 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 27, 2012, 6:40:46 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (16 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -468 +468 @@
 \label{subsect.rtlabs.rtl.translation}
 
+\subsubsection*{Translation of values and memory}
+
 The RTLabs to RTL translation pass marks the frontier between the two memory models used in the CerCo project.
 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.
 
+\subsubsection*{Translation of RTLabs states}
 RTLabs states come in three flavours:
 \begin{displaymath}
@@ -637 +640 @@
 \end{figure}
 
+\subsubsection*{The forward simulation proof}
 The forward simulation proof for all steps that do not involve function calls are lengthy, but routine.
 They 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.
@@ -644 +648 @@
 We sketch here what happens on the source code and on its translation.
 
+\subparagraph{Function call/return in RTLabs}
+
 \begin{displaymath}
 \begin{array}{rcl}
-\mathtt{Call(id,\ args,\ dst,\ pc),\ State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
-                                                           &                 & \mathtt{PUSH(Frame[PC := after\_return])}
+\mathtt{Call(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
+                                                           &                 & \mathtt{PUSH(Frame[pc := after\_return])}
 \end{array}
 \end{displaymath}
@@ -659 +665 @@
 \begin{array}{rcl}
 \mathtt{Call(M(args), dst)},                       & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\
-\mathtt{PUSH(current\_frame[PC := after\_return])} &                                                            & 
+\mathtt{PUSH(current\_frame[pc := after\_return])} &                                                            & 
 \end{array}
 \end{displaymath}
@@ -674 +680 @@
 \begin{displaymath}
 \begin{array}{rcl}
-\mathtt{Call(M(args), dst)}                        & \longrightarrow & \mathtt{SP = alloc,\ regs = \emptyset[- := params]} \\
-\mathtt{PUSH(current\_frame[PC := after\_return])} &                 & \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)}
+\mathtt{Call(M(args), dst)}                        & \longrightarrow & \mathtt{sp = alloc,\ regs = \emptyset[- := params]} \\
+\mathtt{PUSH(current\_frame[pc := after\_return])} &                 & \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)}
 \end{array}
 \end{displaymath}
-Here, execution of the \texttt{Call} state first pushes the current frame with the program counter set to the address following the function call.
-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.
-After this, the stack pointer is freed and a \texttt{Return} state is entered:
+A new stack frame is allocated and its address is stored in the stack pointer.
+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.
+
+
+Eventually, a Return instruction is faced,
+the return value is fetched from the registers map,
+the stack frame is deallocated
+and a Return state is entered:
 \begin{displaymath}
 \begin{array}{rcl}
-\mathtt{sp = alloc,\ regs = \emptyset[- := PARAMS]} & \longrightarrow & \mathtt{free(sp)} \\
-\mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)}     &                 & \mathtt{Return(M(ret\_val), dst, Frames)}
+\mathtt{Return(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{free(sp)} \\
+   &                 & \mathtt{Return(M(ret\_val), dst, Frames)}
 \end{array}
 \end{displaymath}
+
 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:
 \begin{displaymath}
@@ -695 +707 @@
 \end{displaymath}
 
-Translation from RTLabs to RTL states proceeds as follows.
-Return states are translated as is:
+\subparagraph{The RTLabs to RTL translation for function calls}
+Return instructions are translated to return instructions:
 \begin{displaymath}
 \mathtt{Return} \longrightarrow \mathtt{Return}
 \end{displaymath}
 
-\texttt{Call} states are translated to \texttt{Call\_ID} states:
-\begin{displaymath}
-\mathtt{Call(id,\ args,\ dst,\ pc)} \longrightarrow \mathtt{Call\_ID(id,\ \sigma'(args),\ \sigma(dst),\ pc)}
-\end{displaymath}
-Here, $\sigma$ and $\sigma'$ are two maps to be defined between pseudo-registers and lists of pseudo-registers, of the type:
-
-\begin{displaymath}
-\sigma: \mathtt{register} \rightarrow \mathtt{list\ register}
-\end{displaymath}
-
-and:
-
-\begin{displaymath}
-\sigma': \mathtt{list\ register} \rightarrow \mathtt{list\ register}
-\end{displaymath}
-
-where $\sigma'$ is implemented as:
-
-\begin{displaymath}
-\sigma' = \mathtt{flatten} \circ \sigma
-\end{displaymath}
+\texttt{Call} instructions are translated to \texttt{Call\_ID} instructions:
+\begin{displaymath}
+\mathtt{Call(id,\ args,\ dst,\ pc)} \longrightarrow \mathtt{CALL\_ID(id,\ \Sigma'(args),\ \Sigma(dst),\ pc)}
+\end{displaymath}
+Here $\Sigma$ is the map, computed by the compiler,
+that translate pseudo-registers holding front-end values to list of
+pseudo-registers holding the chunks for the front-end values.
+The specification for $\Sigma$ is that for every state $s$,
+$$\sigma(s(r)) = (\sigma(s))(\Sigma(r))$$
+
+\subparagraph{Function call/return in RTL}
 
 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:
 \begin{displaymath}
+\hspace{-3.5cm}
 \begin{diagram}
 & & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\
 & \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\
-\skull & & & & \mathtt{regs} = [\mathtt{params}/-] \\
-& & & & \mathtt{sp} = \mathtt{ALLOC} \\
-& & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\
+\skull & & & &
+\begin{array}{l}
+\mathtt{sp = alloc,\ regs = \emptyset[- := params]} \\
+\mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp}
+\end{array}
 \end{diagram}
 \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
 \begin{displaymath}
-\mathtt{PUSH(current\_frame[PC := after\_return])}
-\end{displaymath}
-
-was executed.
+\mathtt{PUSH(current\_frame[pc := after\_return])}
+\end{displaymath}
+was executed. To summarize, up to the different numer of transitions required
+to do the job, the RTL code for internal function calls closely simulates
+the RTLabs code.
 
 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:
 \begin{align*}
 \mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
-v*                    & := M(\mathtt{rv\_regs}) \\
+v^*                    & := M(\mathtt{rv\_regs}) \\
 \mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
-\mathtt{regs}[v* / \mathtt{dst}] \\
+\mathtt{regs}[v^* / \mathtt{dst}] \\
 \end{align*}
+
+To summarize, the forward simulation diagrams for function call/return
+XXX
+
 
 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}
 \label{subsect.ertl.ltl.translation}
+During the ERTL to LTL translation pseudo-registers are stored in hardware
+registers or spilled on to the stack frame. The decision is based on liveness
+analysis of the ERTL code to determine what pair of pseudoregisters are live
+at the same time at a given location. A coloring algorithm is then used to
+choose where to store the pseudo-registers, allowing pseudo-registers that
+are never live at the same time to share the same location.
+
+We will not certify any coloring algorithm or control flow analysis.
+Instead, we axiomatically assume the existence of solutions to the
+coloring and liveness problems. In a later phase we plan to validate the
+solutions by writing and certifying the code of a validator.
+
+We describe the liveness analysis and colouring analysis first and then
+the ERTL to LTL translation.
+
+Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$ and hardware ones with $\mathtt{hdwregister}$.
+\subsubsection{Liveness analysis}
 \newcommand{\declsf}[1]{\expandafter\newcommand\expandafter{\csname #1\endcsname}{\mathop{\mathsf{#1}}\nolimits}}
 \declsf{Livebefore}
@@ -839 +866 @@
 \declsf{Eliminable}
 \declsf{StatementSem}
-Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$
-and hardware ones with $\mathtt{hdwregister}$.
 
 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
 of pairs of sets of pseudo-registers and sets of hardware registers,
-with pointwise operations.}, we also have have the following
+with pointwise operations.}), we also have have the following
 predicates:
 $$
@@ -920 +945 @@
 \end{equation}
 
-We mark a certain colouring with a subscript if we want to specify in which
-internal function it is taken.
 \subsubsection{The translation}
 For example:
@@ -968 +991 @@
 (with appropriate cost-labelled trace preservation which we omit). We will call $S\mathrel \sigma T$
 the inductive hypothsis, as it will be such in the complete proof by induction on the trace of the program.
-As usual, this step be done by cases
+As usual, this step is done by cases
 on the statement at $\ell(S)$ and how it is translated. We carry out in some detail a single case, the one of
 a binary operation on registers.
@@ -1272 +1295 @@
 Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
 \end{tabular}
-\caption{\label{table}Estimated effort}
+\caption{\label{table} Estimated effort}
 \end{table}
 
@@ -1288 +1311 @@
 are relative to an early version of CompCert) we computed the ratio between
 men months and lines of code in CompCert for each CerCo pass. This is shown
-in the third column of Table~\ref{wildguess}. For those CerCo passes that
+in the third column of Table~\ref{table}. For those CerCo passes that
 have no correspondence in CompCert (like the optimizing assembler) or where
 we have insufficient data, we have used the average of the ratios computed