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 |
