Changeset 526


Ignore:
Timestamp:
Feb 15, 2011, 6:11:40 PM (6 years ago)
Author:
sacerdot
Message:

Something to say in the comparison.

File:
1 edited

Legend:

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

    r525 r526  
    615615\label{sect.related.work}
    616616
     617\CSC{Tell what is NOT formalized/formalizable: the HEX parser/pretty printer
     618 and/or the I/O procedure}
     619\CSC{Appendix with main functions interfaces?}
     620\CSC{Decode: two implementations}
     621\CSC{Discuss over-specification}
     622
     623- WE FORMALIZE ALSO I/O ETC. NOT ONLY THE INSTRUCTION SELECTION (??)
     624  How to test it? Specify it?
     625
     626------------------------------------------
     627
     628Hardware verification?
     629
     630------------------------------------------------------------
     631
     632A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture Anthony Fox and Magnus O. Myreen:
     633
     634- The model operates at the machine code level, as opposed to a more abstract
     635assembly code level. In particular, the model does not provide assembly
     636level “pseudo instructions” and instruction decoding is explicitly modelled
     637inside the logic. This means that the the model can be directly validated
     638by comparing results against the behaviour of hardware employing ARM
     639processors – this is discussed in Section 5.
     640
     641- Monadic style: what do we do in OCaml/Matita?
     642- Single Step Theorems
     643- validation against developments boards and random testing
     644
     645This section discusses related work in formalizing various commercial instruction
     646set architectures using interactive theorem provers, i.e. in ACL2, Coq, Isabelle
     647and HOL4. There is much work that is indirectly related, but here we exclude
     648non-commercial architectures (e.g. DLX) and informal or semi-formal ISA mod-
     649els (e.g. in C, System Verilog, Haskell and so forth).
     650
     651ARM (this paper)
     652x86 (15/7)
     653JVM (many)
     654
     655WE ALSO HAVE AN ASSEMBLER (THEY DON'T)
     656
     657-----------------
     658
     659CompCert:
     660 - assembly level model (no instruction decoding, etc.)
     661 - abstract memory model
     662 They also have a more abstract view of memory which is expressed in terms of memory blocks, in contrast to our very concrete mapping from 32-bit addresses to 8-bit data.
     663 - 90 instructions of the 200+ offered by the processor; not all registers too
     664 - macro instructions that are turned into real instructions only during
     665   pretty-printing!
     666 - no proof of correctness of assembly and linking
     667
     668
     669-----------------
     670
     671Robert Atkey. CoqJVM: An executable specification of the Java virtual machine
     672using dependent types. In Marino Miculan, Ivan Scagnetto, and Furio Honsell,
     673editors, TYPES, volume 4941 of Lecture Notes in Computer Science, pages 18–32.
     674Springer, 2007.
     675
     676CoqJVM dependent types:
     677
     678                                       We remove this spurious partiality from
     679the model by making use of dependent types to maintain invariants about the
     680state of the JVM. These invariants are then available to all proofs concerning
     681the model.
     682
     683            Our belief is that this will make large-scale proofs using the model
     684easier to perform, and we have some initial evidence that this is the case, but
     685detailed research of this claim is still required.
     686
     687------------------------------------
     688
     689Susmit Sarkar, Pater Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge,
     690Thomas Braibant Magnus O. Myreen, and Jade Alglave. The semantics of x86-CC
     691multiprocessor machine code. In Principles of Programming Languages (POPL).
     692ACM, 2009.
     693
     694(What Yann complained on was done in this paper:)
     695                                    To make the semantics
     696scalable, without introducing many errors, we formalised
     697the interpretation of these encodings inside the HOL logic,
     698and built a HOL decoding function by directly copying the
     699relevant lines from the manual into the HOL script.
     700
     701However, they only consider a very small subset of the instructions and they
     702over-approximate the possibilities of unorthogonality of the instruction set.
     703
     704
    617705%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    618706% SECTION                                                                      %
Note: See TracChangeset for help on using the changeset viewer.