A Reliable Non-Intrusive Runtime Verification Framework for 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.