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.


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