# Changeset 532

Ignore:
Timestamp:
Feb 16, 2011, 3:38:43 PM (8 years ago)
Message:

after much faffing, top of minipages now align correctly

File:
1 edited

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

 r529 {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on}, morekeywords={whd,normalize,elim,cases,destruct}, morekeywords={type,of,val}, morekeywords={type,of,val,assert,let,function}, mathescape=true, } \label{subsect.representation.integers} Integers are represented using bitvectors, i.e. fixed length vectors of booleans. In our O'Caml emulator, we faked' bitvectors using phantom types and polymorphic variants, like so: \begin{lstlisting} type bit = bool \begin{figure}[t] \begin{minipage}[t]{0.5\textwidth} \vspace{0pt} \begin{lstlisting} type 'a vect = bit list type word = [Sixteen] vect type byte = [Eight] vect \end{lstlisting} Using this technique, we can provide precise typings for utility and arithmetic functions giving us some stronger guarantees of type safety. For instance, functions that split \texttt{word}s into their constituent \texttt{byte}s: \begin{lstlisting} val from_word: word -> byte * byte \end{lstlisting} let from_nibble = function [b1; b2; b3; b4] -> b1,b2,b3,b4 | _ -> assert false \end{lstlisting} \end{minipage} \quad \begin{minipage}[t]{0.5\textwidth} \vspace{0pt} \begin{lstlisting} type 'a vect type word = [Sixteen] vect type byte = [Eight] vect val from_nibble: nibble -> bit*bit*bit*bit \end{lstlisting} \end{minipage} \caption{Sample of O'Caml implementation and interface for bitvectors module} \label{fig.ocaml.implementation.bitvectors} \end{figure} Integers are represented using bitvectors, i.e. fixed length vectors of booleans. In our O'Caml emulator, we faked' bitvectors using phantom types and polymorphic variants, as in Figure~\ref{fig.ocaml.implementation.bitvectors}. From within the bitvector module (left column) bitvectors are just lists of bits. However, the module's interface (right column) hides this implementation completely. In Matita, we are able to use the full power of dependent types to define real' bitvectors: \begin{lstlisting} Both the Matita and O'Caml emulators follows the classic fetch-decode-execute' model of processor operation. The most important functions in the Matita emulator are highlighted below. \begin{lstlisting} definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat := ... \end{lstlisting} The next instruction, indexed by the program counter, is fetched from code memory with \texttt{fetch}. The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}. An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned. These 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. \begin{lstlisting} definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ... definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ... \end{lstlisting} A single instruction is assembled into its corresponding bit encoding with \texttt{assembly1}: A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is also produced. \begin{lstlisting} definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ... definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ... \end{lstlisting} A single execution step of the processor is evaluated using \texttt{execute\_1}, mapping a \texttt{Status} to a \texttt{Status}: \begin{lstlisting} definition execute_1: Status → Status := ... definition execute_1: Status $\rightarrow$ Status := ... \end{lstlisting} Multiple steps of processor execution are implemented in \texttt{execute}, which wraps \texttt{execute\_1}: let rec execute (n: nat) (s: Status) on n: Status := ... \end{lstlisting} This differs slightly from the design of the O'Caml emulator, which executed a program indefinitely, and also accepted a callback function as an argument, which could `witness' the execution as it happened, and providing a print-out of the processor state, and other debugging information. Due to Matita's requirement that all functions be strongly normalizing, \texttt{execute} cannot execute a program indefinitely, and must execute a fixed number of steps. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.