Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs

Zachary Kent, Ugur Y. Yavuz, Siddhartha Jayanti +2

In the past decade, many techniques have been developed to prove linearizability, the gold standard of correctness for concurrent data structures. Intuitively, linearizability requ…