Verifying linearizability with hindsight

DOI10.1145/1835698.1835722zbMath1315.68068OpenAlexW2157062942MaRDI QIDQ5176190

Martin Vechev, Noam Rinetzky, Greta Yorsh, Eran Yahav, Peter W. O'Hearn

Publication date: 2 March 2015

Published in: Proceedings of the 29th ACM SIGACT-SIGOPS symposium on Principles of distributed computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1835698.1835722

zbMATH Keywords

linearizabilitywait-freedomhindsightoptimistic concurrency

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Parallel algorithms in computer science (68W10) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Tasks in modular proofs of concurrent algorithms ⋮ Higher-order linearisability ⋮ Proving Linearizability Using Partial Orders ⋮ Abstract Specifications for Concurrent Maps ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra

Uses Software

• CCSTM

Cites Work

• Elastic Transactions
• Toward a theory of transactional contention managers
• Software transactional memory

This page was built for publication: Verifying linearizability with hindsight