Verification of a Concurrent Deque Implementation

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. 1 Introduction In this paper we prove the correctness of the concurrent deque implementation given in [1] as a component of the work-stealing thread-scheduling algorithm. This implementation is nonblocking, meaning that slow or preempted processes cannot prevent other processes from making progress [2]. No mutual ..