On Library Correctness under Weak Memory Consistency (artifact)

This artifact contains Rocq formalizations of some proofs presented in the paper.

We provide the artifact in two forms:

• VirtualBox virtual machine image (1.5 GB) which contains everything needed to test the artifact "out of the box". The virtual machine comes with Bodhi Linux 5.0.0 with Coq 8.8.2 already installed.
• Tarball containing the original Coq development (110 kB) in case you want to test the artifact using your local installation of Coq. If you select this option, please make sure you have Coq version 8.8.2 installed.
• .zip file containing the proof development ported to Rocq version 8.20.1 (197 kB)

Please note that the compilation requires 8 GB of RAM. In case you do not have that much RAM avalilable, you should be able to compile all the files except ImplLockedQueue2.v.

Organization of the Coq development:

1. The directory hahn contains a helper library for manipulating lists and binary relations. More information on this library can be found on https://github.com/vafeiadis/hahn.
2. The part of the development corresponding to the paper is contained in the wlib directory. This directory contains the following files.
   1. Language.v and LangSemantics.v
      These files contain the definition of the programing language and its semantics. In the paper, the programing language is introduced in §2, and its semantics in §3.
   2. ExpandFcall.v
      This file contains basic facts regarding the expansion of function calls in our programming language.
   3. Operations.v
      This file contains the definition of the data type used to represent function calls in our programming language. The name of the data type is operation.
   4. LibBase.v
      This file contains formalization of §4.1 of the paper. Here you can find the definitions of library specification, execution, encapsulation, and consistency.
   5. ImplBase.v
      This file contains the formalization of the modularity theorem (Theorem 1 in the paper), and provides the general framework for proving correctness of library implementations. (§4.2 in the paper.)
   6. LibC11.v
      This file contains formulation of RC11 in terms of our library framework. We use this library as the base library on top of which we build all other implementations. (See Remark 1 in the paper.)
   7. LibReg.v
      This file contains formalization of the Example 1.
   8. LibLock.v and ImplLock.v
      These files contain the specification of the mutex library (see §5.1), and the correctness proof for the spinlock implementation.
   9. LibExchanger.v
      This file contains the specification of the exchanger library (§5.2).
   10. LibQueue.v, ImplLockedQueue.v, and ImplLockedQueue2.v
       These files contain the (strong) queue specification (§5.3), and the correctness proof for the globally locked queue implementation.
   11. LibStack.v
       This file contains the specification of the stack library (§5.4).
   12. impl_resources.v
       This file contains some helper lemmas used in the correctness proofs (Impl*.v files).