Changeset 1791 for Deliverables/D1.2/CompilerProofOutline/outline.tex
 Timestamp:
 Feb 28, 2012, 5:01:13 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1790 r1791 499 499 The first lemma required has the following statement: 500 500 \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_i501 \mathtt{load\ s\ a\ M} = \mathtt{Some\ v} \rightarrow \forall i \leq s.\ \mathtt{load\ s\ (a + i)\ \sigma(M)} = \mathtt{Some\ v_i} 502 502 \end{displaymath} 503 503 That is, if we are successful in reading a value of size $s$ from memory at address $a$ in frontend memory, then we should successfully be able to read all of its chunks from memory in the backend memory at appropriate address (from address $a$ up to and including address $a + i$, where $i \leq s$). … … 505 505 Next, we must show that \texttt{store} properly commutes with the $\sigma$map between memory spaces: 506 506 \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)} 508 508 \end{displaymath} 509 509 That is, if we store a value \texttt{v} in the frontend 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 backend memory $\mathtt{\sigma(M)}$. … … 512 512 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'$: 513 513 \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)} 515 515 \end{displaymath} 516 516 That is, suppose we store a transformed value $\mathtt{\sigma(v)}$ into a backend 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')$. … … 556 556 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: 557 557 \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})) 559 559 \end{displaymath} 560 560 Translation then proceeds by translating the remaining stack frames, as well as the contents of the top stack frame. … … 607 607 \begin{displaymath} 608 608 \begin{array}{rcl} 609 \mathtt{C all(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)}, \\ 610 610 & & \mathtt{PUSH(Frame[pc := after\_return])} 611 611 \end{array} 612 612 \end{displaymath} 613 613 Suppose 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{C all} instruction, complete with arguments and destination address.614 Suppose also that the program counter in \texttt{Frame} points to a \texttt{CALL} instruction, complete with arguments and destination address. 615 615 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. 616 616 … … 620 620 \begin{array}{rcl} 621 621 \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])} & & 623 623 \end{array} 624 624 \end{displaymath} … … 636 636 \begin{array}{rcl} 637 637 \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)} 639 639 \end{array} 640 640 \end{displaymath} … … 655 655 \begin{array}{rcl} 656 656 \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)} 658 658 \end{array} 659 659 \end{displaymath} … … 738 738 \begin{align*} 739 739 \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) \\ 741 741 & \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\ 742 742 \end{align*} … … 1189 1189 1190 1190 \begin{table}{h} 1191 \begin{center} 1191 1192 \begin{tabular}{lrlrr} 1192 1193 Pass origin & Code lines & CompCert ratio & Estimated effort & Estimated effort \\ … … 1209 1210 Total & 14630 & 3.75 \permil & 49.30 & 54.0 \\ 1210 1211 \end{tabular} 1212 \end{center} 1211 1213 \caption{\label{table} Estimated effort} 1212 1214 \end{table}
Note: See TracChangeset
for help on using the changeset viewer.