Changeset 1010 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 20, 2011, 6:18:39 PM (8 years ago)
Author:
mulligan
Message:

more added, finished up to end of subsect 3.2

File:
1 edited

Legend:

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

    r1009 r1010  
    300300These 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.
    301301At the heart of this process is \texttt{sigma0} which traverses an assembly program building maps from pseudo program counters to program counters.
    302 This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails:
     302This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction\_safe} fails, which happens if a jump pseudoinstruction is expanded incorrectly:
    303303\begin{lstlisting}
    304304definition sigma0: pseudo_assembly_program
    305305  $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
    306306\end{lstlisting}
    307 We eventually lift this to functions from program counters to program counters:
     307Here, the returned \texttt{BitVectorTrie} is a map between pseudo program counters and program counters, and is constructed by successively expanding pseudoinstructions and incrementing the two program counters the requisite amount to keep them in correct correspondence.
     308The two natural numbers returned are the maximum values that the two program counters attained.
     309
     310We eventually lift this to functions from pseudo program counters to program counters, implemented as \texttt{Word}s:
    308311\begin{lstlisting}
    309312definition sigma_safe:
    310313  pseudo_assembly_program $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
    311314\end{lstlisting}
    312 Now, it's possible to define what a `good policy' is i.e. one that does not cause \texttt{sigma\_safe} to fail.
     315Now, it's possible to define what a `good policy' is.
     316A policy is deemed good when it prevents \texttt{sigma\_safe} from ever failing.
    313317As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
    314318\begin{lstlisting}
    315319definition policy_ok := $\lambda$p. sigma_safe p $\neq$ None $\ldots$.
    316320\end{lstlisting}
    317 Finally, we obtain \texttt{sigma}, a map from program counters to program counters, which is guranteed not to fail as we internally provide a that
    318 \begin{lstlisting}
    319 definition sigma: pseudo_assembly_program $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
     321Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters which incorporates, depending also on a policy.
     322This is a thin shell around \texttt{sigma\_safe}, and dispenses with the option type via a proof that \texttt{sigma\_safe} never fails under the assumption that a supplied policy is correct:
     323\begin{lstlisting}
     324definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
    320325\end{lstlisting}
    321326
     
    328333Using our policies, we now work toward proving the total correctness of the assembler.
    329334By total correctness, we mean that the assembly process does not change the semantics of an assembly program.
    330 Naturally, this necessitates keeping some sort of correspondence between program counters at the assembly level, and program counters at the machine code level.
     335Naturally, this necessitates keeping some sort of correspondence between addresses at the assembly level and addresses at the machine code level.
    331336For this, we use the \texttt{sigma} machinery defined at the end of Subsection~\ref{subsect.policies}.
    332337
Note: See TracChangeset for help on using the changeset viewer.