*****************************************************************************

   #####   #####    ####      Formalization of the GPS program logic
  ##       ##  ##  ##         Version 1.7, released 2016-12-20
  ##  ###  #####    ####      
  ##   ##  ##          ##     Copyright (c) Viktor Vafeiadis
   #####   ##       ####      All rights reserved.

*****************************************************************************

Current version 1.7 , released 2016-12-20


*****************************************
*** Version  1.7, released 2016-12-20 ***
*****************************************

Ported development to Coq 8.6

*****************************************
*** Version  1.6, released 2015-06-05 ***
*****************************************

- Replaced escrows by bidirectional exchanges
- Added support for concurrent non-atomic reads with fractional permissions
- Weakened the premise of the ghost update rule to match the paper
- Updated the read-acq and CAS rules to allow the postconditions
  to record the observed state


*****************************************
*** Version  1.5, released 2014-06-04 ***
*****************************************

- Fixed a typo in the semantics of SC accesses
- Removed file c11orig.v accidentally included in the 1.4 release
- Updated the section numberings in the proof to match the appendix


*****************************************
*** Version  1.4, released 2014-01-20 ***
*****************************************

- Added SC and relaxed atomics to the C11 model


*****************************************
*** Version  1.3, released 2014-01-16 ***
*****************************************

- Formalized ghost resource stripping


*****************************************
*** Version  1.2, released 2013-12-17 ***
*****************************************

- Removed dependence on the axiom of propositional extensionality.
- Improved formatting


*****************************************
*** Version  1.1, released 2013-12-10 ***
*****************************************

- Removed unnecessary library dependencies (Varith, Vlistbase, Vlist)


*****************************************
*** Version  1.0, released 2013-12-09 ***
*****************************************

Initial release, contains soundness proof of GPS