This article presents a theoretical study of 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 a variant of the problem, which we call predictive verification, can be solved, if linearizability is verified indirectly. Namely, it shows that (1) linearizability of a class of concurrent implementations can be predictively 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 using only read/write objects. 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, it is obtained a simple and generic methodology for deriving linearizable implementations that runtime verify their responses, and are able to produce a history certifying this, properties that allows the design of concurrent systems in a modular manner with accountable and forensic guarantees. We call such implementations self-enforced linearizable. The results hold not only for linearizability but for a correctness condition that includes generalizations of it such as set-linearizability and interval-linearizability.

Linearizability is the standard correctness condition for concurrent data structures. Even when an algorithm has been proved correct theoretically, translating it into code may introduce subtle errors that are difficult to detect. Existing runtime verification tools rely on intrusive instrumentation that introduces false positives and false negatives, as the observed execution may differ from the actual one. This paper presents an open-source verification framework for runtime verification of linearizability. The framework treats the system as a black box, requiring only the class name of the concurrent implementation. It consists of two layers: an instrumentation layer, that provides two algorithms based on non-linearizable objects that obtain the current execution without modifying the system under inspection; and a monitoring layer, which decides whether the observed execution is linearizable. The framework is sound : if the observed execution is not linearizable, the real execution is also not linearizable, and a witness history is produced. False negatives are possible — the framework may report linearizable when the real execution is not — but this is the best achievable given the impossibility result of [1]. The framework is implemented in Java and Clojure, supports queues, deques, sets, and maps, and can be extended to other data structures by providing their sequential specification. It is intended for the testing phase of concurrent software development, helping developers and researchers validate that a concurrent implementation matches its theoretical design before deployment.

Implementing correct distributed systems is an error-prone task. Runtime Verification (RV) offers a lightweight formal method to improve reliability by monitoring system executions against correctness properties. However, applying RV in distributed settings—where no process has global knowledge—poses fundamental challenges, particularly under full asynchrony and fault tolerance. This paper addresses the Distributed Runtime Verification (DRV) problem under such conditions. In our model, each process in a distributed monitor receives a fragment of the input word describing system behavior and must decide whether this word belongs to the language representing the correctness property being verified. Hence, the goal is to decide languages in a distributed fault-tolerant manner. We propose several decidability definitions, study the relations among them, and prove possibility and impossibility results. One of our main results is a characterization of the correctness properties that can be decided asynchronously. Remarkably, it applies to any language decidability definition. Intuitively, the characterization is that only properties with no real-time order constraints can be decided in asynchronous fault-tolerant settings. These results expose the expressive limits of DRV in realistic systems, as several properties of practical interest rely on reasoning about real-time order of events in executions. To overcome these limitations, we introduce a weaker model where the system under inspection is verified indirectly. Under this weaker model we define predictive decidability, a decidability definition that turn some real-time sensitive correctness properties verifiable. Our framework unifies and extends existing DRV theory and sharpens the boundary of runtime monitorability under different assumptions.

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.