CMI Silver Jubilee Lecture
Ahmed Bouajjani, University of Paris Denis Diderot (Paris 7), France
Tractable Refinement Checking for Concurrent Objects
Wednesday, January 22, 2015
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 joint work with Michael Emmi, Constantin Enea, and Jad Hamza.