Quantitative Relaxation of Concurrent Data Structures

Description (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 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 obtain new concurrent pool implementations that outperform the state-of-the-art ones.

Link to the paper

Questions

Question 1: What are the states (or state representatives) of a Stack? Give the transitions corresponding to the sequential specification of a stack.

Question 2: Let enq(a)enq(b)enq(c)enq(d) be a Queue trace (shape: Tail -> d -> c -> b -> a -> Head).
a) What are the elements that can be returned by a pop operation on the k=2 restricted out-of-order relaxation of the Queue.
b) Suppose b was returned but not deleted. What are the elements that can be returned by a pop operation on the k=3 out-of-order relaxation of the Queue?

Martin Q1: [s] --push(a)--> [s push(a)] [s] --pop(a)--> [s'] if s == s' push(a) [s] --pop(a)--> [empty] if s == empty Q2: a) a, b, or c b) a, c, or d	Sofia Q1: [ ] --> pop(a) --> [ ] [s push(a)] --> pop(a) --> [s] [s] --> push(a) --> [s push(a)] Q2: a) a, b, c (at most 2 steps) b) a, c, d (at most 3 steps, omitting b)
Andreas Q1: [s] --push(h)-> [s push(h)] [s] --pop(h) -> [s'] if [s] == [s' push(h)] [] if [s] == [] Q2: a) a, b, c (head, head-1, head-2; in general to head-k) b) a, c, d (head -> head-3, without b)	Yunyun Q1: [s] --> push(a) --> [s push(a)] [s push(a)] --> pop(s) --> [s] [] --> pop(_) --> [] Q2: a) a, b, c b) a, c, d
Magnus Q1: [s]: <push(a)> --> [s push(a)] [s]: <pop(a)> --> [s'] if s == s' push(a) [s]: <pop(_)> --> [] if s is empty Q2: a) a, b, c b) a, c, d	Pan Q1: [s] --push(a)--> [s push(a)] [s] --pop(a)-->[s'] if s == s'push(a) [] --pop(null) --> [] Q2: a) a, b, c b) a, c, d
Stavros Q1: [s] --push(a)-> [s push(a)] [s] --pop(a) -> [s'] if [s] == [s' push(a)] [] if [s] == [] Q2: a) a, b, c b) a, c, d