SPLASH 2020 (series) / ECOOP 2020 (series) / Artifacts /
Reconciling Event Structures with Modern Multiprocessors
The artifact supplementing the paper Reconciling Event Structures with Modern Multiprocessors is a virtual machine image containing two Coq packages which include mechanization of proofs stated in the paper. The first package (imm) contains a modified version of the Intermediate Memory Model, extended with the support of sequentially consistent atomics, and the compilation correctness proofs from it to hardware models. The second package (weakestmoToImm) contains a definition of the Weakestmo memory model as well as a compilation correctness proof from it to IMM.