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

Added reference to CompCert? and CompCertTSO.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.