Changeset 549 for Deliverables
- Timestamp:
- Feb 17, 2011, 11:46:40 AM (10 years ago)
- 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 58 58 \institute{Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna} 59 59 60 \bibliographystyle{alpha} 61 60 62 \begin{document} 61 63 … … 651 653 These traces were useful in spotting anything that was `obviously' wrong with the execution of the program. 652 654 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.655 Further, we used MCU 8051 IDE as a reference. 656 Using 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. 655 657 656 658 Our Matita formalisation was largely copied from the O'Caml source code, apart from changes related to addressing modes already mentioned. … … 668 670 Moreover, 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. 669 671 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}.672 Similar work to ours can be found in~\cite{fox:trustworthy:2010}. 671 673 Here, 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. 672 674 This formalisation also considers the machine code level, as opposed to only considering an abstract assembly language. … … 674 676 However, we go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction to machine code. 675 677 676 Further, in~\cite{ again} the authors validated their formalisation by using development boards and random testing.678 Further, in~\cite{fox:trustworthy:2010} the authors validated their formalisation by using development boards and random testing. 677 679 However, we currently rely on non-exhaustive testing against a third party emulator. 678 680 We leave similar exhaustive testing for future work. 679 681 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.682 Executability is another key difference between our work and~\cite{fox:trustworthy:2010}. 683 In~\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. 682 684 We do not need single step theorems of this form. 683 685 This is because Matita is based on a logic that internalizes conversion. … … 687 689 In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably. 688 690 689 Perhaps the closest project to CerCo is CompCert~\cite{ compcert}.691 Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009,blazy:formal:2006}. 690 692 CompCert concerns the certification of an ARM compiler and includes a formalisation in Coq of a subset of ARM. 691 693 Coq and Matita essentially share the same logic. … … 698 700 Even 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. 699 701 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.702 In~\cite{atkey:coqjvm:2007} Atkey presents an executable specification of the Java virtual machine which uses dependent types. 701 703 As 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. 702 704 Our use of dependent types will also help to maintain invariants when we prove the correctness of the CerCo prototype compiler. 703 705 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.706 Finally, in~\cite{sarkar:semantics:2009} Sarkar et al provide an executable semantics for x86-CC multiprocessor machine code. 705 707 This machine code exhibits a high degree of non-uniformity similar to the MCS-51. 706 708 However, 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. … … 728 730 - WE FORMALIZE ALSO I/O ETC. NOT ONLY THE INSTRUCTION SELECTION (??) 729 731 How to test it? Specify it? 732 733 \bibliography{itp-2011.bib} 730 734 731 735 \newpage
Note: See TracChangeset
for help on using the changeset viewer.