CMI Silver Jubilee Lecture

Ahmed Bouajjani, University of Paris Denis Diderot (Paris 7), France

Tractable Refinement Checking for Concurrent Objects

Wednesday, January 22, 2015

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 joint work with Michael Emmi, Constantin Enea, and Jad Hamza.