Changeset 981

Timestamp:

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

Author:

mulligan

Message:

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

Location:

src/ASM/CPP2011

Files:

• cpp-2011.bib (modified) (6 diffs)
• cpp-2011.tex (modified) (3 diffs)

src/ASM/CPP2011/cpp-2011.bib

@@ -22 +22 @@
 
 @article
+{ klein:machine:2006,
+  author = {Gerwin Klein and Tobias Nipkow},
+  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
+  journal = {Transactions on Programming Languages and Systems},
+  volume = {28}, 
+  number = {4}, 
+  pages = {619--695},
+  year = {2006}
+}
+
+@article
 { klein:sel4:2010,
   author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
@@ -54 +65 @@
 }
 
+@book
+{ moore:piton:1996,
+  author = {J Strother Moore},
+  title = {Piton: A mechanically verified assembly language},
+  series = {Automated Reasoning Series},
+  volume = {3},
+  isbn = {978-0-7923-3920-5},
+  publisher = {Springer},
+  year = {1996}
+}
+
+@inproceedings
+{ atkey:coqjvm:2007,
+  author = {Robert Atkey},
+  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
+  booktitle = {Conference of the {TYPES} Project},
+  pages = {18--32},
+  year = {2007}
+}
+
 @inproceedings
 { blazy:formal:2006,
@@ -64 +95 @@
 
 @inproceedings
+{ fox:trustworthy:2010,
+  author = {Anthony Fox and Magnus O. Myreen},
+  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
+  booktitle = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
+  pages = {243--258},
+  year = {2010}
+}
+
+@inproceedings
 { klein:sel4:2009,
   author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
@@ -78 +118 @@
   year = {2011},
   note = {Submitted}
+}
+
+@inproceedings
+{ sarkar:semantics:2009,
+  author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave},
+  title = {The semantics of {x86-CC} multiprocessor machine code},
+  booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
+  pages = {379--391},
+  year = {2009}
+}
+
+@inproceedings
+{ sozeau:subset:2006,
+  author = {Matthieu Sozeau},
+  title = {Subset Coercions in {Coq}},
+  booktitle = {Types for Proofs and Programs},
+  pages = {237--252},
+  year = {2006}
 }
 
@@ -114 +172 @@
 
 @misc
+{ moore:grand:2005,
+  author = {J Strother Moore},
+  title = {A Grand Challenge Proposal for Formal Methods},
+  year = {2005}
+}
+
+@misc
 { sdcc:2011,
   title = {Small Device {C} Compiler 3.0.0},
@@ -143 +208 @@
   year = {2010}
 }
+
+@techreport
+{ klein:machine:2010,
+  author = {Gerwin Klein and Tobias Nipkow},
+  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
+  institution = {National {ICT} Australia},
+  number = {0400001T.1},
+  year = {2010}
+
+}

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}