Changeset 2375 for Papers

Sep 28, 2012, 6:12:02 PM (7 years ago)


1 edited


  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2374 r2375  
    605605pseudostatus and the current tracking map in order to identify those memory
    606606cells and registers that hold fragments of addresses to be mapped using
    607 \texttt{policy} as previously explained.
     607\texttt{policy} as previously explained. It also calls the assembler to
     608replace the code memory of the assembly status (i.e. the assembly program)
     609with the object code produced by the assembler.
    609611definition status_of_pseudo_status:
    632634   program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map
    635 If we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed.
    636 Note we once again use dependent types to ensure that program counters are properly within bounds.
    637 The third argument is a function that resolves the concrete address of a label.
    639 The function \texttt{ticks\_of0} computes how long---in clock cycles---a pseudoinstruction will take to execute when expanded in accordance with a given policy.
    640 The function returns a pair of natural numbers, needed for recording the execution times of each branch of a conditional jump.
    641 \begin{lstlisting}
    642 definition ticks_of0:
    643  pseudo_assembly_program $\rightarrow$ (Identifier $\rightarrow$ Word) $\rightarrow$ $\forall$policy. Word $\rightarrow$
    644    pseudo_instruction $\rightarrow$ nat $\times$ nat
    645 \end{lstlisting}
    646 An additional function, \texttt{ticks\_of}, is merely a wrapper around this function.
    648 Finally, we are able to state and prove our main theorem, relating the execution of a single assembly instruction and the execution of (possibly) many machine code instructions, as long as we are able to track memory addresses properly:
     637We are now ready to state the (slightly simplified) statement of correctness of our compiler, whose
     638proofs combines correctness w.r.t. fetching and correctness w.r.t. execution.
     639It states that the well behaved execution of a single assembly pseudoinstruction
     640according to the cost model induced by compilation
     641is correctly simulated by the execution of (possibly) many machine code
    650644theorem main_thm:
    652646 $\forall$program: pseudo_assembly_program.
    653647 $\forall$program_in_bounds: $\mid$program$\mid$ $\leq$ $2^{16}$.
    654  let maps := create_label_cost_map program in
    655  let addr_of := ... in
    656  program is well labelled $\rightarrow$
    657648 $\forall$policy. policy is correct for program.
    658649 $\forall$ps: PseudoStatus program. ps < $\mid$program$\mid$.
    660651   $\exists$n. execute n (status_of_pseudo_status M ps policy) =
    661652    status_of_pseudo_status M'
    662       (execute_1_pseudo_instruction program
    663        (ticks_of program ($\lambda$id. addr_of id ps) policy) ps) policy.
    664 \end{lstlisting}
    665 The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}.
    666 We explicitly require proof that the policy is correct, the program is well-labelled (i.e. no repeated labels, etc.) and the pseudo-program counter is in the program's bounds.
    667 Theorem \texttt{main\_thm} establishes the correctness of the assembly process and can be lifted to the forward simulation of an arbitrary number of well-behaved steps on the assembly program.
     653     (execute_1_pseudo_instruction program (ticks_of program policy) ps)
     654     policy.
     656The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose tracking map is \texttt{M} and who
     657are well behaved according to \texttt{internal\_pseudo\_address\_map}
     658\texttt{M}. The \texttt{ticks\_of program policy} function returns the
     659costing computed by assembling the \texttt{program} using the given
     660\texttt{policy}. An obvious corollary of \texttt{main\_thm} is the correct
     661simulation of $n$ well behaved steps by some number of steps $m$, where each
     662step must be well behaved w.r.t. the tracking map returned by the previous
    669665% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.