Changeset 981 for src/ASM/CPP2011


Ignore:
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

Location:
src/ASM/CPP2011
Files:
2 edited

Legend:

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

    r970 r981  
    2222
    2323@article
     24{ klein:machine:2006,
     25  author = {Gerwin Klein and Tobias Nipkow},
     26  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
     27  journal = {Transactions on Programming Languages and Systems},
     28  volume = {28},
     29  number = {4},
     30  pages = {619--695},
     31  year = {2006}
     32}
     33
     34@article
    2435{ klein:sel4:2010,
    2536  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},
     
    5465}
    5566
     67@book
     68{ moore:piton:1996,
     69  author = {J Strother Moore},
     70  title = {Piton: A mechanically verified assembly language},
     71  series = {Automated Reasoning Series},
     72  volume = {3},
     73  isbn = {978-0-7923-3920-5},
     74  publisher = {Springer},
     75  year = {1996}
     76}
     77
     78@inproceedings
     79{ atkey:coqjvm:2007,
     80  author = {Robert Atkey},
     81  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
     82  booktitle = {Conference of the {TYPES} Project},
     83  pages = {18--32},
     84  year = {2007}
     85}
     86
    5687@inproceedings
    5788{ blazy:formal:2006,
     
    6495
    6596@inproceedings
     97{ fox:trustworthy:2010,
     98  author = {Anthony Fox and Magnus O. Myreen},
     99  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
     100  booktitle = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
     101  pages = {243--258},
     102  year = {2010}
     103}
     104
     105@inproceedings
    66106{ klein:sel4:2009,
    67107  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},
     
    78118  year = {2011},
    79119  note = {Submitted}
     120}
     121
     122@inproceedings
     123{ sarkar:semantics:2009,
     124  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},
     125  title = {The semantics of {x86-CC} multiprocessor machine code},
     126  booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
     127  pages = {379--391},
     128  year = {2009}
     129}
     130
     131@inproceedings
     132{ sozeau:subset:2006,
     133  author = {Matthieu Sozeau},
     134  title = {Subset Coercions in {Coq}},
     135  booktitle = {Types for Proofs and Programs},
     136  pages = {237--252},
     137  year = {2006}
    80138}
    81139
     
    114172
    115173@misc
     174{ moore:grand:2005,
     175  author = {J Strother Moore},
     176  title = {A Grand Challenge Proposal for Formal Methods},
     177  year = {2005}
     178}
     179
     180@misc
    116181{ sdcc:2011,
    117182  title = {Small Device {C} Compiler 3.0.0},
     
    143208  year = {2010}
    144209}
     210
     211@techreport
     212{ klein:machine:2010,
     213  author = {Gerwin Klein and Tobias Nipkow},
     214  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
     215  institution = {National {ICT} Australia},
     216  number = {0400001T.1},
     217  year = {2010}
     218
     219}
  • src/ASM/CPP2011/cpp-2011.tex

    r976 r981  
    363363\end{lstlisting}
    364364Here, \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.
     365We assemble a single pseudoinstruction with \texttt{assembly\_1\_pseudoinstruction}, which internally calls \texttt{jump\_expansion} and \texttt{expand\_pseudo\_instruction}.
    365366The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks.
    366367
     
    438439We have proved the total correctness of an assembler for MCS-51 assembly language.
    439440In 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.
    440 
    441 \subsection{Use of dependent types and Russell}
    442 \label{subsect.use.of.dependent.types.and.Russell}
    443 
     441Expanding 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.
     442
     443Aside from their application in verified compiler projects such as CerCo, verified assemblers could also be applied to the verification of operating system kernels.
     444Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}.
     445This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler.
     446
     447\paragraph{Use of dependent types and Russell}
    444448Our formalisation makes sparing use of dependent types.
    445449In certain datastructures, such as tries and vectors, they are used to guarantee invariants.
     
    449453However, there are certain cases where the use of dependent types is unavoidable.
    450454For 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.
    451 In cases such as these we make use of Matita's implementation of Russell~\cite{}.
     455In cases such as these we make use of Matita's implementation of Russell~\cite{sozeau:subset:2006}.
     456In Matita, Russell may be implemented with two coercions and some notational sugaring.
    452457
    453458\subsection{Related work}
    454459\label{subsect.related.work}
     460
     461% piton
     462We are not the first to consider the total correctness of an assembler for a non-trivial assembly language.
     463Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996,moore:grand:2005}.
     464This 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}.
     465%dpm more: weirich paper?
     466
     467% jinja
     468Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006,klein:machine:2010}.
     469They 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.
     470
     471Finally, 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.
     472As previously mentioned, CompCert considers only extensional correctness of the compiler, and not intensional correctness, which CerCo focusses on.
     473However, CerCo also extends CompCert in other ways.
     474Namely, the CompCert verified compilation chain terminates at the PowerPC or ARM assembly level, and takes for granted the existence of a trustworthy assembler.
     475CerCo chooses to go further, by considering a verified compilation chain all the way down to the machine code level.
     476In essence, the work presented in this publication is one part of CerCo's extension over CompCert.
    455477
    456478\bibliography{cpp-2011.bib}
Note: See TracChangeset for help on using the changeset viewer.