Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

DOI10.1145/3583668.3594563arXiv2301.02638MaRDI QIDQ6202229FDOQ6202229

Authors: Armando Castañeda 

Publication date: 26 March 2024

Published in: Proceedings of the 2023 ACM Symposium on Principles of Distributed Computing (Search for Journal in Brave)

Abstract: This paper studies the problem of verifying linearizability at runtime, where one seeks for a concurrent algorithm for verifying that the current execution of a given concurrent shared object implementation is linearizable. It shows that it is impossible to runtime verify linearizability for some common sequential objects, regardless of the consensus power of base objects. Then, it argues that actually a stronger version of the problem can be solved, if linearizability is verified indirectly. Namely, it shows that (1) linearizability of a class of concurrent implementations can be strongly verified using only read/write base objects (i.e. without the need of consensus), and (2) any implementation can be transformed to its counterpart in the class (which implements the same object) using only read/write objects too. As far as we know, this is the first runtime verification algorithm for any correctness condition that is fully asynchronous and fault-tolerant. As a by-product, a simple and generic methodology for deriving self-enforced linearizable implementations is obtained. This type implementations produce outputs that are guaranteed linearizable, and are able to produce a certificate of it, which allows the design of concurrent systems in a modular manner with accountable and forensic guarantees. These results hold not only for linearizability but for a correctness condition that includes generalizations of it such as set-linearizability and interval-linearizability.

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

zbMATH Keywords

verificationfault-toleranceshared memorymonitoringwait-freedomlinearizabilitylock-freedomenforcementconcurrent algorithmsdistributed runtime verification

Mathematics Subject Classification ID

Distributed algorithms (68W15) Distributed systems (68M14)

Cites Work

• An overview of the runtime verification tool Java PathExplorer
• Forward and backward simulations. I. Untimed Systems
• Distributed verification and hardness of distributed approximation
• Causal memory: definitions, implementation, and programming
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Time, clocks, and the ordering of events in a distributed system
• Impossibility of distributed consensus with one faulty process
• Atomic snapshots of shared memory
• Locality and checkability in wait-free computing
• Atomizer: A dynamic atomicity checker for multithreaded programs
• Failure-aware Runtime Verification of Distributed Systems
• Quantitative relaxation of concurrent data structures
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Testing Shared Memories
• Verifying Concurrent Programs against Sequential Specifications
• Runtime verification with minimal intrusion through parallelism
• Tractable refinement checking for concurrent objects
• Locality and checkability in wait-free computing
• Deciding and verifying network properties locally with few output bits
• A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring
• Unifying Concurrent Objects and Distributed Tasks
• Decentralized Asynchronous Crash-resilient Runtime Verification

This page was built for publication: Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

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