Changeset 960 for src/ASM/CPP2011/cpp2011.tex
 Timestamp:
 Jun 15, 2011, 3:39:44 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r957 r960 1 1 \documentclass{llncs} 2 2 3 \usepackage{amsfonts} 3 4 \usepackage{amsmath} 5 \usepackage{amssymb} 4 6 \usepackage[english]{babel} 7 \usepackage{color} 8 \usepackage{fancybox} 9 \usepackage{graphicx} 5 10 \usepackage[colorlinks]{hyperref} 6 11 \usepackage[utf8x]{inputenc} 7 12 \usepackage{listings} 13 \usepackage{mdwlist} 14 \usepackage{microtype} 15 \usepackage{stmaryrd} 16 \usepackage{url} 17 18 \renewcommand{\verb}{\lstinline} 19 \def\lstlanguagefiles{lstgrafite.tex} 20 \lstset{language=Grafite} 8 21 9 22 \newlength{\mylength} … … 20 33 {\endminipage\endSbox 21 34 \[\fbox{\TheSbox}\]} 22 23 %\lstdefinelanguage{matitaocaml}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=matitaocaml,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=146 %}47 48 \renewcommand{\verb}{\lstinline}49 \def\lstlanguagefiles{lstgrafite.tex}50 \lstset{language=Grafite}51 35 52 36 \title{On the correctness of an assembler for the Intel MCS51 microprocessor} … … 190 174 \label{sect.matita} 191 175 176 Matita is a proof assistant based on the (Co)inductive Calculus of Constructions~\cite{asperti:user:2007}. 177 For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar. 178 We take time here to explain one of Matita's syntactic idiosyncracies, however. 179 The use of `$\mathtt{\ldots}$' or `$\mathtt{?}$' in an argument position denotes a type to be inferred automatically by unification. 180 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. 192 181 193 182 %  % … … 197 186 \label{sect.the.proof} 198 187 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 191 The formalisation in Matita of the semantics of MCS51 machine code is described in~\cite{mulligan:executable:2011}. 192 We merely describe enough here to understand the rest of the proof. 193 194 At heart, the MCS51 emulator centres around a \texttt{Status} record, describing the current state of the microprocessor. 195 This record contains fields corresponding to the microprocessor's program counter, special function registers, and so on. 196 At the machine code level, code memory is implemented as a trie of bytes, addressed by the program counter. 197 Machine code programs are loaded into \texttt{Status} using the \texttt{load\_code\_memory} function. 198 199 We 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} 201 definition execute_1: Status $\rightarrow$ Status := $\ldots$ 202 \end{lstlisting} 203 The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement!) number of steps of a program. 204 205 Naturally, assembly programs have analogues. 206 The counterpart of the \texttt{Status} record is \texttt{PseudoStatus}. 207 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. 208 Our analogue of \texttt{execute\_1} is \texttt{execute\_1\_pseudo\_instruction}: 209 \begin{lstlisting} 210 definition execute_1_pseudo_instruction: (Word $\rightarrow$ nat $\times$ nat) $\rightarrow$ 211 PseudoStatus $\rightarrow$ PseudoStatus := $\ldots$ 212 \end{lstlisting} 213 Notice, here, that the emulation function for pseudoprograms takes an additional argument. 214 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. 215 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. 216 This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}. 217 During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es. 218 219 The assembler, mapping programs consisting of lists of pseudoinstructions to lists of bytes, operates in a mostly straightforward manner. 220 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: 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 225 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. 226 Each machine code instruction $\mathtt{I^i_j}$ is then assembled, using the \texttt{assembly1} function, into a list of bytes. 227 This 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} 218 234 219 235 \begin{lstlisting} … … 222 238  medium_jump: jump_length 223 239  long_jump: jump_length. 224 240 \end{lstlisting} 241 242 \begin{lstlisting} 225 243 definition jump_expansion_policy ≝ BitVectorTrie jump_length 16. 226 244 \end{lstlisting} … … 286 304 287 305 \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 in293 let preamble ≝ \fst program in294 let data_labels ≝ construct_datalabels preamble in295 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in296 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in297 let expansion ≝ jump_expansion ppc program in298 let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in299 ∃instructions.300 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.301 \end{lstlisting}302 303 \begin{lstlisting}304 306 axiom assembly_ok: 305 307 ∀program,assembled,costs,labels. … … 347 349 \label{sect.conclusions} 348 350 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 349 363 \subsection{Use of dependent types and Russell} 350 364 \label{subsect.use.of.dependent.types.and.Russell} … … 364 378 \bibliography{cpp2011.bib} 365 379 366 \end{document} 380 \end{document}\renewcommand{\verb}{\lstinline} 381 \def\lstlanguagefiles{lstgrafite.tex} 382 \lstset{language=Grafite}
Note: See TracChangeset
for help on using the changeset viewer.