Quantitative relaxation of concurrent data structures

Henzinger, Thomas A and Kirsch, Christoph M and Payer, Hannes and Sezgin, Ali and Sokolova, Ana (2013) Quantitative relaxation of concurrent data structures. In: POPL: Principles of Programming Languages., January 23 - 25, 2013 , Rome, Italy.

[img] Text
popl128-henzinger-clean.pdf - Accepted Version
Available under License All rights reserved.
[IST-2014-198-v1+1]
Download (287Kb)
Official URL: http://dl.acm.org/citation.cfm?id=2429109

Abstract

There is a trade-off between performance and correctness in implementing concurrent data structures. Better performance may be achieved at the expense of relaxing correctness, by redefining the semantics of data structures. We address such a redefinition of data structure semantics and present a systematic and formal framework for obtaining new data structures by quantitatively relaxing existing ones. We view a data structure as a sequential specification S containing all "legal" sequences over an alphabet of method calls. Relaxing the data structure corresponds to defining a distance from any sequence over the alphabet to the sequential specification: the k-relaxed sequential specification contains all sequences over the alphabet within distance k from the original specification. In contrast to other existing work, our relaxations are semantic (distance in terms of data structure states). As an instantiation of our framework, we present two simple yet generic relaxation schemes, called out-of-order and stuttering relaxation, along with several ways of computing distances. We show that the out-of-order relaxation, when further instantiated to stacks, queues, and priority queues, amounts to tolerating bounded out-of-order behavior, which cannot be captured by a purely syntactic relaxation (distance in terms of sequence manipulation, e.g. edit distance). We give concurrent implementations of relaxed data structures and demonstrate that bounded relaxations provide the means for trading correctness for performance in a controlled way. The relaxations are monotonic which further highlights the trade-off: increasing k increases the number of permitted sequences, which as we demonstrate can lead to better performance. Finally, since a relaxed stack or queue also implements a pool, we actually have new concurrent pool implementations that outperform the state-of-the-art ones.

Item Type: Conference or Workshop Item (Paper)
DOI: 10.1145/2480359.2429109
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems
000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 004 Data processing & computer science
500 Science > 510 Mathematics
Research Group: Henzinger Group
Depositing User: Cezara Dragoi
Date Deposited: 28 Apr 2014 09:10
Last Modified: 07 Mar 2017 14:09
URI: https://repository.ist.ac.at/id/eprint/198

Actions (login required)

View Item View Item