A Revised and Verified Proof of the Scalable Commutativity Rule

Lillian Tsai, Eddie Kohler, M. Frans Kaashoek +1

This paper explains a flaw in the published proof of the Scalable Commutativity Rule (SCR), presents a revised and formally verified proof of the SCR in the Coq proof assistant, an…