In this paper, we consider the problem of automatically monitoring linearizability. Here, one observes an execution of a concurrent program that interacts with a concurrent object and determines if the execution witnesses the violation of linearizability with respect to the sequential specification of the underlying data structure of the concurrent object. This problem has been extensively studied in the past for read-write registers, and both tight upper and lower bounds have been proposed in this case. While this problem has also been studied for the case of other prominent data structures such as stacks and queues, we find that these results are either not extensive or in some cases incorrect. In this paper, we study the problem under the restriction where values inserted in the data types are distinct (in the execution observed). We then show that under such a restriction, the linearizability problem is solvable in polynomial time for these data types. Beyond theoretical soundness and completeness, the algorithms proposed are empirically proven to outperform all state-of-the-art linearizability monitors.

翻译：本文研究线性一致性的自动监测问题。该问题关注对并发程序与并发对象交互执行的观测，并判定该执行是否违反了相对于底层数据结构顺序规范的线性一致性。过去，针对读写寄存器的此类问题已得到广泛研究，并提出了严格的上界与下界。尽管针对栈、队列等其他重要数据结构的研究也已开展，但我们发现现有结果要么不够全面，要么在某些情况下存在错误。本文在数据类型中插入值（在观测的执行中）互不相同的限制条件下研究该问题。我们证明在此限制下，针对这些数据类型的线性一致性问题可在多项式时间内求解。除理论上的可靠性与完备性外，所提算法经实证检验，其性能优于所有现有最先进的线性一致性监测器。