Authors: Siddhartha Jayanti (Dartmouth), Ugur Yavuz (BU).
This repository contains the auxiliary material for our SPAA 2025 paper "Formal Machine-Verification of MemSnap: An Efficient, Far-Future Linearizable Snapshot Algorithm". It provides a formal specification of the adaptive snapshot type along with machine-verified proofs about the type and its implementation MemSnap (Jayanti et al., 2024), including its proof of linearizability through the meta-configuration tracking technique (Jayanti, Jayanti, Yavuz, & Hernandez, 2024) in TLA+/TLAPS. All proofs have been mechanically verified in TLAPS 1.5.0.
| Module | Description |
|---|---|
| AdaptiveSnapshot | Defines the adaptive snapshot type, compatibly with meta-configuration tracking. |
| AdaptiveSnapshotTheorems_proofs | TLAPS proofs for the theorems defined in AdaptiveSnapshotTheorems. |
| AdaptiveSnapshotTheorems | Contains a set of theorems about the adaptive snapshot type and its transition functions. |
| AdaptiveSnapshotTheorems_proofs | TLAPS proofs for the theorems in the AdaptiveSnapshotTheorems module. |
| Module | Description |
|---|---|
| MCTracking | Implements the machinery for meta-configuration tracking, including the invocation, evolution, and filtering of configurations, and associated theorems. |
| MCTracking_proofs | TLAPS proofs for the theorems in the MCTracking module. |
| Module | Description |
|---|---|
| MemSnap | Defines the MemSnap algorithm, an adaptive snapshot implementation. |
| MemSnapWFTheorems | Defines the well-formedness theorems for the MemSnap algorithm, covering key properties such as type correctness. |
| MemSnapWFTheorems_proofs | TLAPS proofs for the theorems defined in MemSnapWFTheorems. |
| MemSnapForwardingTheorems | Contains theorems related to the forwarding mechanism of the MemSnap algorithm. |
| MemSnapForwardingTheorems_proofs | TLAPS proofs for the theorems in MemSnapForwardingTheorems. |
| MemSnapMCTrackingTheorems | Contains the theorem that proves MemSnap is a linearizable adaptive snapshot implementation through meta-configuration tracking. |
| MemSnapMCTrackingTheorems_proofs | TLAPS proofs of the theorems in MemSnapMCTrackingTheorems. |
| MemSnapLinearizability | Contains the main theorem proving the linearizability of MemSnap, and its TLAPS proof. This follows as a corollary of theorems in MemSnapMCTrackingTheorems. |
| Module | Description |
|---|---|
| Assumptions | Contains a few assumptions that are used throughout other modules. |
| Permutations | Contains theorems about permutations of finite sets. |
| Permutations_proofs | TLAPS proofs for the theorems in the Permutations module. |