Changeset 649 for Deliverables/D1.1


Ignore:
Timestamp:
Mar 8, 2011, 4:00:02 PM (9 years ago)
Author:
mulligan
Message:

Reworked presentation.

File:
1 moved

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.1/Presentations/WP4-dominic.tex

    r648 r649  
    4242\begin{frame}
    4343\frametitle{Work Package 4.1}
    44 Work Package 4.1 entitled `Executable Formal Semantics of Machine Code', described as follows (from Grant Agreement):
     44Work Package 4.1 entitled `Executable Formal Semantics of Machine Code':
    4545\begin{quote}
    4646Formal definition of the semantics of the target language. The semantics will be given in a functional (and hence executable) form, useful for testing, validation and project assessment.
    4747\end{quote}
     48Manpower: Dominic Mulligan ( hours) and Claudio Sacerdoti Coen ( hours).
    4849\end{frame}
    4950
     
    5253\begin{itemize}
    5354\item
    54 MCS-51 is our target processor.
    5555Commonly called the 8051 (has an immediate successor in the 8052).
    5656\item
    57 A popular 8-bit microprocessor introduced by Intel in the late 1970s.
    58 \item
    59 Still widely used in embedded systems, and widely manufactured (including within the EU).
    60 \item
    61 Is a relatively simple microprocessor especially suited to CerCo's aims.
    62 \item
    63 We can accurately predict how long an instruction will take to execute in cycles (i.e. no pipelining, caching etc.)
    64 We use timings from a Siemen's datasheet.
    65 Vary between manufacturers and models.
     57Popular 8-bit microprocessor from the late 1970s.
     58\item
     59Widely used and manufactured.
     60\item
     61Relatively simple microprocessor (especially suited for CerCo).
     62\item
     63Can accurately predict timing information in cycles.
    6664\end{itemize}
    6765\end{frame}
     
    7169\begin{itemize}
    7270\item
    73 I will not give an exhaustive introduction to the processor.
    74 I am going to reveal enough for you to understand what problems we faced in formalising it.
    75 \item
    76 The MCS-51 has a byzantine memory model.
    77 \item
    78 Memory spaces overlap, have different sizes, may not be present depending on model, can be addressed in multiple ways, and addressed with different sized pointers.
    79 \item
    80 Instruction set is non-orthogonal.
    81 For instance, \texttt{MOV} can take 16 combinations of addressing mode out of a possible 300+.
     71No exhaustive introduction.
     72Reveal enough to understand what problems we faced.
     73\item
     74Byzantine memory model.
     75\item
     76Overlap, have different sizes, may not be present depending on model, addressed in multiple ways, addressed with different sized pointers.
     77\item
     78Non-orthogonal instruction set.
     79\texttt{MOV} takes 16 combinations of addressing mode (possible 300+)s.
    8280\end{itemize}
    8381\end{frame}
     
    8785\begin{itemize}
    8886\item
    89 Instruction set contains three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used).
    90 \item
    91 These differ in the size of permissible offset and the size in bytes of instruction.
    92 \item
    93 MCS-51 also has various timers, UART I/O and interrupts.
    94 Succesor 8052 adds additional timers.
    95 \item
    96 Interrupts are simpler than a modern processor, as flags can be used to manually handle errors.
     87Three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used).
     88\item
     89Differ in the size of permissible offset and the size in bytes of instruction.
     90\item
     91Also has various timers, UART I/O and interrupts.
     928052 adds additional timers.
     93\item
     94Interrupts are simple.
     95Flags can be used to manually handle errors.
    9796\end{itemize}
    9897\end{frame}
     
    10099\begin{frame}
    101100\frametitle{Development strategy}
    102 We built two emulators for the processor.
    103 
    104 The first was written in O'Caml.
    105 This allowed us to `iron out' issues in the design and implementation, and make rapid changes in O'Caml's more permissive type system.
    106 We made use of O'Caml's ability to perform I/O for debugging purposes.
    107 
    108 When we were happy with the O'Caml emulator, we moved to Matita.
    109 Matita's language is lexically similar to O'Caml, so swathes of code could be copy-pasted with little additional effort.
     101\begin{itemize}
     102\item
     103Have two emulators.
     104\item
     105First in O'Caml.
     106`Iron out' issues.
     107\item
     108I/O for debugging purposes.
     109\item
     110Then we moved to Matita.
     111Lexically similar to O'Caml: code copy-pasted.
     112\end{itemize}
    110113\end{frame}
    111114
     
    114117\begin{itemize}
    115118\item
    116 Unconditional jumps a problem, as offset has to be computed ahead of time.
    117 \item
    118 This is problematic for separate compilation, and also for prototype C compiler.
    119 \item
    120 Much better to implement pseudoinstructions which are `assembled away'.
     119Unconditional jumps: offset computed ahead of time.
     120\item
     121Problems: separate compilation, prototype C compiler.
     122\item
     123Add pseudoinstructions and `assemble away'.
    121124\item
    122125Introduce labels and cost labels (for cost traces).
    123126\item
    124 Then introduce pseudoinstructions like \texttt{Jump} for unconditional jumping to labels: no offset calculation required beforehand.
    125 \item
    126 Other pseudoinstructions introduced: \texttt{Mov} for moving arbitrary (16 bit) data stored at a label (global vars) and conditional jumps to labels.
    127 \item
    128 Our assembly language similar to that of SDCC.
     127Introduce pseudoinstructions.
     128\texttt{Jump}: unconditional jump to labels.
     129\item
     130Other pseudoinstructions introduced: \texttt{Mov} moves (16 bit) data stored at a label (global vars).
     131Conditional jumps to labels.
     132\item
     133Assembly language similar to that of SDCC.
    129134\end{itemize}
    130135\end{frame}
     
    132137\begin{frame}[fragile]
    133138\frametitle{Polymorphic variants and phantom types}
    134 The instruction set is highly non-orthogonal.
    135 We used polymorphic variants and phantom types to capture this non-orthogonality in the type system.
     139Instruction set is highly non-orthogonal.
     140Polymorphic variants and phantom types used to capture this non-orthogonality.
    136141For instance:
    137142
     
    155160\begin{frame}[fragile]
    156161\frametitle{Use of dependent types I}
    157 This approach worked well in O'Caml, but Matita does not have polymorphic variants, so we need a substitute.
     162Worked well in O'Caml, Matita does not have polymorphic variants.
    158163We use dependent types.
    159164
     
    166171\end{lstlisting}
    167172\end{small}
    168 And another type \texttt{addressing\_mode\_tag} of `tags' whose constructors are in correspondence with those of \texttt{addressing\_mode}.
     173Another type \texttt{addressing\_mode\_tag} of `tags'.
     174Constructors are in correspondence with those of \texttt{addressing\_mode}.
    169175\end{frame}
    170176
    171177\begin{frame}[fragile]
    172178\frametitle{Use of dependent types II}
    173 We use vectors of \texttt{addressing\_mode\_tag}s in our type signatures for instructions.
     179Use vectors of \texttt{addressing\_mode\_tag}s in type signatures for instructions.
    174180For instance:
    175181\begin{small}
     
    183189\end{small}
    184190We need: an \emph{ad hoc} $\Sigma$ type and two coercions.
    185 One coercion automatically opens up a proof obligation when it is used, which requires some lemmas.
    186 
    187 These lemmas and automation close all proof obligations generated (over 300 in typechecking the main interpreter function).
     191One coercion opens up a proof obligation when it is used.
     192Requires some lemmas.
     193
     194Lemmas and automation close proof obligations generated (300+ in typechecking interpreter function).
    188195\end{frame}
    189196
    190197\begin{frame}
    191198\frametitle{Overlapping memory spaces and addressing modes}
    192 MCS-51 memory spaces overlap, and can be addressed using different modes and sized pointers.
    193 The `status' record models memory merely as disjoint spaces, using a `tries with holes' datastructure.
    194 
    195 All complications to do with overlapping are handled by \texttt{set\_arg\_XX} and \texttt{get\_arg\_XX} for \texttt{XX} = 1, 8, 16.
    196 These functions make use of the aforementioned dependent type trick.
     199\begin{itemize}
     200\item
     201Memory spaces overlap, can be addressed with different modes and pointers.
     202\item
     203`Status' record models memory as disjoint spaces.
     204\item
     205`Tries with holes' datastructure (dependent types).
     206\item
     207Complications with overlapping handled by \texttt{set\_arg\_XX} and \texttt{get\_arg\_XX} for \texttt{XX} = 1, 8, 16.
     208\item
     209Make use of dependent type trick.
     210\end{itemize}
    197211\end{frame}
    198212
     
    204218Multiple data sheets from different manufacturers (errors found!)
    205219\item
    206 O'Caml output to Intel HEX for loading into third party tools, and input for use with SDCC.
    207 \item
    208 O'Caml produced trace files with processor status after every execution step, every opcode tested.
    209 \item
    210 Matita formalisation is also executable, and traces can be compared with O'Caml.
     220Output to Intel HEX.
     221Loading into third party tools.
     222\item
     223O'Caml trace files with processor status after every execution step.
     224Every opcode tested.
     225\item
     226Matita formalisation is also executable.
     227\item
     228Traces can be compared with O'Caml.
    211229\end{itemize}
    212230\end{frame}
     
    214232\begin{frame}
    215233\frametitle{What is implemented}
    216 In O'Caml we implemented the emulator proper, associated assembler, supprting debugging code (for loading and outputting Intel HEX), and also have (untested) code for timers, interrupts and I/O.
    217 
    218 In Matita, we have the emulator proper and associated assembler.
    219 We have yet to port the timers and I/O, preferring to focus on the core emulator.
     234\begin{itemize}
     235\item
     236In O'Caml: emulator proper, associated assembler, supprting debugging code (Intel HEX), (untested) code for timers, interrupts and I/O.
     237\item
     238In Matita: emulator proper and associated assembler.
     239\item
     240Yet to port the timers and I/O, preferring to focus on the core emulator.
     241\end{itemize}
    220242\end{frame}
    221243
Note: See TracChangeset for help on using the changeset viewer.