Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. 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. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations.
We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Empirically, we find that our approach is practically complete, in that we detect nearly all violations arising in actual executions.
Tue 16 JunDisplayed time zone: Tijuana, Baja California change
09:15 - 10:55
|Composing Concurrency Control|
Ofri Ziv Tel Aviv University, Alex Aiken Stanford University, Guy Golan-Gueta Yahoo Labs, G. Ramalingam Microsoft Research, Mooly Sagiv Tel Aviv UniversityMedia Attached
|Dynamic Partial Order Reduction for Relaxed Memory Models|
Research PapersMedia Attached
|Monitoring Refinement via Symbolic Reasoning|
Michael Emmi , Constantin Enea LIAFA, Université Paris Diderot, Jad Hamza LIAFA, Université Paris DiderotMedia Attached
|Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications|
Stephen Longfield Cornell University, Brittany Nkounkou Cornell University, Rajit Manohar Cornell University, Ross Tate Cornell UniversityMedia Attached