Wait-free linearization with an assertional proof

DOI10.1007/BF02280829MaRDI QIDQ5136979zbMATH OpenOpenAlexFDO

Authors W. H. Hesselink

Publication date 30 November 2020

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf02280829

zbMATH Keywords

stabilityconsensusinvariantspace complexitytime complexitywait-freecorrectnessmemory managementlinearizableconcurrent data object

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Reliability, testing and fault tolerance of networks and computer systems (68M15) Distributed algorithms (68W15) Distributed systems (68M14)

Recommendations

• Wait-free linearization with a mechanical proof
• A sound and complete proof technique for linearizability of concurrent data structures
• scientific article; zbMATH DE number 1263230
• Proving Linearizability Via Non-atomic Refinement
• Testing and verifying concurrent objects

Cites work

• scientific article; zbMATH DE number 50008 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• An axiomatic proof technique for parallel programs
• Impossibility of distributed consensus with one faulty process
• On-the-fly garbage collection for several mutators
• The Hoare logic of concurrent programs
• The ``Hoare Logic of CSP, and All That

Cited in

(7)

• Wait-free linearization with a mechanical proof
• A simple constructive computability theorem for wait-free computation
• Bounded delay for a free address
• A Single-Enqueuer Wait-Free Queue Implementation
• Universal constructions that ensure disjoint-access parallelism and wait-freedom
• Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}
• Making objects writable

Describes a project that uses

Uses Software

• UNITY

This page was built for publication: Wait-free linearization with an assertional proof

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