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

Timestamp:

Jun 16, 2011, 2:39:23 PM (9 years ago)

Author:

mulligan

Message:

added more, worked on conclusions and related work. need just to finish explanation of large lemmas

File:

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

src/ASM/CPP2011/cpp-2011.tex

@@ -363 +363 @@
 \end{lstlisting}
 Here, \texttt{len} is the number of machine code instructions the pseudoinstruction at hand has been expanded into, \texttt{encoding\_check} is a recursive function that checks for any possible corruption of the code memory, resulting from expanding the pseudoinstruction.
+We assemble a single pseudoinstruction with \texttt{assembly\_1\_pseudoinstruction}, which internally calls \texttt{jump\_expansion} and \texttt{expand\_pseudo\_instruction}.
 The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks.
 
@@ -438 +439 @@
 We have proved the total correctness of an assembler for MCS-51 assembly language.
 In particular, our assembly language featured labels, arbitrary conditional and unconditional jumps to labels, global data and instructions for moving this data into the MCS-51's single 16-bit register.
-
-\subsection{Use of dependent types and Russell}
-\label{subsect.use.of.dependent.types.and.Russell}
-
+Expanding these pseudoinstructions into machine code instructions is not trivial, and the proof that the assembly process is `correct', in that the semantics of an assembly program are not changed is complex.
+
+Aside from their application in verified compiler projects such as CerCo, verified assemblers could also be applied to the verification of operating system kernels.
+Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}.
+This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler.
+
+\paragraph{Use of dependent types and Russell}
 Our formalisation makes sparing use of dependent types.
 In certain datastructures, such as tries and vectors, they are used to guarantee invariants.
@@ -449 +453 @@
 However, there are certain cases where the use of dependent types is unavoidable.
 For instance, when proving that the \texttt{build\_maps} function is correct, a function that collates the cost and data labels of an assembly program into map datastructures.
-In cases such as these we make use of Matita's implementation of Russell~\cite{}.
+In cases such as these we make use of Matita's implementation of Russell~\cite{sozeau:subset:2006}.
+In Matita, Russell may be implemented with two coercions and some notational sugaring.
 
 \subsection{Related work}
 \label{subsect.related.work}
+
+% piton
+We are not the first to consider the total correctness of an assembler for a non-trivial assembly language.
+Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996,moore:grand:2005}.
+This was a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two high-level languages---a dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}.
+%dpm more: weirich paper?
+
+% jinja
+Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006,klein:machine:2010}.
+They provide a compiler, virtual machine and operational semantics for the programming language and virtual machine, and prove that their compiler is semantics and type preserving.
+
+Finally, mention should be made of CompCert~\cite{compcert:2011,blazy:formal:2006,leroy:formal:2009,leroy:formally:2009}, another verified compiler project related to CerCo.
+As previously mentioned, CompCert considers only extensional correctness of the compiler, and not intensional correctness, which CerCo focusses on.
+However, CerCo also extends CompCert in other ways.
+Namely, the CompCert verified compilation chain terminates at the PowerPC or ARM assembly level, and takes for granted the existence of a trustworthy assembler.
+CerCo chooses to go further, by considering a verified compilation chain all the way down to the machine code level.
+In essence, the work presented in this publication is one part of CerCo's extension over CompCert.
 
 \bibliography{cpp-2011.bib}