Changeset 549


Ignore:
Timestamp:
Feb 17, 2011, 11:46:40 AM (6 years ago)
Author:
mulligan
Message:

Half of bibliography added.

Location:
Deliverables/D4.1/ITP-Paper
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r548 r549  
    5858\institute{Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna}
    5959
     60\bibliographystyle{alpha}
     61
    6062\begin{document}
    6163
     
    651653These traces were useful in spotting anything that was `obviously' wrong with the execution of the program.
    652654
    653 Further, we made use of an open source emulator for the MCS-51, \texttt{mcu8051ide}.
    654 Using our execution traces, we were able to step through a compiled program, one instruction at a time, in \texttt{mcu8051ide}, and compare the resulting execution trace with the trace produced by our emulator.
     655Further, we used MCU 8051 IDE as a reference.
     656Using our execution traces, we were able to step through a compiled program, one instruction at a time, in MCU 8051 IDE, and compare the resulting execution trace with the trace produced by our emulator.
    655657
    656658Our Matita formalisation was largely copied from the O'Caml source code, apart from changes related to addressing modes already mentioned.
     
    668670Moreover, in addition to formalising the interface of an MCS-51 processor, we have also built a complete MCS-51 ecosystem: the UART, the I/O lines, and hardware timers, along with an assembler.
    669671
    670 Similar work to ours can be found in~\cite{A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture Anthony Fox and Magnus O. Myreen}.
     672Similar work to ours can be found in~\cite{fox:trustworthy:2010}.
    671673Here, the authors describe the formalisation, in HOL4, of the ARMv7 instruction set architecture, and point to a good list of references to related work in the literature.
    672674This formalisation also considers the machine code level, as opposed to only considering an abstract assembly language.
     
    674676However, we go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction to machine code.
    675677
    676 Further, in~\cite{again} the authors validated their formalisation by using development boards and random testing.
     678Further, in~\cite{fox:trustworthy:2010} the authors validated their formalisation by using development boards and random testing.
    677679However, we currently rely on non-exhaustive testing against a third party emulator.
    678680We leave similar exhaustive testing for future work.
    679681
    680 Executability is another key difference between our work and~\cite{again}.
    681 In~\cite{again} the authors provide an automation layer to derive single step theorems: if the processor is in a particular state that satisfies some preconditions, then after execution of an instruction it will reside in another state satisfying some postconditions.
     682Executability is another key difference between our work and~\cite{fox:trustworthy:2010}.
     683In~\cite{fox:trustworthy:2010} the authors provide an automation layer to derive single step theorems: if the processor is in a particular state that satisfies some preconditions, then after execution of an instruction it will reside in another state satisfying some postconditions.
    682684We do not need single step theorems of this form.
    683685This is because Matita is based on a logic that internalizes conversion.
     
    687689In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably.
    688690
    689 Perhaps the closest project to CerCo is CompCert~\cite{compcert}.
     691Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009,blazy:formal:2006}.
    690692CompCert concerns the certification of an ARM compiler and includes a formalisation in Coq of a subset of ARM.
    691693Coq and Matita essentially share the same logic.
     
    698700Even from a technical level the two formalisations differ: while we tried to exploit dependent types as often as possible, CompCert largely sticks to the non-dependent fragment of Coq.
    699701
    700 In~\cite{Robert Atkey. CoqJVM: An executable specification of the Java virtual machine using dependent types. In Marino Miculan, Ivan Scagnetto, and Furio Honsell, editors, TYPES, volume 4941 of Lecture Notes in Computer Science, pages 18-32.  Springer, 2007.} Atkey presents an executable specification of the Java virtual machine which uses dependent types.
     702In~\cite{atkey:coqjvm:2007} Atkey presents an executable specification of the Java virtual machine which uses dependent types.
    701703As we do, dependent types are used to remove spurious partiality from the model, and to lower the need for over-specifying the behaviour of the processor in impossible cases.
    702704Our use of dependent types will also help to maintain invariants when we prove the correctness of the CerCo prototype compiler.
    703705
    704 Finally, in~\cite{Susmit Sarkar, Pater Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant Magnus O. Myreen, and Jade Alglave. The semantics of x86-CC multiprocessor machine code. In Principles of Programming Languages (POPL). ACM, 2009.} Sarkar et al provide an executable semantics for x86-CC multiprocessor machine code.
     706Finally, in~\cite{sarkar:semantics:2009} Sarkar et al provide an executable semantics for x86-CC multiprocessor machine code.
    705707This machine code exhibits a high degree of non-uniformity similar to the MCS-51.
    706708However, only a very small subset of the instruction set is considered, and they over-approximate the possibilities of unorthogonality of the instruction set, largely dodging the problems we had to face.
     
    728730- WE FORMALIZE ALSO I/O ETC. NOT ONLY THE INSTRUCTION SELECTION (??)
    729731  How to test it? Specify it?
     732
     733\bibliography{itp-2011.bib}
    730734
    731735\newpage
Note: See TracChangeset for help on using the changeset viewer.