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

DOI10.1007/978-3-030-31157-5_10zbMath1539.68167MaRDI QIDQ6536175

Philippe Quéinnec, Aurélie Hurault

Publication date: 5 April 2024

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)

Related Items (1)

Tasks in modular proofs of concurrent algorithms

Cites Work

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

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