# Changeset 2375 for Papers

Ignore:
Timestamp:
Sep 28, 2012, 6:12:02 PM (9 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2374 pseudostatus and the current tracking map in order to identify those memory cells and registers that hold fragments of addresses to be mapped using \texttt{policy} as previously explained. \texttt{policy} as previously explained. It also calls the assembler to replace the code memory of the assembly status (i.e. the assembly program) with the object code produced by the assembler. \begin{lstlisting} definition status_of_pseudo_status: program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} XXXXXXXXXX If we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed. Note we once again use dependent types to ensure that program counters are properly within bounds. The third argument is a function that resolves the concrete address of a label. 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. The function returns a pair of natural numbers, needed for recording the execution times of each branch of a conditional jump. \begin{lstlisting} definition ticks_of0: pseudo_assembly_program $\rightarrow$ (Identifier $\rightarrow$ Word) $\rightarrow$ $\forall$policy. Word $\rightarrow$ pseudo_instruction $\rightarrow$ nat $\times$ nat \end{lstlisting} An additional function, \texttt{ticks\_of}, is merely a wrapper around this function. 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: We are now ready to state the (slightly simplified) statement of correctness of our compiler, whose proofs combines correctness w.r.t. fetching and correctness w.r.t. execution. It states that the well behaved execution of a single assembly pseudoinstruction according to the cost model induced by compilation is correctly simulated by the execution of (possibly) many machine code instructions. \begin{lstlisting} theorem main_thm: $\forall$program: pseudo_assembly_program. $\forall$program_in_bounds: $\mid$program$\mid$ $\leq$ $2^{16}$. let maps := create_label_cost_map program in let addr_of := ... in program is well labelled $\rightarrow$ $\forall$policy. policy is correct for program. $\forall$ps: PseudoStatus program. ps < $\mid$program$\mid$. $\exists$n. execute n (status_of_pseudo_status M ps policy) = status_of_pseudo_status M' (execute_1_pseudo_instruction program (ticks_of program ($\lambda$id. addr_of id ps) policy) ps) policy. \end{lstlisting} 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}. 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. 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. (execute_1_pseudo_instruction program (ticks_of program policy) ps) policy. \end{lstlisting} The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose tracking map is \texttt{M} and who are well behaved according to \texttt{internal\_pseudo\_address\_map} \texttt{M}. The \texttt{ticks\_of program policy} function returns the costing computed by assembling the \texttt{program} using the given \texttt{policy}. An obvious corollary of \texttt{main\_thm} is the correct simulation of $n$ well behaved steps by some number of steps $m$, where each step must be well behaved w.r.t. the tracking map returned by the previous step. % ---------------------------------------------------------------------------- %