This is the associated Coq development for the paper: Ori Lahav and Viktor Vafeiadis. Explaining Relaxed Memory Models with Program Transformations. Submitted. 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.5, using the standard library and the files provided in this tarball. To compile the whole development, you need to have Coq 8.5 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 * extralib.v Additions to the standard library * ExtraRelations.v Many lemmas about relations, including minimal cycle lemmas * cactions.v Definition of events * WMModels.v Definitions of various versions of the SC, RA, SRA, TSO models (Sections 2, 4 and 5 of the paper) * SCresults.v Equivalence of the various SC-coherence definitions (Section 2.1) * RAresults.v Results about RA and SRA (from the POPL'16 paper of Lahav et al.) * TSOresults.v Results about TSO including the proof of Theorem 1 (Section 4) * PowerFull.v Formalization of the TOPLAS'14 Power model of Alglave et al. Proof of Theorem 2 (Section 6) **[ 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.