Checking linearizability with fine-grained traces
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.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
23
References
4
Citations
NaN
KQI