Soham Chakraborty ; Thomas A. Henzinger ; Ali Sezgin ; Viktor Vafeiadis - Aspect-oriented linearizability proofs

lmcs:1051 - Logical Methods in Computer Science, April 1, 2015, Volume 11, Issue 1 - https://doi.org/10.2168/LMCS-11(1:20)2015
Aspect-oriented linearizability proofs

Authors: Soham Chakraborty ; Thomas A. Henzinger ; Ali Sezgin ; Viktor Vafeiadis ORCID-iD

    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 patterns, such as helping and optimistic updates. In 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.


    Volume: Volume 11, Issue 1
    Published on: April 1, 2015
    Accepted on: June 25, 2015
    Submitted on: February 28, 2014
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages
    Fundings :
      Source : OpenAIRE Research Graph
    • Quantitative Reactive Modeling; Funder: European Commission; Code: 267989
    • Semantic Foundations for Real-World Systems; Funder: UK Research and Innovation; Code: EP/H005633/1

    Linked data

    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.disc.2022.5
    • 10.4230/lipics.disc.2022.5
    Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure
    Amram, Gal ; Hayoun, Avi ; Mizrahi, Lior ; Weiss, Gera ;

    12 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 741 times.
    This article's PDF has been downloaded 439 times.