Checking linearizability with fine-grained traces
Zhenyue Long, Yu Zhang · 2016
Linearizability is an important correctness criterion for concurrent objects and automatic checking of linearizability often involves searching a sequential witness in an exponentially growing space of traces. We present two acceleration techniques for checking linearizability based on fine-grained traces: one is based on speculation of linearization points, and the other is to separate read-only methods from the enumeration of serial witnesses. We have applied them to checking linearizability of eight different algorithms and the experiment shows that both can offer significant speed-up, allowing us to explore further on error analysis of concurrent objects based on fine-grained traces.