Verification of a Concurrent Deque Implementation
R. D. Blumofe, C. G. Plaxton, and S. Ray
Technical Report TR-99-11, Department of Computer Sciences, University
of Texas at Austin, June 1999.
Abstract
We prove the correctness of the concurrent deque component of a recent
implementation of the work-stealing algorithm. Specifically, we prove that this
concurrent deque implementation is synchronizable. Synchronizability is a
weaker condition than the more traditional notion of serializability. Our
concurrent deque implementation is not serializable, but its synchronizability
makes it sufficient for use in the work-stealing algorithm. Whereas
serializability requires that concurrent method invocations appear as if they
are executed atomically in some serial order, synchronizability allows some
invocations to appear as if they are executed atomically at exactly the same
time.
Relevant files