## Abstract

Concurrent data-structures, such as stacks, queues, and deques,

often implicitly enforce a total order over elements in

their underlying memory layout. However, much of this order

is unnecessary: linearizability only requires that elements

are ordered if the insert methods ran in sequence. We propose

a new approach which uses timestamping to avoid unnecessary

ordering. Pairs of elements can be left unordered

if their associated insert operations ran concurrently, and

order imposed as necessary at the eventual removal.

We realise our approach in a new non-blocking datastructure,

the TS (timestamped) stack. Using the same approach,

we can define corresponding queue and deque datastructures.

In experiments on x86, the TS stack outperforms

and outscales all its competitors – for example, it outperforms

the elimination-backoff stack by factor of two. In our

approach, more concurrency translates into less ordering,

giving less-contended removal and thus higher performance

and scalability. Despite this, the TS stack is linearizable with

respect to stack semantics.

The weak internal ordering in the TS stack presents a

challenge when establishing linearizability: standard techniques

such as linearization points work well when there

exists a total internal order. We present a new stack theorem,

mechanised in Isabelle, which characterises the orderings

sufficient to establish stack semantics. By applying our

stack theorem, we show that the TS stack is indeed linearizable.

Our theorem constitutes a new, generic proof technique

for concurrent stacks, and it paves the way for future weakly

ordered data-structure designs.

often implicitly enforce a total order over elements in

their underlying memory layout. However, much of this order

is unnecessary: linearizability only requires that elements

are ordered if the insert methods ran in sequence. We propose

a new approach which uses timestamping to avoid unnecessary

ordering. Pairs of elements can be left unordered

if their associated insert operations ran concurrently, and

order imposed as necessary at the eventual removal.

We realise our approach in a new non-blocking datastructure,

the TS (timestamped) stack. Using the same approach,

we can define corresponding queue and deque datastructures.

In experiments on x86, the TS stack outperforms

and outscales all its competitors – for example, it outperforms

the elimination-backoff stack by factor of two. In our

approach, more concurrency translates into less ordering,

giving less-contended removal and thus higher performance

and scalability. Despite this, the TS stack is linearizable with

respect to stack semantics.

The weak internal ordering in the TS stack presents a

challenge when establishing linearizability: standard techniques

such as linearization points work well when there

exists a total internal order. We present a new stack theorem,

mechanised in Isabelle, which characterises the orderings

sufficient to establish stack semantics. By applying our

stack theorem, we show that the TS stack is indeed linearizable.

Our theorem constitutes a new, generic proof technique

for concurrent stacks, and it paves the way for future weakly

ordered data-structure designs.

Original language | English |
---|---|

Title of host publication | Proceedings of the 42th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. |

Publisher | ACM |

Number of pages | 14 |

Publication status | Published - 2015 |