Tractable Refinement Checking For Concurrent Objects

Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Yet programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations - or in formal terms, one risks violating observational refinement. Testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations.We develop a polynomial-time (per execution) approximation to refinement checking. The approximation is parameterized by an accuracy k is an element of N representing the degree to which refinement violations are visible. In principle, more violations are detectable as k increases, and in the limit, all are detectable. Our insight for this approximation arises from foundational properties on the partial orders characterizing the happens-before relations between object invocations: they are interval orders, with a well defined measure of complexity, i.e., their length. Approximating the happens-before relation with a possibly-weaker interval order of bounded length can be efficiently implemented by maintaining a bounded number of integer counters. In practice, we find that refinement violations can be detected with very small values of k, and that our approach scales far beyond existing refinement-checking approaches.