Changeset 574 for Deliverables


Ignore:
Timestamp:
Feb 18, 2011, 1:32:46 PM (11 years ago)
Author:
mulligan
Message:

Tweaked the document, and removed all junk from the end of the file.

File:
1 edited

Legend:

Unmodified
Added
Removed

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

    r572 r574  
    6666
    6767\begin{abstract}
    68 We summarise our formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.
     68We summarise the formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.
    6969The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
    7070
    7171The formalisation proceeded in two stages, first implementing an O'Caml prototype, for quickly `ironing out' bugs, and then porting the O'Caml emulator to Matita.
    7272Though mostly straight-forward, this porting presented multiple problems.
    73 Of particular interest is how we handled the unorthoganality of the MSC-51's instruction set.
     73Of particular interest is how the unorthoganality of the MSC-51's instruction set is handled.
    7474In O'Caml, this was handled with polymorphic variants.
    7575In Matita, we achieved the same effect with a non-standard use of dependent types.
    … …  
    140140The latter is what we describe in this paper.
    141141The focus of the formalisation has been on capturing the intensional behaviour of the processor.
    142 However, the design of the MCS-51 itself has caused problems in our formalisation.
     142However, the design of the MCS-51 itself has caused problems in the formalisation.
    143143For example, the MCS-51 has a highly unorthogonal instruction set.
    144144To cope with this unorthogonality, and to produce an executable specification, we rely on Matita's dependent types.
    … …  
    152152For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C~\cite{sdcc:2010}, and other compilers for BASIC, Forth and Modula-2 are also extant.
    153153An open source emulator for the processor, MCU 8051 IDE, is also available~\cite{mcu8051ide:2010}.
    154 Both MCU 8051 IDE and SDCC were used in for validating our formalisation.
     154Both MCU 8051 IDE and SDCC were used in for validating the formalisation.
    155155
    156156\begin{figure}[t]
    … …  
    277277\paragraph{Overview of paper}\quad
    278278In Section~\ref{sect.design.issues.formalisation} we discuss design issues in the development of the formalisation.
    279 In Section~\ref{sect.validation} we discuss how we validated the design and implementation of our emulator to ensure that what we formalised was an accurate model of an MCS-51 series microprocessor.
     279In Section~\ref{sect.validation} we discuss how we validated the design and implementation of the emulator to ensure that what we formalised was an accurate model of an MCS-51 series microprocessor.
    280280In Section~\ref{sect.related.work} we describe previous work, with an eye toward describing its relation with the work described herein.
    281281In Section~\ref{sect.conclusions} we conclude.
    … …  
    296296\label{subsect.development.strategy}
    297297
    298 Our implementation progressed in two stages.
     298The implementation progressed in two stages.
    299299We began with an emulator written in O'Caml to `iron out' any bugs in the design and implementation.
    300300O'Caml's ability to perform file I/O also eased debugging and validation.
    … …  
    340340The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits), and also more exoteric quantities (7, 3 and 9-bits).
    341341To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans.
    342 In our O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
     342In the O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
    343343From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
    344344However, the module's interface (right column) enforces size invariants in the rest of the code.
    … …  
    364364
    365365The MCS-51 has numerous disjoint memory spaces addressed by differently sized pointers.
    366 In our O'Caml implementation, we use a map data structure (from the standard library) for each space.
     366In the O'Caml implementation, we use a map data structure (from the standard library) for each space.
    367367Matita's standard library is small, and does not contain a generic map data structure.
    368368We had the opportunity of crafting a dependently typed special-purpose data structure for the job to enforce the correspondence between the size of pointer and the size of the memory space.
    … …  
    370370
    371371We picked a modified form of trie of fixed height $h$.
    372 Paths are represented by bitvectors (already used in our implementation for addresses and registers) of length $h$:
     372Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$:
    373373\begin{lstlisting}
    374374inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
    … …  
    405405A pseudoinstruction \texttt{Mov} moves (16-bit) data stored at a label into the MCS-51's one 16-bit register, \texttt{DPTR}.
    406406
    407 Our pseudoinstructions and labels induce an assembly language similar to that of SDCC's.
     407The pseudoinstructions and labels induce an assembly language similar to that of SDCC's.
    408408All pseudoinstructions and labels are `assembled away' prior to program execution.
    409409Jumps are computed in two stages.
    … …  
    491491...
    492492\end{lstlisting}
    493 Which were then combined in our inductive datatype for assembly instructions using the union operator `$|$':
     493Which were then combined in the inductive datatype for assembly preinstructions using the union operator `$|$':
    494494\begin{lstlisting}
    495495type 'addr preinstruction =
    … …  
    567567Proof obligations require us to state and prove a few auxilliary lemmas related to the transitivity of subtyping.
    568568For instance, an \texttt{addressing\_mode} that belongs to an allowed set also belongs to any one of its supersets.
    569 At the moment, Matita's automation exploits these lemmas to completely solve all the proof obligations opened in our formalisation.
     569At the moment, Matita's automation exploits these lemmas to completely solve all the proof obligations opened in the formalisation.
    570570The \texttt{execute\_1} function, for instance, opens over 200 proof obligations during type checking.
    571571
    … …  
    631631We leave the computation of the delay time to the environment.
    632632
    633 We use only the P1 and P3 lines despite the MCS-51 having four output lines, P0--P3.
     633We use only the P1 and P3 lines despite the MCS-51 having 4 output lines, P0--P3.
    634634This is because P0 and P2 become inoperable if the processor is equipped with XRAM (we assume it is).
    635635
    … …  
    668668Intel HEX is a standard format that all compilers targetting the MCS-51, and similar processors, produce.
    669669It is essentially a snapshot of the processor's code memory in compressed form.
    670 Using this we were able to compile C programs with SDCC and load the resulting program directly into our emulator's code memory, ready for execution.
    671 Further, we can produce a HEX file from our emulator's code memory for loading into third party tools.
     670Using this we were able to compile C programs with SDCC and load the resulting program directly into the emulator's code memory, ready for execution.
     671Further, we can produce a HEX file from the emulator's code memory for loading into third party tools.
    672672After each step of execution, we can print out both the instruction that had been executed and a snapshot of the processor's state, including all flags and register contents.
    673673For example:
    … …  
    696696
    697697We further used MCU 8051 IDE as a reference, which allows a user to step through an assembly program one instruction at a time.
    698 Using our execution traces, we were able to step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator.
    699 
    700 Our Matita formalisation was largely copied from the O'Caml source code, apart from the changes already mentioned.
     698Using these execution traces, we were able to step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator.
     699
     700The Matita formalisation was largely copied from the O'Caml source code, apart from the changes already mentioned.
    701701However, as the Matita emulator is executable, we could perform further validation by comparing the trace of a program's execution in the Matita emulator with the trace of the same program in the O'Caml emulator.
    702702
    … …  
    795795
    796796\end{document}
    797 
    798 \newpage
    799 
    800 \appendix
    801 
    802 \section{Listing of main O'Caml functions}
    803 \label{sect.listing.main.ocaml.functions}
    804 
    805 \subsubsection{From \texttt{ASMInterpret.ml(i)}}
    806 
    807 \begin{center}
    808 \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
    809 Name & Description \\
    810 \hline
    811 \texttt{assembly} & Assembles an abstract syntax tree representing an 8051 assembly program into a list of bytes, its compiled form. \\
    812 \texttt{initialize} & Initializes the emulator status. \\
    813 \texttt{load} & Loads an assembled program into the emulator's code memory. \\
    814 \texttt{fetch} & Fetches the next instruction, and automatically increments the program counter. \\
    815 \texttt{execute} & Emulates the processor.  Accepts as input a function that pretty prints the emulator status after every emulation loop. \\
    816 \end{tabular*}
    817 \end{center}
    818 
    819 \subsubsection{From \texttt{ASMCosts.ml(i)}}
    820 
    821 \begin{center}
    822 \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
    823 Name & Description \\
    824 \hline
    825 \texttt{compute} & Computes a map associating costings to basic blocks in the program.
    826 \end{tabular*}
    827 \end{center}
    828 
    829 \subsubsection{From \texttt{IntelHex.ml(i)}}
    830 
    831 \begin{center}
    832 \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
    833 Name & Description \\
    834 \hline
    835 \texttt{intel\_hex\_of\_file} & Reads in a file and parses it if in Intel IHX format, otherwise raises an exception. \\
    836 \texttt{process\_intel\_hex} & Accepts a parsed Intel IHX file and populates a hashmap (of the same type as code memory) with the contents.
    837 \end{tabular*}
    838 \end{center}
    839 
    840 \subsubsection{From \texttt{Physical.ml(i)}}
    841 
    842 \begin{center}
    843 \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
    844 Name & Description \\
    845 \hline
    846 \texttt{subb8\_with\_c} & Performs an eight bit subtraction on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\
    847 \texttt{add8\_with\_c} & Performs an eight bit addition on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\
    848 \texttt{dec} & Decrements an eight bit bitvector with underflow, if necessary. \\
    849 \texttt{inc} & Increments an eight bit bitvector with overflow, if necessary.
    850 \end{tabular*}
    851 \end{center}
    852 
    853 \newpage
    854 
    855 \section{Listing of main Matita functions}
    856 \label{sect.listing.main.matita.functions}
    857 
    858 \subsubsection{From \texttt{Arithmetic.ma}}
    859 
    860 \begin{center}
    861 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
    862 Title & Description \\
    863 \hline
    864 \texttt{add\_n\_with\_carry} & Performs an $n$ bit addition on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\
    865 \texttt{sub\_8\_with\_carry} & Performs an eight bit subtraction on bitvectors. The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\
    866 \texttt{half\_add} & Performs a standard half addition on bitvectors, returning the result and carry bit. \\
    867 \texttt{full\_add} & Performs a standard full addition on bitvectors and a carry bit, returning the result and a carry bit.
    868 \end{tabular*}
    869 \end{center}
    870 
    871 \subsubsection{From \texttt{Assembly.ma}}
    872 
    873 \begin{center}
    874 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
    875 Title & Description \\
    876 \hline
    877 \texttt{assemble1} & Assembles a single 8051 assembly instruction into its memory representation. \\
    878 \texttt{assemble} & Assembles an 8051 assembly program into its memory representation.\\
    879 \texttt{assemble\_unlabelled\_program} &\\& Assembles a list of (unlabelled) 8051 assembly instructions into its memory representation.
    880 \end{tabular*}
    881 \end{center}
    882 
    883 \subsubsection{From \texttt{BitVectorTrie.ma}}
    884 
    885 \begin{center}
    886 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
    887 Title & Description \\
    888 \hline
    889 \texttt{lookup} & Returns the data stored at the end of a particular path (a bitvector) from the trie.  If no data exists, returns a default value. \\
    890 \texttt{insert} & Inserts data into a tree at the end of the path (a bitvector) indicated.  Automatically expands the tree (by filling in stubs) if necessary.
    891 \end{tabular*}
    892 \end{center}
    893 
    894 \subsubsection{From \texttt{DoTest.ma}}
    895 
    896 \begin{center}
    897 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
    898 Title & Description \\
    899 \hline
    900 \texttt{execute\_trace} & Executes an assembly program for a fixed number of steps, recording in a trace which instructions were executed.
    901 \end{tabular*}
    902 \end{center}
    903 
    904 \subsubsection{From \texttt{Fetch.ma}}
    905 
    906 \begin{center}
    907 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
    908 Title & Description \\
    909 \hline
    910 \texttt{fetch} & Decodes and returns the instruction currently pointed to by the program counter and automatically increments the program counter the required amount to point to the next instruction. \\
    911 \end{tabular*}
    912 \end{center}
    913 
    914 \subsubsection{From \texttt{Interpret.ma}}
    915 
    916 \begin{center}
    917 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
    918 Title & Description \\
    919 \hline
    920 \texttt{execute\_1} & Executes a single step of an 8051 assembly program. \\
    921 \texttt{execute} & Executes a fixed number of steps of an 8051 assembly program.
    922 \end{tabular*}
    923 \end{center}
    924 
    925 \subsubsection{From \texttt{Status.ma}}
    926 
    927 \begin{center}
    928 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
    929 Title & Description \\
    930 \hline
    931 \texttt{load} & Loads an assembled 8051 assembly program into code memory.
    932 \end{tabular*}
    933 \end{center}
    934 \end{document}
Note: See TracChangeset for help on using the changeset viewer.