# Rely-Guarantee Reasoning for Causally Consistent Shared Memory

Ori Lahav (Tel Aviv University) <orilahav@tau.ac.il>
Brijesh Dongol (University of Surrey) <b.dongol@surrey.ac.uk>
Heike Wehrheim (University of Oldenburg) <heike.wehrheim@uni-oldenburg.de>

Coq development accompanying the CAV'23 paper.

## Build

- Requirements: [Coq 8.17.0](https://coq.inria.fr/download)

- Building the project:
	Run "make clean" to remove previous builds (if any).
        Run "make -j".
        It will first make the "Hahn" library.
        (Based on the public library available at https://github.com/vafeiadis/hahn - slightly modified)

- Interactive Theorem Proving: use [ProofGeneral](https://proofgeneral.github.io/) or [CoqIDE](https://coq.inria.fr/download).
  Note that `make` creates `_CoqProject`, which is then used by ProofGeneral and CoqIDE. To use it:
    + ProofGeneral: use a recent version.
    + CoqIDE: configure it to use `_CoqProject`: `Edit` > `Preferences` > `Project`: change `ignored` to `appended to arguments`.

## Contents

The main result formalized here is the equivalence between:
(1) the potential-based system described in §6 the paper (called SRALn in the Coq development); and 
(2) the operational version of the SRA model based on consistent execution graphs (called SRAG in the Coq development), where each step extends the current execution graph with one event (representing some memory access) in a way that keeps the graph SRA-consistent according to the declarative (aka axiomatic) definition of consistency under SRA.

The Coq definition of SRALn (SRALn.v) formalize the paper definitions. 

To prove the equivalence we use forward simulation in one direction and backward simulation for the converse. These techniques are shown to be sound in "Memory_system.v". The simulation relation itself (for both directions) is provided in "Match_SRAn.v".


## Files included
Below, we list the files and briefly explain their contents:

# Helpers
- AuxRel.v: Lemmas about relations, paths, functions and sets (extending the Hahn library).
- Basic.v: Simple technical lemmas about lists (extending Coq's standard library).

# Basic definitions
- Labels.v: Definition of transition labels

# SRAG
- Events.v: Definition of execution graph events
- Execution.v: Definition of execution graphs, their components (reads-from and modification order), their induced relations (e.g., happens-before) and basic properties of execution graphs.
- FG.v: Definition of an extension of an execution graph with one event, and various properties of such extensions. This is the main building block for defining SRAG, which is obtained by placing further restrictions on such extensions.
- Wmax.v: Definition of the maximal write to each location in an execution graph and useful properties.
- Add_max.v: Definition of an extension of an execution graph with one event, when the previous write event is the maximal write (to the relevant location). Required for write and RMW steps of SRAG.
- SRAG.v: Definition of the SRAG memory subsystem.

# SRALn 
- Subseq.v: Definitions of subsequences and lemmas about them (required to define the "lose" step in SRAL and WRAL). It provides two equivalent presentations: (1) a recursive definition; and (2) a "witness"-based definition (where a witness is a strictly increasing mapping between indices).
- SRALn.v: Definition of the SRALn memory subsystem (Section 5 in the paper).

# Simulations and simulation relation
- Memory_system.v: General memory subsystem definitions and simulation arguments.
- Write_lists.v: Basic definitions for handling SRA's "write lists"
- Wmax_t.v: Definition of a maximal write observed by a thread. Needed for establishing the simulation.
- Match_SRAn.v: Simulation relation definition

# SRAG simulates SRALn
- GsimL_read_SRAn.v: read step.
- GsimL_write_SRAn.v: write step.
- GsimL_rmw_SRAn.v: rmw step.
- GsimL_silent_SRAn.v: silent steps.

# SRALn simulates SRAG
- LsimG_read_SRAn.v: read step.
- LsimG_write_SRAn.v: write step.
- LsimG_rmw_SRAn.v: rmw step.

# Final result
- SRALn_SRAG.v: SRALn and SRAG have the same runs.
