Changeset 528


Ignore:
Timestamp:
Feb 16, 2011, 11:14:29 AM (6 years ago)
Author:
mulligan
Message:

Removed all \begin{quote} .. \end{quote} around code snippets for better layout. Reduced to 14 pages as a result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r527 r528  
    293293Instead, we chose to use a modified form of trie, where paths are represented by bitvectors.
    294294As bitvectors were widely used in our implementation already for representing integers, this worked well:
    295 \begin{quote}
    296295\begin{lstlisting}
    297296inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
     
    300299| Stub: ∀n. BitVectorTrie A n.
    301300\end{lstlisting}
    302 \end{quote}
    303301Here, \texttt{Stub} is a constructor that can appear at any point in our tries.
    304302It internalises the notion of `uninitialized data'.
     
    343341
    344342The internal state of our Matita emulator is represented as a record:
    345 \begin{quote}
    346343\begin{lstlisting}
    347344record Status: Type[0] ≝
     
    357354}.
    358355\end{lstlisting}
    359 \end{quote}
    360356This record neatly encapsulates the current memory contents, the program counter, the state of the current SFRs, and so on.
    361357One peculiarity is the packing of the 24 combined SFRs into fixed length vectors.
     
    364360Both the Matita and O'Caml emulators follows the classic `fetch-decode-execute' model of processor operation.
    365361The most important functions in the Matita emulator are highlighted below.
    366 \begin{quote}
    367362\begin{lstlisting}
    368363definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat := ...
    369364\end{lstlisting}
    370 \end{quote}
    371365The next instruction, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
    372366An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
    373367These costs are taken from a Siemen's data sheet for the MCS-51, and will likely vary across manufacturers and particular derivatives of the processor.
    374 \begin{quote}
    375368\begin{lstlisting}
    376369definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ...
    377370\end{lstlisting}
    378 \end{quote}
    379371A single instruction is assembled into its corresponding bit encoding with \texttt{assembly1}:
    380 \begin{quote}
    381372\begin{lstlisting}
    382373definition assembly1: instruction $\rightarrow$ list Byte := ...
    383374\end{lstlisting}
    384 \end{quote}
    385375An assembly program, consisting of a preamble containing global data, and a list of (pseudo)instructions, is assembled using \texttt{assembly}.
    386376Pseudoinstructions and labels are eliminated in favour of concrete instructions from the MCS-51 instruction set.
    387377A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is also produced.
    388 \begin{quote}
    389378\begin{lstlisting}
    390379definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ...
    391380\end{lstlisting}
    392 \end{quote}
    393381A single execution step of the processor is evaluated using \texttt{execute\_1}, mapping a \texttt{Status} to a \texttt{Status}:
    394 \begin{quote}
    395382\begin{lstlisting}
    396383definition execute_1: Status → Status := ...
    397384\end{lstlisting}
    398 \end{quote}
    399385Multiple steps of processor execution are implemented in \texttt{execute}, which wraps \texttt{execute\_1}:
    400 \begin{quote}
    401386\begin{lstlisting}
    402387let rec execute (n: nat) (s: Status) on n: Status := ...
    403388\end{lstlisting}
    404 \end{quote}
    405389
    406390%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    417401Such non-orthogonality in the instruction set was handled with the use of polymorphic variants in the O'Caml emulator.
    418402For instance, we introduced types corresponding to each addressing mode:
    419 \begin{quote}
    420403\begin{lstlisting}
    421404type direct = [ `DIRECT of byte ]
     
    423406...
    424407\end{lstlisting}
    425 \end{quote}
    426408Which were then used in our inductive datatype for assembly instructions, as follows:
    427 \begin{quote}
    428409\begin{lstlisting}
    429410type 'addr preinstruction =
     
    440421...
    441422\end{lstlisting}
    442 \end{quote}
    443423Here, \texttt{union6} is a disjoint union type, defined as follows:
    444 \begin{quote}
    445424\begin{lstlisting}
    446425type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a | ... | `U6 of 'f ]
    447426\end{lstlisting}
    448 \end{quote}
    449427For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
    450428
     
    455433
    456434We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against:
    457 \begin{quote}
    458435\begin{lstlisting}
    459436inductive addressing_mode: Type[0] ≝
     
    462439...
    463440\end{lstlisting}
    464 \end{quote}
    465441We also wished to express in the type of functions the \emph{impossibility} of pattern matching against certain constructors.
    466442In order to do this, we introduced an inductive type of addressing mode `tags'.
    467443The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}:
    468 \begin{quote}
    469444\begin{lstlisting}
    470445inductive addressing_mode_tag : Type[0] ≝
     
    473448...
    474449\end{lstlisting}
    475 \end{quote}
    476450A function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag} is provided, as follows:
    477 \begin{quote}
    478451\begin{lstlisting}
    479452let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d ≝
     
    483456...
    484457\end{lstlisting}
    485 \end{quote}
    486458We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
    487 \begin{quote}
    488459\begin{lstlisting}
    489460let rec is_in (n) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l ≝
     
    493464     is_a he A $\vee$ is_in ? tl A ].
    494465\end{lstlisting}
    495 \end{quote}
    496 Here \texttt{VEmpty} and \texttt{VCons} are the two constructors of the \texttt{Vector} data type, and $\mathtt{\vee}$ is inclusive disjunction on Booleans.
    497 \begin{quote}
     466Here $\mathtt{\vee}$ is inclusive disjunction on the \texttt{bool} datatype.
    498467\begin{lstlisting}
    499468record subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
     
    503472}.
    504473\end{lstlisting}
    505 \end{quote}
    506474We can now provide an inductive type of preinstructions with precise typings:
    507 \begin{quote}
    508475\begin{lstlisting}
    509476inductive preinstruction (A: Type[0]): Type[0] ≝
     
    512479...
    513480\end{lstlisting}
    514 \end{quote}
    515481Here $\llbracket - \rrbracket$ is syntax denoting a vector.
    516482We see that the constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), and the second being one of a register, direct, indirect or data addressing mode.
     
    521487The previous machinery allows us to state in the type of a function what addressing modes that function expects.
    522488For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
    523 \begin{quote}
    524489\begin{lstlisting}
    525490definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
     
    537502     ] (subaddressing_modein $\ldots$ a).
    538503\end{lstlisting}
    539 \end{quote}
    540504All other cases are discharged by the catch-all at the bottom of the match expression.
    541505Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
     
    558522
    559523To accurately model timers, we must modify the central \texttt{status} record of the emulator to keep track of the current time:
    560 \begin{quote}
    561524\begin{lstlisting}
    562525type time = int
    563526type status = { ... clock: time; ... }
    564527\end{lstlisting}
    565 \end{quote}
    566528Before every execution step, the \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute.
    567529The processor then executes the instruction, followed by the code implementing the timers.
Note: See TracChangeset for help on using the changeset viewer.