Changeset 968 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 15, 2011, 4:32:57 PM (8 years ago)
Author:
mulligan
Message:

work on paper

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r960 r968  
    213213Notice, here, that the emulation function for pseudoprograms takes an additional argument.
    214214This is a function that maps program counters (for the pseudoprogram) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion.
    215 We require \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in the number of clock ticks needed for execution.
     215We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions.
     216If we change how we expand conditional jumps to labels, for instance, then the costing needs to change, hence \texttt{execute\_1\_pseudo\_instruction}'s parametricity in the costing.
     217
     218The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in the number of clock ticks needed for execution.
    216219This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
    217220During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es.
     
    233236\label{subsect.policies}
    234237
    235 \begin{lstlisting}
    236 inductive jump_length: Type[0] ≝
     238Policies exist to dictate how conditional and unconditional jumps at the assembly level should be expanded into machine code instructions.
     239Using policies, we are able to completely decouple the decision over how jumps are expanded with the act of expansion, simplifying our proofs.
     240As mentioned, the MCS-51 instruction set includes three different jump instructions: \texttt{SJMP}, \texttt{AJMP} and \texttt{LJMP}; call these `short', `medium' and `long' jumps, respectively:
     241\begin{lstlisting}
     242inductive jump_length: Type[0] :=
    237243  | short_jump: jump_length
    238244  | medium_jump: jump_length
     
    240246\end{lstlisting}
    241247
    242 \begin{lstlisting}
    243 definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
    244 \end{lstlisting}
    245 
    246 \begin{lstlisting}
    247 definition policy_ok := λpolicy.λp. sigma_safe policy p <> None ....
    248 \end{lstlisting}
    249 
     248A \texttt{jump\_expansion\_policy} is a map from \texttt{Word}s to \texttt{jump\_length}s, implemented as a trie.
     249Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump.
     250\begin{lstlisting}
     251definition jump_expansion_policy := BitVectorTrie jump_length 16.
     252\end{lstlisting}
     253
     254Next, we require a series of `sigma' functions.
     255These functions map assembly program counters to their machine code counterparts, establishing the correspondence between `positions' in an assembly program and `positions' in a machine code program.
     256At the heart of this process is \texttt{sigma0} which traverses an assembly program building maps from program counter to program counter.
     257This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails:
     258\begin{lstlisting}
     259definition sigma0: pseudo_assembly_program
     260                   $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
     261\end{lstlisting}
     262
     263We eventually lift this to functions from program counters to program counters:
     264\begin{lstlisting}
     265definition sigma_safe: pseudo_assembly_program
     266                       $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
     267\end{lstlisting}
     268
     269Now, it's possible to define what a `good policy' is i.e. one that does not cause \texttt{sigma\_safe} to fail.
     270As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
     271\begin{lstlisting}
     272definition policy_ok := $\lambda$policy. $\lambda$p. sigma_safe policy p $\neq$ None $\ldots$.
     273\end{lstlisting}
     274
     275Finally, we obtain \texttt{sigma}, a map from program counters to program counters, which is guranteed not to fail, as we must provide a proof that our policy at hand is a `good policy'.
    250276\begin{lstlisting}
    251277definition sigma:
Note: See TracChangeset for help on using the changeset viewer.