Changeset 1791


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

cleaning up

File:
1 edited

Legend:

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

    r1790 r1791  
    499499The first lemma required has the following statement:
    500500\begin{displaymath}
    501 \mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
     501\mathtt{load\ s\ a\ M} = \mathtt{Some\ v} \rightarrow \forall i \leq s.\ \mathtt{load\ s\ (a + i)\ \sigma(M)} = \mathtt{Some\ v_i}
    502502\end{displaymath}
    503503That 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$).
     
    505505Next, we must show that \texttt{store} properly commutes with the $\sigma$-map between memory spaces:
    506506\begin{displaymath}
    507 \sigma(\mathtt{store}\ a\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(a)\ \sigma(M)
     507\sigma(\mathtt{store\ a\ v\ M}) = \mathtt{store\ \sigma(v)\ \sigma(a)\ \sigma(M)}
    508508\end{displaymath}
    509509That 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)}$.
     
    512512Writing \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'$:
    513513\begin{displaymath}
    514 \texttt{load}^* \sigma(a)\ (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M)) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
     514\mathtt{load^* \sigma(a)\ (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M))} = \mathtt{load^*\ \sigma(s)\ \sigma(a)\ \sigma(M)}
    515515\end{displaymath}
    516516That 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')$.
     
    556556For \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:
    557557\begin{displaymath}
    558 \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}))
     558\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}))
    559559\end{displaymath}
    560560Translation then proceeds by translating the remaining stack frames, as well as the contents of the top stack frame.
     
    607607\begin{displaymath}
    608608\begin{array}{rcl}
    609 \mathtt{Call(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
     609\mathtt{CALL(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
    610610                                                           &                 & \mathtt{PUSH(Frame[pc := after\_return])}
    611611\end{array}
    612612\end{displaymath}
    613613Suppose we are given a \texttt{State} with a list of stack frames, with the top frame being \texttt{Frame}.
    614 Suppose also that the program counter in \texttt{Frame} points to a \texttt{Call} instruction, complete with arguments and destination address.
     614Suppose also that the program counter in \texttt{Frame} points to a \texttt{CALL} instruction, complete with arguments and destination address.
    615615Then 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.
    616616
     
    620620\begin{array}{rcl}
    621621\mathtt{Call(M(args), dst)},                       & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\
    622 \mathtt{PUSH(current\_frame[pc := after\_return])} &                                                            &
     622\mathtt{PUSH(Frame[pc := after\_return])} &                                                            &
    623623\end{array}
    624624\end{displaymath}
     
    636636\begin{array}{rcl}
    637637\mathtt{Call(M(args), dst)}                        & \longrightarrow & \mathtt{sp = alloc,\ regs = \emptyset[- := params]} \\
    638 \mathtt{PUSH(current\_frame[pc := after\_return])} &                 & \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)}
     638\mathtt{PUSH(Frame[pc := after\_return])} &                 & \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)}
    639639\end{array}
    640640\end{displaymath}
     
    655655\begin{array}{rcl}
    656656\mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\
    657 \mathtt{Return(M(ret\_val), dst, frames)} &                 & \mathtt{State(regs[dst := M(ret\_val),\ pc)}
     657\mathtt{Return(M(ret\_val), dst, Frame^*)} &                 & \mathtt{State(regs[dst := M(ret\_val),\ pc)}
    658658\end{array}
    659659\end{displaymath}
     
    738738\begin{align*}
    739739\mathtt{sp} & = \mathtt{RegisterSPH} / \mathtt{RegisterSPL} \\
    740 \mathtt{graph} & \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
     740\mathtt{graph} & = \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
    741741& \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
    742742\end{align*}
     
    11891189
    11901190\begin{table}{h}
     1191\begin{center}
    11911192\begin{tabular}{lrlrr}
    11921193Pass origin & Code lines & CompCert ratio & Estimated effort & Estimated effort \\
     
    12091210Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
    12101211\end{tabular}
     1212\end{center}
    12111213\caption{\label{table} Estimated effort}
    12121214\end{table}
Note: See TracChangeset for help on using the changeset viewer.