Event Entry
What and Who
A Fast, Correct Time-Stamped Stack
Date, Time and Location
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 (represented by unordered timestamps) if their
associated insert operations ran concurrently, and order imposed as
necessary by the eventual remove operations.
We realise our approach in a new non-blocking data-structure, the TS
(timestamped) stack. 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 have developed a new stack theorem, mechanised in Isabelle,
which characterises the orderings sufficient to establish stack
semantics. By applying our stack theorem, we can show that the TS
stack is indeed correct.
Contact
Video Broadcast
Brigitta Hansen, 08/05/2014 14:25 -- Created document.