Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}

DOI10.1007/978-3-030-31157-5_10zbMATH Open1539.68167MaRDI QIDQ6536175FDOQ6536175

Authors: Aurélie Hurault, Philippe Quéinnec 

Publication date: 5 April 2024

Recommendations

• Tasks in modular proofs of concurrent algorithms
• Tasks in modular proofs of concurrent algorithms
• Wait-free algorithms for fast, long-lived renaming
• Long lived adaptive splitter and applications
• Wait-free linearization with an assertional proof

zbMATH Keywords

formal verificationTLA\textsuperscript{+}non-blocking algorithm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• On interprocess communication. II: Algorithms
• The PlusCal Algorithm Language
• Distributed Computing
• Wait-free algorithms for fast, long-lived renaming
• The renaming problem in shared memory systems: an introduction
• Lock-free dynamic hash tables with open addressing
• Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors
• Elimination trees and the construction of pools and stacks
• How to write a 21\(^{\text{st}}\) century proof
• Computer Aided Verification
• Deep specifications and certified abstraction layers
• Verifying linearizability with hindsight

Cited In (2)

• Tasks in modular proofs of concurrent algorithms
• Tasks in modular proofs of concurrent algorithms

This page was built for publication: Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}

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