Quantitative Relaxation of Concurrent Data Structure

VCLA hosted a RiSE seminar talk by Ana Sokolova on June 14th, 2012.

ABSTRACT

This talk reports on a true RiSE cooperation. I will present joint work with Thomas A. Henzinger and Ali Sezgin from IST Austria as well as Christoph M. Kirsch and Hannes Payer from the University of Salzburg. The cooperation was initiated during one of the RiSE meetings.

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 A of method calls. Relaxing the data structure corresponds to defining a distance from any sequence over A to the sequential specification: the relaxed sequential specification Sk contains all sequences over A within distance k from S. 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 a simple yet generic relaxation scheme. We show that this relaxation, when further instantiated on queues, stacks, 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 also present various concurrent implementations of queue, stack, and priority queue relaxations and argue 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 increases the performance.