Tasks in modular proofs of concurrent algorithms

DOI10.1016/j.ic.2023.105040arXiv1909.05537MaRDI QIDQ6044466

Aurélie Hurault, Matthieu Roy, Philippe Quéinnec, Armando Castañeda

Publication date: 19 May 2023

Published in: Information and Computation (Search for Journal in Brave)

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

zbMATH Keywords

verificationformal methodslinearizabilityconcurrent algorithmsrenamingsplitterdistributed tasks\(\mathrm{TLA}^+\)

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The renaming problem in shared memory systems: an introduction
• Tight bounds for adopt-commit objects
• A scalable lock-free stack algorithm
• A calculus of communicating systems
• More \(choices\) allow more \(faults\): Set consensus problems in totally asynchronous systems
• Elimination trees and the construction of pools and stacks
• Modular verification of concurrency-aware linearizability
• Wait-free algorithms for fast, long-lived renaming
• Round-by-round fault detectors (extended abstract)
• Byzantizing Paxos by Refinement
• The topological structure of asynchronous computability
• Concurrent Programming: Algorithms, Principles, and Foundations
• The PlusCal Algorithm Language
• Renaming in an asynchronous environment
• Unifying Concurrent Objects and Distributed Tasks
• The BG distributed simulation algorithm
• Verifying linearizability with hindsight
• Generalized FLP impossibility result for t-resilient asynchronous computations
• Nonblocking Concurrent Data Structures with Condition Synchronization
• MCMT: A Model Checker Modulo Theories