Verified Compilation of Linearizable Data Structures

Mechanizing Rely Guarantee for Semantic Refinement

The development is known to compile with Coq 8.4pl6 (January 2016).

The development requires the ppsimpl tactic as a dependency, whose sources can be found: here.

To install ppsimpl:

Then, in the ppsimpl directory, do

Our formal development is organised as follow:

Readme: this very file
Makefile: invoke "make" to use
Lib.v: utilities
language.v: syntax and semantics
programming.v : some Coq notations for program syntax and macros
semantical_facts.v: auxilliary lemmas
compile.v: the compilation function
logic.v: formalization of the proof obligations
invariant.v: invariant of hybrid executions
simulation_high.v: the high simulation
simulation_low.v: the low simulation
simulation.v: their composition
behavior.v: main result of the paper -- full version
behavior_simple.v: main result of the paper -- version close to the paper
main.v: alternative formulation of the main result of the paper -- syntactic proof obligations
proof_system.v: a sound, simple proof system
rg_logic.v: a more clever proof system, embedded in the first one
lock.v: case study 1: definition and proof of methods
lock_behavior.v: case study 1: full instantiation for any client
bucket.v: case study 2: definition and proof of methods. Note that buckets are referred to as buffers in the accompagnying paper
bucket_behavior.v: case study 2: full instantiation for any client
util.v, util_arith.v, util_stability.v : various utility lemmas