Specifying Relaxed Concurrent Data Structures Using NADTs

Abstract

To improve performance scalability of concurrent data structures, one solution is to relax their sequential semantics. While a variety of specification approaches focus on characterizing the relaxed semantics, client-side reasoning using the current methodologies is difficult. We employ nondeterministic abstract data types (NADTs) for the first time to specify the relaxed concurrent data structures, and as instantiations of our specification approach, we propose new correctness criteria of out-of-order queues and stacks. We further prove the relaxation equivalence of the out-of-order dequeue and enqueue operations. Our specification approach is intuitive and generic, and can provide clients with explicit interfaces. As a demonstration of our approach, we specify and verify the k-segment queue.