Changeset 960


Ignore:
Timestamp:
Jun 15, 2011, 3:39:44 PM (8 years ago)
Author:
mulligan
Message:

more work on paper

Location:
src/ASM/CPP2011
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.bib

    r953 r960  
    7272
    7373@inproceedings
     74{ mulligan:executable:2011,
     75  author = {Dominic P. Mulligan and Claudio Sacerdoti Coen},
     76  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
     77  booktitle = {Formal Methods in Computer Aided Design},
     78  year = {2011},
     79  note = {Submitted}
     80}
     81
     82@inproceedings
    7483{ yan:wcet:2008,
    7584  author = {Jun Yan and Wei Zhang},
     
    9099@misc
    91100{ cerco-report-code:2011,
    92   title = {{CerCo Deliverable D2.2}: prototype cost-preserving C compiler},
     101  title = {{CerCo Deliverable D2.2}: prototype cost-preserving {C} compiler},
    93102  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D2_2.pdf} and \url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D2_2_Code.tar.gz}},
    94103  year = {2011},
  • src/ASM/CPP2011/cpp-2011.tex

    r957 r960  
    11\documentclass{llncs}
    22
     3\usepackage{amsfonts}
    34\usepackage{amsmath}
     5\usepackage{amssymb}
    46\usepackage[english]{babel}
     7\usepackage{color}
     8\usepackage{fancybox}
     9\usepackage{graphicx}
    510\usepackage[colorlinks]{hyperref}
    611\usepackage[utf8x]{inputenc}
    712\usepackage{listings}
     13\usepackage{mdwlist}
     14\usepackage{microtype}
     15\usepackage{stmaryrd}
     16\usepackage{url}
     17
     18\renewcommand{\verb}{\lstinline}
     19\def\lstlanguagefiles{lst-grafite.tex}
     20\lstset{language=Grafite}
    821
    922\newlength{\mylength}
     
    2033                {\endminipage\endSbox
    2134                        \[\fbox{\TheSbox}\]}
    22 
    23 %\lstdefinelanguage{matita-ocaml}
    24 %  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
    25 %   morekeywords={[2]whd,normalize,elim,cases,destruct},
    26 %   morekeywords={[3]type,of,val,assert,let,function},
    27 %   mathescape=true,
    28 %  }
    29 %\lstset{language=matita-ocaml,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
    30 %        keywordstyle=\bfseries, %\color{red}\bfseries,
    31 %        keywordstyle=[2]\bfseries, %\color{blue},
    32 %        keywordstyle=[3]\bfseries, %\color{blue}\bfseries,
    33 %%        commentstyle=\color{green},
    34 %%        stringstyle=\color{blue},
    35 %        showspaces=false,showstringspaces=false}
    36 %\DeclareUnicodeCharacter{8797}{:=}
    37 %\DeclareUnicodeCharacter{8797}{:=}
    38 %\DeclareUnicodeCharacter{10746}{++}
    39 %\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
    40 %\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
    41 
    42 %\lstset{
    43 %  extendedchars=false,
    44 %  inputencoding=utf8x,
    45 %  tabsize=1
    46 %}
    47 
    48 \renewcommand{\verb}{\lstinline}
    49 \def\lstlanguagefiles{lst-grafite.tex}
    50 \lstset{language=Grafite}
    5135
    5236\title{On the correctness of an assembler for the Intel MCS-51 microprocessor}
     
    190174\label{sect.matita}
    191175
     176Matita is a proof assistant based on the (Co)inductive Calculus of Constructions~\cite{asperti:user:2007}.
     177For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar.
     178We take time here to explain one of Matita's syntactic idiosyncracies, however.
     179The use of `$\mathtt{\ldots}$' or `$\mathtt{?}$' in an argument position denotes a type to be inferred automatically by unification.
     180The 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.
    192181
    193182% ---------------------------------------------------------------------------- %
     
    197186\label{sect.the.proof}
    198187
    199   \begin{itemize}
    200    \item use of dependent types to throw away wrong programs that would made
    201     the statement for completeness complex. E.g. misuse of addressing modes,
    202     jumps to non existent labels, etc.
    203    \item try to go for small reflection; avoid inductive predicates that require
    204     tactics (inversion, etc.) that do not work well with dependent types; small
    205     reflection usually does
    206    \item use coercions to simulate Russell; mix together the proof styles
    207     a la Russell (for situations with heavy dependent types) and the standard
    208     one
    209   \end{itemize}
    210 
    211 \begin{lstlisting}
    212  definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus
    213 \end{lstlisting}
    214 
    215 \begin{lstlisting}
    216  definition execute: nat → Status → Status
    217 \end{lstlisting}
     188\subsection{The assembler and semantics of machine code}
     189\label{subsect.the.assembler.and.semantics.of.machine.code}
     190
     191The formalisation in Matita of the semantics of MCS-51 machine code is described in~\cite{mulligan:executable:2011}.
     192We merely describe enough here to understand the rest of the proof.
     193
     194At heart, the MCS-51 emulator centres around a \texttt{Status} record, describing the current state of the microprocessor.
     195This record contains fields corresponding to the microprocessor's program counter, special function registers, and so on.
     196At the machine code level, code memory is implemented as a trie of bytes, addressed by the program counter.
     197Machine code programs are loaded into \texttt{Status} using the \texttt{load\_code\_memory} function.
     198
     199We may execut a single step of a machine code program using the \texttt{execute\_1} function, which returns an updated \texttt{Status}:
     200\begin{lstlisting}
     201definition execute_1: Status $\rightarrow$ Status := $\ldots$
     202\end{lstlisting}
     203The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement!) number of steps of a program.
     204
     205Naturally, assembly programs have analogues.
     206The counterpart of the \texttt{Status} record is \texttt{PseudoStatus}.
     207Instead 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.
     208Our analogue of \texttt{execute\_1} is \texttt{execute\_1\_pseudo\_instruction}:
     209\begin{lstlisting}
     210definition execute_1_pseudo_instruction: (Word $\rightarrow$ nat $\times$ nat) $\rightarrow$
     211                                         PseudoStatus $\rightarrow$ PseudoStatus := $\ldots$
     212\end{lstlisting}
     213Notice, here, that the emulation function for pseudoprograms takes an additional argument.
     214This 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.
     215We 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.
     216This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
     217During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es.
     218
     219The assembler, mapping programs consisting of lists of pseudoinstructions to lists of bytes, operates in a mostly straightforward manner.
     220To 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:
     221\begin{displaymath}
     222[\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]}
     223\end{displaymath}
     224
     225Here $\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.
     226Each machine code instruction $\mathtt{I^i_j}$ is then assembled, using the \texttt{assembly1} function, into a list of bytes.
     227This process is iterated for each pseudoinstruction, before the lists are flattened into a single bit list representation of the original assembly program.
     228
     229% ---------------------------------------------------------------------------- %
     230% SECTION                                                                      %
     231% ---------------------------------------------------------------------------- %
     232\subsection{Policies}
     233\label{subsect.policies}
    218234
    219235\begin{lstlisting}
     
    222238  | medium_jump: jump_length
    223239  | long_jump: jump_length.
    224 
     240\end{lstlisting}
     241
     242\begin{lstlisting}
    225243definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
    226244\end{lstlisting}
     
    286304
    287305\begin{lstlisting}
    288 axiom assembly_ok_to_expand_pseudo_instruction_ok:
    289  ∀program,assembled,costs.
    290   Some ... LANGLEassembled,costsRANGLE = assembly program →
    291    ∀ppc.
    292     let code_memory ≝ load_code_memory assembled in
    293     let preamble ≝ \fst program in   
    294     let data_labels ≝ construct_datalabels preamble in
    295     let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
    296     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    297     let expansion ≝ jump_expansion ppc program in
    298     let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in
    299      ∃instructions.
    300       Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
    301 \end{lstlisting}
    302 
    303 \begin{lstlisting}
    304306axiom assembly_ok:
    305307 ∀program,assembled,costs,labels.
     
    347349\label{sect.conclusions}
    348350
     351  \begin{itemize}
     352   \item use of dependent types to throw away wrong programs that would made
     353    the statement for completeness complex. E.g. misuse of addressing modes,
     354    jumps to non existent labels, etc.
     355   \item try to go for small reflection; avoid inductive predicates that require
     356    tactics (inversion, etc.) that do not work well with dependent types; small
     357    reflection usually does
     358   \item use coercions to simulate Russell; mix together the proof styles
     359    a la Russell (for situations with heavy dependent types) and the standard
     360    one
     361  \end{itemize}
     362
    349363\subsection{Use of dependent types and Russell}
    350364\label{subsect.use.of.dependent.types.and.Russell}
     
    364378\bibliography{cpp-2011.bib}
    365379
    366 \end{document}
     380\end{document}\renewcommand{\verb}{\lstinline}
     381\def\lstlanguagefiles{lst-grafite.tex}
     382\lstset{language=Grafite}
  • src/ASM/CPP2011/lst-grafite.tex

    r958 r960  
    22mathescape=true,
    33texcl=false,
    4 keywords={include },
     4keywords={include},
    55morekeywords={record, with, match, let, rec, corec, inductive, definition, axiom,
    66        qed, intro, intros, symmetry, simplify, rewrite, apply, elim, assumption,
     
    151151%backgroundcolor=\color{gray},
    152152frame=tblr,
    153 frameround=tttt,
     153%frameround=tttt,
    154154columns=flexible,
    155 basicstyle=\small,
     155basicstyle=\footnotesize\tt,
    156156}
    157157
Note: See TracChangeset for help on using the changeset viewer.