Name
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∈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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1145/2676726.2677002 | POPL |
Keywords | Field | DocType |
concurrency,linearizability,mechanical verification,refinement | Linearizability,Integer,Synchronization,Interval order,Parameterized complexity,Semaphore,Concurrency,Computer science,Algorithm,Theoretical computer science,Bounded function | Conference |
Volume | Issue | ISSN |
50 | 1 | 0362-1340 |
Citations | PageRank | References |
17 | 0.66 | 26 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ahmed Bouajjani | 1 | 2663 | 184.84 |
| Michael Emmi | 2 | 365 | 21.76 |
| Constantin Enea | 3 | 249 | 26.95 |
| Jad Hamza | 4 | 71 | 6.44 |