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.

翻译：暂无翻译