--- res: bibo_abstract: - "Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on identifying the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates.\r\nIn response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof.@eng" bibo_authorlist: - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Ali foaf_name: Sezgin, Ali foaf_surname: Sezgin foaf_workInfoHomepage: http://www.librecat.org/personId=4C7638DA-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Viktor foaf_name: Vafeiadis, Viktor foaf_surname: Vafeiadis bibo_doi: 10.1007/978-3-642-40184-8_18 bibo_volume: 8052 dct_date: 2013^xs_gYear dct_language: eng dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@ dct_title: Aspect-oriented linearizability proofs@ ...