# Changeset 649

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

Reworked presentation.

File:
1 moved

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

 r648 \begin{frame} \frametitle{Work Package 4.1} Work Package 4.1 entitled Executable Formal Semantics of Machine Code', described as follows (from Grant Agreement): Work Package 4.1 entitled Executable Formal Semantics of Machine Code': \begin{quote} Formal 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. \end{quote} Manpower: Dominic Mulligan ( hours) and Claudio Sacerdoti Coen ( hours). \end{frame} \begin{itemize} \item MCS-51 is our target processor. Commonly called the 8051 (has an immediate successor in the 8052). \item A popular 8-bit microprocessor introduced by Intel in the late 1970s. \item Still widely used in embedded systems, and widely manufactured (including within the EU). \item Is a relatively simple microprocessor especially suited to CerCo's aims. \item We can accurately predict how long an instruction will take to execute in cycles (i.e. no pipelining, caching etc.) We use timings from a Siemen's datasheet. Vary between manufacturers and models. Popular 8-bit microprocessor from the late 1970s. \item Widely used and manufactured. \item Relatively simple microprocessor (especially suited for CerCo). \item Can accurately predict timing information in cycles. \end{itemize} \end{frame} \begin{itemize} \item I will not give an exhaustive introduction to the processor. I am going to reveal enough for you to understand what problems we faced in formalising it. \item The MCS-51 has a byzantine memory model. \item 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. \item Instruction set is non-orthogonal. For instance, \texttt{MOV} can take 16 combinations of addressing mode out of a possible 300+. No exhaustive introduction. Reveal enough to understand what problems we faced. \item Byzantine memory model. \item Overlap, have different sizes, may not be present depending on model, addressed in multiple ways, addressed with different sized pointers. \item Non-orthogonal instruction set. \texttt{MOV} takes 16 combinations of addressing mode (possible 300+)s. \end{itemize} \end{frame} \begin{itemize} \item Instruction set contains three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used). \item These differ in the size of permissible offset and the size in bytes of instruction. \item MCS-51 also has various timers, UART I/O and interrupts. Succesor 8052 adds additional timers. \item Interrupts are simpler than a modern processor, as flags can be used to manually handle errors. Three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used). \item Differ in the size of permissible offset and the size in bytes of instruction. \item Also has various timers, UART I/O and interrupts. 8052 adds additional timers. \item Interrupts are simple. Flags can be used to manually handle errors. \end{itemize} \end{frame} \begin{frame} \frametitle{Development strategy} We built two emulators for the processor. The first was written in O'Caml. This allowed us to iron out' issues in the design and implementation, and make rapid changes in O'Caml's more permissive type system. We made use of O'Caml's ability to perform I/O for debugging purposes. When we were happy with the O'Caml emulator, we moved to Matita. Matita's language is lexically similar to O'Caml, so swathes of code could be copy-pasted with little additional effort. \begin{itemize} \item Have two emulators. \item First in O'Caml. Iron out' issues. \item I/O for debugging purposes. \item Then we moved to Matita. Lexically similar to O'Caml: code copy-pasted. \end{itemize} \end{frame} \begin{itemize} \item Unconditional jumps a problem, as offset has to be computed ahead of time. \item This is problematic for separate compilation, and also for prototype C compiler. \item Much better to implement pseudoinstructions which are assembled away'. Unconditional jumps: offset computed ahead of time. \item Problems: separate compilation, prototype C compiler. \item Add pseudoinstructions and assemble away'. \item Introduce labels and cost labels (for cost traces). \item Then introduce pseudoinstructions like \texttt{Jump} for unconditional jumping to labels: no offset calculation required beforehand. \item Other pseudoinstructions introduced: \texttt{Mov} for moving arbitrary (16 bit) data stored at a label (global vars) and conditional jumps to labels. \item Our assembly language similar to that of SDCC. Introduce pseudoinstructions. \texttt{Jump}: unconditional jump to labels. \item Other pseudoinstructions introduced: \texttt{Mov} moves (16 bit) data stored at a label (global vars). Conditional jumps to labels. \item Assembly language similar to that of SDCC. \end{itemize} \end{frame} \begin{frame}[fragile] \frametitle{Polymorphic variants and phantom types} The instruction set is highly non-orthogonal. We used polymorphic variants and phantom types to capture this non-orthogonality in the type system. Instruction set is highly non-orthogonal. Polymorphic variants and phantom types used to capture this non-orthogonality. For instance: \begin{frame}[fragile] \frametitle{Use of dependent types I} This approach worked well in O'Caml, but Matita does not have polymorphic variants, so we need a substitute. Worked well in O'Caml, Matita does not have polymorphic variants. We use dependent types. \end{lstlisting} \end{small} And another type \texttt{addressing\_mode\_tag} of tags' whose constructors are in correspondence with those of \texttt{addressing\_mode}. Another type \texttt{addressing\_mode\_tag} of tags'. Constructors are in correspondence with those of \texttt{addressing\_mode}. \end{frame} \begin{frame}[fragile] \frametitle{Use of dependent types II} We use vectors of \texttt{addressing\_mode\_tag}s in our type signatures for instructions. Use vectors of \texttt{addressing\_mode\_tag}s in type signatures for instructions. For instance: \begin{small} \end{small} We need: an \emph{ad hoc} $\Sigma$ type and two coercions. One coercion automatically opens up a proof obligation when it is used, which requires some lemmas. These lemmas and automation close all proof obligations generated (over 300 in typechecking the main interpreter function). One coercion opens up a proof obligation when it is used. Requires some lemmas. Lemmas and automation close proof obligations generated (300+ in typechecking interpreter function). \end{frame} \begin{frame} \frametitle{Overlapping memory spaces and addressing modes} MCS-51 memory spaces overlap, and can be addressed using different modes and sized pointers. The status' record models memory merely as disjoint spaces, using a tries with holes' datastructure. All complications to do with overlapping are handled by \texttt{set\_arg\_XX} and \texttt{get\_arg\_XX} for \texttt{XX} = 1, 8, 16. These functions make use of the aforementioned dependent type trick. \begin{itemize} \item Memory spaces overlap, can be addressed with different modes and pointers. \item Status' record models memory as disjoint spaces. \item Tries with holes' datastructure (dependent types). \item Complications with overlapping handled by \texttt{set\_arg\_XX} and \texttt{get\_arg\_XX} for \texttt{XX} = 1, 8, 16. \item Make use of dependent type trick. \end{itemize} \end{frame} Multiple data sheets from different manufacturers (errors found!) \item O'Caml output to Intel HEX for loading into third party tools, and input for use with SDCC. \item O'Caml produced trace files with processor status after every execution step, every opcode tested. \item Matita formalisation is also executable, and traces can be compared with O'Caml. Output to Intel HEX. Loading into third party tools. \item O'Caml trace files with processor status after every execution step. Every opcode tested. \item Matita formalisation is also executable. \item Traces can be compared with O'Caml. \end{itemize} \end{frame} \begin{frame} \frametitle{What is implemented} 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. In Matita, we have the emulator proper and associated assembler. We have yet to port the timers and I/O, preferring to focus on the core emulator. \begin{itemize} \item In O'Caml: emulator proper, associated assembler, supprting debugging code (Intel HEX), (untested) code for timers, interrupts and I/O. \item In Matita: emulator proper and associated assembler. \item Yet to port the timers and I/O, preferring to focus on the core emulator. \end{itemize} \end{frame}
Note: See TracChangeset for help on using the changeset viewer.