Aspect-oriented linearizability proofs

Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency p...

Full description

Bibliographic Details
Main Authors: Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2015-04-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/1051/pdf