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.

翻译：本文研究了运行时验证线性一致性的问题，即设计一种并发算法，用于验证给定并发共享对象实现的当前执行是否满足线性一致性。研究表明，对于某些常见的顺序对象，无论基础对象的共识能力如何，运行时验证线性一致性均是不可能的。随后论证了若通过间接方式验证线性一致性，则可解决该问题的更强版本。具体而言，本文展示了：(1) 仅使用读写基础对象（即无需共识机制）即可对某一类并发实现进行强线性一致性验证；(2) 仅使用读写对象即可将任意实现转化为同一对象类型的该类实现。据我们所知，这是首个完全异步且容错的正确性条件运行时验证算法。作为副产品，本文获得了一种简单通用的自强制线性一致性实现推导方法。此类实现输出的结果被保证满足线性一致性，并能生成对应的证书，从而支持以模块化方式设计具有可问责性与司法保证性的并发系统。这些结论不仅适用于线性一致性，还适用于其泛化形式（如集合线性一致性与区间线性一致性）所涵盖的正确性条件。