Publications

1. A Universal Technique for Machine-Certified Proofs of Linearizable Algorithms. Prasad Jayanti, Siddhartha V. Jayanti, Uğur Y. Yavuz, Lizzie Hernández Videa. arXiv preprint. January 2023. Code

   ^{Abstract: Linearizability has been the long standing gold standard for consistency in concurrent data structures. However, proofs of linearizability can be long and intricate, hard to produce, and extremely time consuming even to verify. In this work, we address this issue by introducing simple universal, sound, and complete proof methods for producing machine-verifiable proofs of linearizability and its close cousin, strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti’s single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the Temporal Logic of Actions Proof System).}

2. A Machine-Verified Proof of Linearizability for a Queue Algorithm. Uğur Y. Yavuz. Master’s thesis. May 2022.

   ^{Abstract: Proofs of linearizability are typically intricate and lengthy, and readers may find it difficult to verify their correctness. We present a unique technique for producing proofs of linearizability that are fully verifiable by a mechanical proof system, thereby eliminating the need for any manual verification. Specifically, we reduce the burden of proving linearizable object implementations correct to the proof of a particular invariant whose correctness can be shown inductively. Noting that the latter is a task that many proof systems (such as the TLA+ Proof System we chose to work with) are well-suited to handle, this technique allows us to shift the responsibility of verification away from the reader and onto a machine, by enabling us to produce mechanically verifiable proofs of linearizability. We then demonstrate the effectiveness of this technique, which heretofore had only been applied to problems of a smaller scale, by proving the linearizability of a well-known queue algorithm whose proof of correctness is known to be challenging.}

3. Producing Easy-to-Verify Proofs of Linearizability. Uğur Y. Yavuz. Bachelor’s thesis (awarded High Honors). June 2021. Available upon request.

   ^{Abstract: Proofs of linearizability tend to be complex and lengthy, rendering their verification challenging for readers. We provide a novel technique to produce easy-to-verify proofs of linearizability, with the help of mechanical proof assistants. Specifically, we reduce the task of proving the correctness of a linearizable object implementation, to a proof of an inductive invariant of a slightly modified version of the implementation. As the latter is a task many mechanical proof systems (such as TLAPS) are well-suited to undertake, this reduction allows the verification of the proof by the reader, to only consist of a trivial syntactic check of whether the modification fulfills certain criteria. To demonstrate the practicability of this technique, we provide two applications.}