Quantitative relaxation of concurrent data structures Conference Paper


Author(s): Henzinger, Thomas A; Kirsch, Christoph M; Payer, Hannes; Sezgin, Ali; Sokolova, Ana
Title: Quantitative relaxation of concurrent data structures
Affiliation IST Austria
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.
Keywords: quantitative models; (concurrent) data structures; costs; relaxed semantics
Conference Title: POPL: Principles of Programming Languages
Conference Dates: January 23-25, 2013
Conference Location: Rome, Italy
Publisher: ACM  
Date Published: 2013-01-01
Start Page: 317
End Page: 328
URL:
DOI: 10.1145/2429069.2429109
Notes: This work has been supported by the European Research Council advanced grant QUAREM, the National Research Network RiSE on Rigorous Systems Engineering (Austrian Science Fund S11404- N23), and an Elise Richter Fellowship (Austrian Science Fund V00125). We thank the anonymous referees for their constructive and inspiring comments and suggestions. Ana Sokolova wishes to thank Dexter Kozen and in particular Joel Ouaknine: had they not saved her life, she would have missed a lot of the fun involved in working on this paper and seeing it finished.
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2.  Ali Sezgin
    5 Sezgin
Related IST Austria Work