Changeset 2095


Ignore:
Timestamp:
Jun 15, 2012, 1:58:32 PM (5 years ago)
Author:
mulligan
Message:

Added reference to CompCert? and CompCertTSO.

Location:
src/ASM/CPP2012-asm
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-asm/cpp-2012-asm.bib

    r2092 r2095  
    113113
    114114@inproceedings
     115{ sevcik:relaxed-memory:2011,
     116  author = {Jaroslav \v{S}ev\v{c}\'ik and Viktor Vafeiadis and  Francesco {Zappa Nardelli} and Suresh Jagannathan and Peter Sewell},
     117  title = {Relaxed-Memory Concurrency and Verified Compilation},
     118  booktitle = {Principles of Programming Languages {(POPL)}},
     119  year = {2011}
     120}
     121
     122@inproceedings
    115123{ tuch:types:2007,
    116124  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
  • src/ASM/CPP2012-asm/cpp-2012-asm.tex

    r2092 r2095  
    554554The definition and proof of a terminating, correct jump expansion policy is described in a companion publication to this one~\cite{boender:correctness:2012}.
    555555
    556 Aside from their application in verified compiler projects such as CerCo and CompCert, verified assemblers such as ours could also be applied to the verification of operating system kernels.
     556Aside from their application in verified compiler projects such as CerCo, CompCert~\cite{leroy:formally:2009} and CompCertTSO~\cite{sevcik:relaxed-memory:2011}, verified assemblers such as ours could also be applied to the verification of operating system kernels.
    557557Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}.
    558558This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler and compiler.
    559559
    560 Note that both CompCert and the seL4 formalisation assume the existence of `trustworthy' assemblers.
    561 The observation that an optimising assembler cannot preserve the semantics of every assembly program may have important consequences for these projects.
     560Note that both CompCert, CompCertTSO and the seL4 formalisation assume the existence of `trustworthy' assemblers.
     561For instance, the CompCert C compiler's backend stops at the PowerPC assembly language, in the default backend.
     562The observation that an optimising assembler cannot preserve the semantics of every assembly program may have important consequences for these projects (though in the case of CompCertTSO, targetting a multiprocessor, what exactly constitutes the subset of `good programs' may not be entirely clear).
    562563If CompCert chooses to assume the existence of an optimising assembler, then care should be made to ensure that any assembly program produced by the CompCert compiler falls into the subset of programs that have a hope of having their semantics preserved by an optimising assembler.
    563564
Note: See TracChangeset for help on using the changeset viewer.