Sciweavers

PODC
2010
ACM
14 years 3 months ago
Verifying linearizability with hindsight
We present a proof of safety and linearizability of a highlyconcurrent optimistic set algorithm. The key step in our proof is the Hindsight Lemma, which allows a thread to infer t...
Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev,...