Compilation correctness from Promising 1.0 to IMM

Related papers

• [POPL19] Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
  [Paper | arXiv | POPL19 arifact release]
  Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis

Building the Project

Requirements

• Coq 8.9.1
• Hahn library (coq-hahn)
• The Coq development of IMM (coq-imm.1.2)

Building Manually

To build the project, one needs to install some libraries (imm, promising-coq, hahn, coq-imm.1.2), which the project depends on. This might be done by running ./configure. The command installs Coq as well. After that, one needs to run make (or make -j4 for a faster build).

Description of code and its relation to Sections 6 and 7 of the [Podkopaev-al:POPL19] paper

• Promise.v—a definition of a Promise outcome (Def. 6.1).
• PromiseFuture.v— a proof that it is enough to show certification only for a restricted set of future memories (Remark 3).
• SimulationRel.v—a simulation relation (Section 7.3).
• SimulationPlainStep.v— a proof of simulation step (Prop. 7.8).
• PlainStepBasic.v, WritePlainStep.v, FencePlainStep.v, RMWPlainStep.v, ReadPlainStep.v, ReadPlainStepHelper.v—auxiliary lemmas for the simulation step proof.
• SubExecution.v, CertCOhelper.v, CertExecution1.v, CertExecution2.v, Receptiveness.v, CertGraphInit.v—construction of the certification graph and proofs of its properties (Section 7.4).
• PromiseToIMMs.v—a proof of the compilation correctness from Promise to IMMs (Prop. 6.8 and 6.9, Thm. 7.1).

Auxiliary files: MaxValue.v, Event_imm_promise.v, SimStateHelper.v, SimulationPlainStepAux.v, SimulationRelAux.v, ViewRel.v, MemoryAux.v.