Root Causing Linearizability Violations
Published in International Conference on Computer Aided Verification (CAV), 2020
Recommended citation: Berk Cirisci, Constantin Enea, Azadeh Farzan. "Root Causing Linearizability Violations." In Proceedings of the 31st International Conference on Computer Aided Verification (CAV), 2020.
This paper presents a testing based method for finding root causes of linearizability violations of concurrent libraries.
Abstract. Linearizability is the de facto correctness criterion for concurrent abstract data type implementations. Violation of linearizability is witnessed by an error trace in which the outputs of individual operations do not match sequential executions of the same operations. Extensive work has been done in proving linearizability of concurrent ADTs or discovering linearizability bugs in them. Little work has been done in trying to provide useful hints to the programmer when a violation of linearizability is discovered by a tester tool. In this paper, we propose an approach that identifies the root causes of linearizability errors in the form of code blocks whose atomicity is required to restore linearizability. The key insight of this paper is that the problem can be reduced to a simpler algorithmic problem of identifying minimal root causes of conflict serializability violation in an error trace combined with a heuristic for identifying which of these are more likely to be the true root cause of non-linearizability. We propose theoretical results outlining this reduction, and an algorithm to solve the simpler problem. We have implemented our approach and carried out several experiments on realistic concurrent {ADTs showing its efficiency.