Changeset 968 for src/ASM/CPP2011/cpp-2011.tex

Timestamp:

Jun 15, 2011, 4:32:57 PM (10 years ago)

Author:

mulligan

Message:

work on paper

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (3 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -213 +213 @@
 Notice, here, that the emulation function for pseudoprograms takes an additional argument.
 This 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.
-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.
+We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions.
+If 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.
+
+The 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.
 This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
 During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es.
@@ -233 +236 @@
 \label{subsect.policies}
 
-\begin{lstlisting}
-inductive jump_length: Type[0] ≝
+Policies exist to dictate how conditional and unconditional jumps at the assembly level should be expanded into machine code instructions.
+Using policies, we are able to completely decouple the decision over how jumps are expanded with the act of expansion, simplifying our proofs.
+As 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:
+\begin{lstlisting}
+inductive jump_length: Type[0] :=
   | short_jump: jump_length
   | medium_jump: jump_length
@@ -240 +246 @@
 \end{lstlisting}
 
-\begin{lstlisting}
-definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
-\end{lstlisting}
-
-\begin{lstlisting}
-definition policy_ok := λpolicy.λp. sigma_safe policy p <> None ....
-\end{lstlisting}
-
+A \texttt{jump\_expansion\_policy} is a map from \texttt{Word}s to \texttt{jump\_length}s, implemented as a trie.
+Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump.
+\begin{lstlisting}
+definition jump_expansion_policy := BitVectorTrie jump_length 16.
+\end{lstlisting}
+
+Next, we require a series of `sigma' functions.
+These 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.
+At the heart of this process is \texttt{sigma0} which traverses an assembly program building maps from program counter to program counter.
+This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails:
+\begin{lstlisting}
+definition sigma0: pseudo_assembly_program
+                   $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
+\end{lstlisting}
+
+We eventually lift this to functions from program counters to program counters:
+\begin{lstlisting}
+definition sigma_safe: pseudo_assembly_program
+                       $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
+\end{lstlisting}
+
+Now, it's possible to define what a `good policy' is i.e. one that does not cause \texttt{sigma\_safe} to fail.
+As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
+\begin{lstlisting}
+definition policy_ok := $\lambda$policy. $\lambda$p. sigma_safe policy p $\neq$ None $\ldots$.
+\end{lstlisting}
+
+Finally, 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'.
 \begin{lstlisting}
 definition sigma: