Name
Abstract | ||
|---|---|---|
High-performance implementations of distributed and multicore shared objects often guarantee only the weak consistency of their concurrent operations, foregoing the de-facto yet performance-restrictive consistency criterion of linearizability. While such weak consistency is often vital for achieving performance requirements, practical automation for checking weak-consistency is lacking. In principle, algorithmically checking the consistency of executions according to various weak-consistency criteria is hard: in addition to the enumeration of linearizations of an execution's operations, such criteria generally demand the enumeration of possible visibility relations among the linearized operations; a priori, both enumerations are exponential.In this work we identify an optimization to weak-consistency checking: rather than enumerating every possible visibility relation, it suffices to consider only the minimal visibility relations which adhere to the various constraints of the given criterion, for a significant class of consistency criteria. We demonstrate the soundness of this optimization, and describe an associated minimal-visibility consistency checking algorithm. Empirically, we show that our algorithm significantly outperforms the baseline weak-consistency checking algorithm, which naively enumerates all visibilities, and adds only modest overhead to the baseline linearizability checking algorithm, which does not enumerate visibilities. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-96145-3_26 | COMPUTER AIDED VERIFICATION (CAV 2018), PT I |
Keywords | DocType | Volume |
Linearizability, Consistency, Runtime verification | Conference | 10981 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Emmi | 1 | 365 | 21.76 |
| Constantin Enea | 2 | 249 | 26.95 |