Quantitative Quiescent Consistency: A correctness criterion for concurrent objects

Linearizability is the defacto correctness criterion for concurrent data structures.  Unfortunately, the performance penalty imposed by linearizability scales linearly with the number of contending threads.   Consequently, Herlihy and Shavit propose Quiescent Consistency (QC), an alternative correctness criterion for concurrent data structures.

QC imposes very weak constraints on the implementation when there are open concurrent method calls. We propose an alternative criterion, Quantitative Quiescent Consistency (QQC).  Whereas QC only constrains the behavior of a data structure across quiescent points when there are no open calls, QQC also constrains it at every moment by counting the number of open calls: the implementation can be ``off'' of the specification by an amount proportional to the number of open calls.

The high performance data structures developed by Herlihy and Shavit continue to satisfy QQC.

We study the metatheory of QQC.  We show that QQC satisfies compositionality.  In order to illustrate the flexibility provided by QQC, we provide an opsem with a notion of speculation that generates only QQC consistent behaviors of the data structure.

Joint work with James Riely.