Formal Machine-Verification of MemSnap: An Efficient, Far-Future Linearizable Snapshot Algorithm

In this work, we consider the MemSnap algorithm [Jayanti et al., PODC 2024]---an efficient, yet extremely intricate solution to the adaptive snapshot problem---and give a formally machine-verified proof of its correctness, i.e., linearizability. An adaptive snapshot object maintains m components and supports operations to read, write, and update individual components (via arbitrary hardware read-modify-write operations), a click operation to take a fast (implicit) snapshot of all of the components, and an operation to observe the value of any component in the latest snapshot. Expressed in just 12 total lines of pseudocode, MemSnap is succinct. Simultaneously, it achieves optimal time and space complexity, implementing each operation in just O(1) steps and requiring only O(m) space to store the entire data structure consisting of m components. Nevertheless, the algorithm is extremely intricate and challenging to prove correct, especially since it is far-future linearizable, meaning that the precise linearization point of an operation may be indeterminate even after the operation returns a response. In our work, we formalize the enhanced version of MemSnap, which enables a very useful parallel primitive, called parallel observation. In particular, if the scanner has access to parallelism, it can scan a complete snapshot of the m components in O(m) work with an O(1) span using MemSnap. We formalize MemSnap in TLA+ (based on Lamport's temporal logic of actions) and develop a complete machine-verified proof of its linearizability. Our proof, consisting of 14,000 lines of TLA+ code, is verified by TLAPS (the TLA+ Proof System), and is the first machine-verified proof of this elegant and complex algorithm.