Atomicity Refinement for Verified Compilation

This page complements a submission to TOPLAS; last update on 2013-09-20.

Disclaimer

The development available here slightly differs from what is described in the paper. In particular the rely-guarantee methodology is encoded in a permission system.

Download the Coq development

[.tgz] (150kio, tested with Coq 8.3pl2 and CompCert-TSO 1.12)

Browse the Coq development

The syntax/semantic of the INJECT language

• Permissions
• MemoryMachine
• TSOMemoryMachine
• INJECT

The syntax/semantic of the RTLinject language

• RTLinject

The definition of refines and the compositional rules

• RefinesDefs
• AllRefinesRulesAux
• AllRefinesRules

Injected Code

• InjectedCode
• GCthread
• RefinesInjectedCodes

Certified backend RTLinject → Asm

• RTLinjectlow
• RTLofRTLinject
• RTLofRTLinjectspec
• RTLofRTLinjectproof

MIR compiler and sample programs

• MIR
• RTLinjectgen
• MIRcompiler
• MIRexample