Tractable Refinement Checking for Concurrent Objects

Ahmed Bouajjani
Université Paris Diderot - Paris VII
Friday, 28 November, 2014 - 14:00
Forum D

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$ (a natural number) 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.

This is a joint work with Michael Emmi, Constantin Enea, and Jad Hamza.