# Verified Compilation of Linearizable Data Structures

## Mechanizing Rely Guarantee for Semantic Refinement

## Accepted paper at the Software Verification and Testing track at the 33rd ACM/SIGAPP Symposium on Applied Computing.

[SimuLin.pdf]

## Source code of the Coq formalization

Download the Coq development.

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:

- git clone https://gforge.inria.fr/git/ppsimpl/ppsimpl.git
Then, in the ppsimpl directory, do

- ./configure
- make && make install

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