Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

DOI10.1145/3583668.3594563MaRDI 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)

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)

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.

Cites work

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

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)