# Changeset 1791 for Deliverables/D1.2

Ignore:
Timestamp:
Feb 28, 2012, 5:01:13 PM (9 years ago)
Message:

cleaning up

File:
1 edited

### Legend:

Unmodified
 r1790 The first lemma required has the following statement: \begin{displaymath} \mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i \mathtt{load\ s\ a\ M} = \mathtt{Some\ v} \rightarrow \forall i \leq s.\ \mathtt{load\ s\ (a + i)\ \sigma(M)} = \mathtt{Some\ v_i} \end{displaymath} That is, if we are successful in reading a value of size $s$ from memory at address $a$ in front-end memory, then we should successfully be able to read all of its chunks from memory in the back-end memory at appropriate address (from address $a$ up to and including address $a + i$, where $i \leq s$). Next, we must show that \texttt{store} properly commutes with the $\sigma$-map between memory spaces: \begin{displaymath} \sigma(\mathtt{store}\ a\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(a)\ \sigma(M) \sigma(\mathtt{store\ a\ v\ M}) = \mathtt{store\ \sigma(v)\ \sigma(a)\ \sigma(M)} \end{displaymath} That is, if we store a value \texttt{v} in the front-end memory \texttt{M} at address \texttt{a} and transform the resulting memory with $\sigma$, then this is equivalent to storing a transformed value $\mathtt{\sigma(v)}$ at address $\mathtt{\sigma(a)}$ into the back-end memory $\mathtt{\sigma(M)}$. Writing \texttt{load}$^*$ for the multiple consecutive iterations of \texttt{load} used to fetch all chunks of a value, we must prove that, when $a \neq a'$: \begin{displaymath} \texttt{load}^* \sigma(a)\ (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M)) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M) \mathtt{load^* \sigma(a)\ (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M))} = \mathtt{load^*\ \sigma(s)\ \sigma(a)\ \sigma(M)} \end{displaymath} That is, suppose we store a transformed value $\mathtt{\sigma(v)}$ into a back-end memory $\mathtt{\sigma(M)}$ at address $\mathtt{\sigma(a')}$, using \texttt{store}, and then load from the address $\sigma(a)$. Even if $a$ and $a'$ are distinct by hypothesis, there is \emph{a priori} no guarantee that the consecutive bytes for the value stored at $\sigma(a)$ are disjoint from those for the values stored at $\sigma(a')$. For \texttt{State} we perform a further case analysis of the top stack frame, which decomposes into a tuple holding the current program counter value, the current stack pointer and the value of the registers: \begin{displaymath} \sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{\langle PC, REGS, SP \rangle})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), \star, \star, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem})) \sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{\langle PC, REGS, SP, \ldots \rangle})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), \star, \star, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem})) \end{displaymath} Translation then proceeds by translating the remaining stack frames, as well as the contents of the top stack frame. \begin{displaymath} \begin{array}{rcl} \mathtt{Call(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\ \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} Suppose we are given a \texttt{State} with a list of stack frames, with the top frame being \texttt{Frame}. Suppose also that the program counter in \texttt{Frame} points to a \texttt{Call} instruction, complete with arguments and destination address. Suppose also that the program counter in \texttt{Frame} points to a \texttt{CALL} instruction, complete with arguments and destination address. Then this is executed by entering into a \texttt{Call} state where the arguments are loaded from memory, and the address pointing to the instruction immediately following the \texttt{Call} instruction is filled in, with the current stack frame being pushed on top of the stack with the return address substituted for the program counter. \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(Frame[pc := after\_return])} &                                                            & \end{array} \end{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{PUSH(Frame[pc := after\_return])} &                 & \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)} \end{array} \end{displaymath} \begin{array}{rcl} \mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\ \mathtt{Return(M(ret\_val), dst, frames)} &                 & \mathtt{State(regs[dst := M(ret\_val),\ pc)} \mathtt{Return(M(ret\_val), dst, Frame^*)} &                 & \mathtt{State(regs[dst := M(ret\_val),\ pc)} \end{array} \end{displaymath} \begin{align*} \mathtt{sp} & = \mathtt{RegisterSPH} / \mathtt{RegisterSPL} \\ \mathtt{graph} & \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\ \mathtt{graph} & = \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\ & \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\ \end{align*} \begin{table}{h} \begin{center} \begin{tabular}{lrlrr} Pass origin & Code lines & CompCert ratio & Estimated effort & Estimated effort \\ Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\ \end{tabular} \end{center} \caption{\label{table} Estimated effort} \end{table}