On Library Correctness under Weak Memory Consistency

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

The Coq development is organized as follows.

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.

   a) Language.v & 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.

   b) ExpandFcall.v
      This file contains basic facts regarding the expansion of function calls
      in our programming language. 

   c) 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.

   d) 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.

   e) 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.)

   f) 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.)
      
   g) LibReg.v
      This file contains formalization of the Example 1.

   h) LibLock.v ImplLock.v
      These files contain the specification of the mutex library (see §5.1),
      and the correctness proof for the spinlock implementation.

   i) LibExchanger.v
      This file contains the specification of the exchanger library (§5.2).
  
   j) LibQueue.v ImplLockedQueue.v ImplLockedQueue2.v
      These files contain the (strong) queue specification (§5.3), and the
      correctness proof for the globally locked queue implementation.

   k) LibStack.v
      This file contains the specification of the stack library (§5.4).

   j) impl_resources.v
      This file contains some helper lemmas used in the implementation
      correctness proofs (Impl*.v files).


Additional information:
  - the required version of Coq is 8.20.1
  - compilation requires 8 GB of RAM (the offending file is ImplLockedQueue2.v);
  - More information can be found on the project's web site:
    http://plv.mpi-sws.org/yacovet/
  
