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

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2374 r2375 605 605 pseudostatus and the current tracking map in order to identify those memory 606 606 cells 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 608 replace the code memory of the assembly status (i.e. the assembly program) 609 with the object code produced by the assembler. 608 610 \begin{lstlisting} 609 611 definition status_of_pseudo_status: … … 632 634 program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map 633 635 \end{lstlisting} 634 XXXXXXXXXX 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. 638 639 The function \texttt{ticks\_of0} computes how longin clock cyclesa 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. 647 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: 636 637 We are now ready to state the (slightly simplified) statement of correctness of our compiler, whose 638 proofs combines correctness w.r.t. fetching and correctness w.r.t. execution. 639 It states that the well behaved execution of a single assembly pseudoinstruction 640 according to the cost model induced by compilation 641 is correctly simulated by the execution of (possibly) many machine code 642 instructions. 649 643 \begin{lstlisting} 650 644 theorem main_thm: … … 652 646 $\forall$program: pseudo_assembly_program. 653 647 $\forall$program_in_bounds: $\mid$program$\mid$ $\leq$ $2^{16}$. 654 let maps := create_label_cost_map program in655 let addr_of := ... in656 program is well labelled $\rightarrow$657 648 $\forall$policy. policy is correct for program. 658 649 $\forall$ps: PseudoStatus program. ps < $\mid$program$\mid$. … … 660 651 $\exists$n. execute n (status_of_pseudo_status M ps policy) = 661 652 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 wellbehaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}. 666 We explicitly require proof that the policy is correct, the program is welllabelled (i.e. no repeated labels, etc.) and the pseudoprogram 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 wellbehaved steps on the assembly program. 653 (execute_1_pseudo_instruction program (ticks_of program policy) ps) 654 policy. 655 \end{lstlisting} 656 The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose tracking map is \texttt{M} and who 657 are well behaved according to \texttt{internal\_pseudo\_address\_map} 658 \texttt{M}. The \texttt{ticks\_of program policy} function returns the 659 costing computed by assembling the \texttt{program} using the given 660 \texttt{policy}. An obvious corollary of \texttt{main\_thm} is the correct 661 simulation of $n$ well behaved steps by some number of steps $m$, where each 662 step must be well behaved w.r.t. the tracking map returned by the previous 663 step. 668 664 669 665 %  %
Note: See TracChangeset
for help on using the changeset viewer.