This is the associated Coq development for the paper:

  Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis.
  Taming Release-Acquire Consistency.
  In POPL 2016.

The Coq development is copyrighted (c) Viktor Vafeiadis and is
released under a BSD-style license included at the end of this file.

For more information, visit   http://plv.mpi-sws.org/sra/


**[ INSTALLATION INSTRUCTIONS ]**********************************************

The proofs were developed under Coq 8.6, using the standard library and 
the files provided in this tarball. To compile the whole development,
you need to have Coq 8.6 installed  (available at http://coq.inria.fr/)
Then, open a shell script and type "make".

The development consists of the following Coq files:

* Vbase.v 
    A standard library of tactics

* ExtraRelations.v
    Many lemmas about relations, including minimal cycle lemmas

* cactions.v 
    Definition of events

* RAmodels.v
    Definitions of the RA and SRA models and lemmas about them 
    (Sections 2 and 3 of the paper)

* Transformations.v 
    Validity of local program transformations w.r.t. SRA 
    (Section 3.1 of the paper)
    
* SCreduction.v
    Properties of fences in (S)RA and the two reduction theorems from RA to SC 
    (Section 5)

* TSO.v
    Formalization of the TSO memory model.
    Proof that it is equivalent to the alternative formulation.
    Reduction theorem from RA to TSO for client-server programs.
    (Section 6)

* PowerFull.v
    Formalization of the TOPLAS'14 Power model of Alglave et al. 
    Proof that the alternative semantics of "sync" fences is equivalent to Power's. 
    (Section 7)

* RMWequiv.v
    Proof that the SRA model is equivalent to a variant without update events
    that instead splits them to a read and a write events.
    This is used to simplify the correspondence to Power.
    (not in the paper)

* PowerRA.v
    A simplification of the TOPLAS'14 model for the release/acquire fragment.
    Proof that SRA and PowerRA (i.e., the restriction of Power) are equivalent.
    (Section 7)

**[ LICENSE ]****************************************************************

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,
   this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
   this list of conditions and the following disclaimer in the documentation
   and/or other materials provided with the distribution.
3. Neither the name of the author nor the names of its contributors may be
   used to endorse or promote products derived from this software without
   specific prior written permission.

This formalization is provided by the copyright holders and contributors
"as is" and any express or implied warranties, including, but not limited
to, the implied warranties of merchantability and fitness for a particular
purpose are disclaimed.  In no event shall the copyright owner or
contributors be liable for any direct, indirect, incidental, special,
exemplary, or consequential damages (including, but not limited to,
procurement of substitute goods or services; loss of use, data, or profits;
or business interruption) however caused and on any theory of liability,
whether in contract, strict liability, or tort (including negligence or
otherwise) arising in any way out of the use of this formalization, even if
advised of the possibility of such damage.