Higher-order linearisability

DOI10.1016/J.JLAMP.2019.01.002MaRDI QIDQ2423744zbMATH OpenOpenAlexWikidataFDO

Authors Andrzej S. Murawski, Nikos Tzevelekos

Publication date 20 June 2019

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1610.07965

zbMATH Keywords

concurrencyhigher-order computationlinearisability

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Linearisability is a central notion for verifying concurrent libraries: a given library is proven safe if its operational history can be rearranged into a new sequential one which, in addition, satisfies a given specification. Linearisability has been examined for libraries in which method arguments and method results are of ground type, including libraries parameterised with such methods. In this paper we extend linearisability to the general higher-order setting: methods can be passed as arguments and returned as values. A library may also depend on abstract methods of any order. We use this generalised notion to show correctness of several higher-order example libraries.

Recommendations

• Higher-order linearisability
• Parameterised linearisability
• Linearizability with ownership transfer
• Linearizability with ownership transfer
• Concurrent Library Correctness on the TSO Memory Model

Cites work

• A Fully Abstract Trace Semantics for General References
• A Game Semantics of Idealized CSP
• A fully abstract may testing semantics for concurrent objects
• A system-level game semantics
• Abstraction for concurrent objects
• Foundations of Software Science and Computation Structures
• Higher-order linearisability
• Impredicative concurrent abstract predicates
• Liveness-Preserving Atomicity Abstraction
• Logical relations for fine-grained concurrency
• Parameterised linearisability
• Quarantining weakness. Compositional reasoning under relaxed memory models (extended abstract)
• Specifying and verifying concurrent algorithms with histories and subjectivity
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Verifying linearizability with hindsight

Cited in

(8)

• Checking linearizability of encapsulated extended operations
• Preface to the special issue on open problems in concurrency theory
• Linearizability with ownership transfer
• Linear Realizability
• Linearizability with ownership transfer
• Logical concurrency control from sequential proofs
• Parameterised linearisability
• Higher-order linearisability

This page was built for publication: Higher-order linearisability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2423744)