Changeset 984


Ignore:
Timestamp:
Jun 16, 2011, 4:16:41 PM (8 years ago)
Author:
mulligan
Message:

updates

File:
1 edited

Legend:

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

    r983 r984  
    218218                                         PseudoStatus $\rightarrow$ PseudoStatus := $\ldots$
    219219\end{lstlisting}
    220 Notice, here, that the emulation function for pseudoprograms takes an additional argument.
    221 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.
     220Notice, here, that the emulation function for assembly programs takes an additional argument.
     221This is a function that maps program counters (at the assembly level) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion.
    222222We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions.
    223223If 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.
     
    397397
    398398However, this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process.
    399 In particular, \texttt{fetch\_assembly\_pseudo2} says nothing about how
    400 
    401 An \texttt{internal\_pseudo\_address\_map} positions in the memory of a \texttt{PseudoStatus} with a physical memory address.
     399In particular, \texttt{fetch\_assembly\_pseudo2} says nothing about how memory addresses evolve during assembly.
     400Memory addresses in one memory space may be mapped to memory addresses in a completely different memory space during assembly.
     401To handle this problem, we need some more machinery.
     402
     403We use an \texttt{internal\_pseudo\_address\_map} for this purpose.
     404An \texttt{internal\_pseudo\_address\_map} associates positions in the memory of a \texttt{PseudoStatus} with a physical memory address:
    402405\begin{lstlisting}
    403406definition internal_pseudo_address_map := list (BitVector 8).
    404407\end{lstlisting}
    405408We use \texttt{internal\_pseudo\_address\_map}s to convert the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}.
     409The actual conversion process is performed by \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram}:\footnote{An associated set of axioms describe how \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} behaves.  This is a form of parametricity.  We don't care about the particulars of the conversion functions, as long as they behave in accordance with our axioms.}
     410
     411\begin{lstlisting}
     412axiom low_internal_ram_of_pseudo_low_internal_ram:
     413  internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7.
     414\end{lstlisting}
     415A similar axiom exists for high internal RAM.
     416
    406417Notice, the MCS-51's internal RAM is addressed with a 7-bit `byte'.
    407418% dpm: ugly English, fix
    408419The whole of the internal RAM space is addressed with bytes: the first bit is used to distinguish between the programmer addressing low and high internal memory.
    409 \begin{lstlisting}
    410 axiom low_internal_ram_of_pseudo_low_internal_ram:
    411   internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7.
    412 \end{lstlisting}
    413 A similar axiom exists for high internal RAM.
    414420
    415421Next, we are able to translate \texttt{PseudoStatus} records into \texttt{Status} records using \texttt{status\_of\_pseudo\_status}.
Note: See TracChangeset for help on using the changeset viewer.