Changeset 960 for src/ASM/CPP2011/cpp-2011.tex

Timestamp:

Jun 15, 2011, 3:39:44 PM (9 years ago)

Author:

mulligan

Message:

more work on paper

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (8 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -1 +1 @@
 \documentclass{llncs}
 
+\usepackage{amsfonts}
 \usepackage{amsmath}
+\usepackage{amssymb} 
 \usepackage[english]{babel}
+\usepackage{color}
+\usepackage{fancybox}
+\usepackage{graphicx}
 \usepackage[colorlinks]{hyperref}
 \usepackage[utf8x]{inputenc}
 \usepackage{listings}
+\usepackage{mdwlist}
+\usepackage{microtype}
+\usepackage{stmaryrd}
+\usepackage{url}
+
+\renewcommand{\verb}{\lstinline}
+\def\lstlanguagefiles{lst-grafite.tex}
+\lstset{language=Grafite}
 
 \newlength{\mylength}
@@ -20 +33 @@
                 {\endminipage\endSbox
                         \[\fbox{\TheSbox}\]}
-
-%\lstdefinelanguage{matita-ocaml}
-%  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
-%   morekeywords={[2]whd,normalize,elim,cases,destruct},
-%   morekeywords={[3]type,of,val,assert,let,function},
-%   mathescape=true,
-%  }
-%\lstset{language=matita-ocaml,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
-%        keywordstyle=\bfseries, %\color{red}\bfseries,
-%        keywordstyle=[2]\bfseries, %\color{blue},
-%        keywordstyle=[3]\bfseries, %\color{blue}\bfseries,
-%%        commentstyle=\color{green},
-%%        stringstyle=\color{blue},
-%        showspaces=false,showstringspaces=false}
-%\DeclareUnicodeCharacter{8797}{:=}
-%\DeclareUnicodeCharacter{8797}{:=}
-%\DeclareUnicodeCharacter{10746}{++}
-%\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
-%\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
-
-%\lstset{
-%  extendedchars=false,
-%  inputencoding=utf8x,
-%  tabsize=1
-%}
-
-\renewcommand{\verb}{\lstinline}
-\def\lstlanguagefiles{lst-grafite.tex}
-\lstset{language=Grafite}
 
 \title{On the correctness of an assembler for the Intel MCS-51 microprocessor}
@@ -190 +174 @@
 \label{sect.matita}
 
+Matita is a proof assistant based on the (Co)inductive Calculus of Constructions~\cite{asperti:user:2007}.
+For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar.
+We take time here to explain one of Matita's syntactic idiosyncracies, however.
+The use of `$\mathtt{\ldots}$' or `$\mathtt{?}$' in an argument position denotes a type to be inferred automatically by unification.
+The use of `$\mathtt{?}$' in the body of a definition, lemma or axiom denotes an incomplete term that is to be closed, by hand, using tactics.
 
 % ---------------------------------------------------------------------------- %
@@ -197 +186 @@
 \label{sect.the.proof}
 
-  \begin{itemize}
-   \item use of dependent types to throw away wrong programs that would made
-    the statement for completeness complex. E.g. misuse of addressing modes,
-    jumps to non existent labels, etc.
-   \item try to go for small reflection; avoid inductive predicates that require
-    tactics (inversion, etc.) that do not work well with dependent types; small
-    reflection usually does
-   \item use coercions to simulate Russell; mix together the proof styles
-    a la Russell (for situations with heavy dependent types) and the standard
-    one
-  \end{itemize}
-
-\begin{lstlisting}
- definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus
-\end{lstlisting}
-
-\begin{lstlisting}
- definition execute: nat → Status → Status
-\end{lstlisting}
+\subsection{The assembler and semantics of machine code}
+\label{subsect.the.assembler.and.semantics.of.machine.code}
+
+The formalisation in Matita of the semantics of MCS-51 machine code is described in~\cite{mulligan:executable:2011}.
+We merely describe enough here to understand the rest of the proof.
+
+At heart, the MCS-51 emulator centres around a \texttt{Status} record, describing the current state of the microprocessor.
+This record contains fields corresponding to the microprocessor's program counter, special function registers, and so on.
+At the machine code level, code memory is implemented as a trie of bytes, addressed by the program counter.
+Machine code programs are loaded into \texttt{Status} using the \texttt{load\_code\_memory} function.
+
+We may execut a single step of a machine code program using the \texttt{execute\_1} function, which returns an updated \texttt{Status}:
+\begin{lstlisting}
+definition execute_1: Status $\rightarrow$ Status := $\ldots$
+\end{lstlisting}
+The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement!) number of steps of a program.
+
+Naturally, assembly programs have analogues.
+The counterpart of the \texttt{Status} record is \texttt{PseudoStatus}.
+Instead of code memory being implemented as tries of bytes, code memory is here implemented as lists of pseudoinstructions, and program counters are merely indices into this list.
+Our analogue of \texttt{execute\_1} is \texttt{execute\_1\_pseudo\_instruction}:
+\begin{lstlisting}
+definition execute_1_pseudo_instruction: (Word $\rightarrow$ nat $\times$ nat) $\rightarrow$
+                                         PseudoStatus $\rightarrow$ PseudoStatus := $\ldots$
+\end{lstlisting}
+Notice, here, that the emulation function for pseudoprograms takes an additional argument.
+This is a function that maps program counters (for the pseudoprogram) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion.
+We require \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in the number of clock ticks needed for execution.
+This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
+During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es.
+
+The assembler, mapping programs consisting of lists of pseudoinstructions to lists of bytes, operates in a mostly straightforward manner.
+To a degree of approximation, the assembler on an assembly program, consisting of $n$ pseudoinstructions $\mathtt{P_i}$ for $1 \leq i \leq n$, works as in the following diagram:
+\begin{displaymath}
+[\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly1}^*$}} \mathtt{[0110]}\right)^{*}} \mathtt{[010101]}
+\end{displaymath}
+
+Here $\mathtt{I^i_j}$ for $1 \leq j \leq q$ are the $q$ machine code instructions obtained by expanding, with \texttt{expand\_pseudo\_instruction}, a single pseudoinstruction.
+Each machine code instruction $\mathtt{I^i_j}$ is then assembled, using the \texttt{assembly1} function, into a list of bytes.
+This process is iterated for each pseudoinstruction, before the lists are flattened into a single bit list representation of the original assembly program.
+
+% ---------------------------------------------------------------------------- %
+% SECTION                                                                      %
+% ---------------------------------------------------------------------------- %
+\subsection{Policies}
+\label{subsect.policies}
 
 \begin{lstlisting}
@@ -222 +238 @@
   | medium_jump: jump_length
   | long_jump: jump_length.
-
+\end{lstlisting}
+
+\begin{lstlisting}
 definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
 \end{lstlisting}
@@ -286 +304 @@
 
 \begin{lstlisting}
-axiom assembly_ok_to_expand_pseudo_instruction_ok:
- ∀program,assembled,costs.
-  Some ... LANGLEassembled,costsRANGLE = assembly program →
-   ∀ppc.
-    let code_memory ≝ load_code_memory assembled in
-    let preamble ≝ \fst program in   
-    let data_labels ≝ construct_datalabels preamble in
-    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
-    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
-    let expansion ≝ jump_expansion ppc program in
-    let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in
-     ∃instructions.
-      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
-\end{lstlisting}
-
-\begin{lstlisting}
 axiom assembly_ok:
  ∀program,assembled,costs,labels.
@@ -347 +349 @@
 \label{sect.conclusions}
 
+  \begin{itemize}
+   \item use of dependent types to throw away wrong programs that would made
+    the statement for completeness complex. E.g. misuse of addressing modes,
+    jumps to non existent labels, etc.
+   \item try to go for small reflection; avoid inductive predicates that require
+    tactics (inversion, etc.) that do not work well with dependent types; small
+    reflection usually does
+   \item use coercions to simulate Russell; mix together the proof styles
+    a la Russell (for situations with heavy dependent types) and the standard
+    one
+  \end{itemize}
+
 \subsection{Use of dependent types and Russell}
 \label{subsect.use.of.dependent.types.and.Russell}
@@ -364 +378 @@
 \bibliography{cpp-2011.bib}
 
-\end{document}
+\end{document}\renewcommand{\verb}{\lstinline}
+\def\lstlanguagefiles{lst-grafite.tex}
+\lstset{language=Grafite}