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

DOI10.1007/978-3-030-31157-5_10MaRDI QIDQ6536175zbMATH OpenFDO

Authors Aurélie Hurault, Philippe Quéinnec

Publication date 5 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-31157-5_10

zbMATH Keywords

formal verificationnon-blocking algorithmTLA\textsuperscript{+}

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)

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

Cites work

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

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)