Formal Machine-Verification of MemSnap

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.

Overview

Adaptive snapshot type modules

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.

Meta-configuration tracking modules

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.

MemSnap modules

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.

Auxiliary modules

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.