|
3.30 p.m., Seminar Hall CMI Silver Jubilee Lecture Tractable Refinement Checking for Concurrent Objects Prof. Ahmed Bouajjani LIAFA, Univ. of Paris Denis Diderot (Paris 7). 22-01-15 Abstract 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.
|
