Tue 16 Jun 2015 10:05 - 10:30 at PLDI Main BLUE (Portland 254-255) - Concurrency II Chair(s): Suresh Jagannathan

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.

PLDI 2015 Artifact Evaluated Badge

Conference Day
Tue 16 Jun

Displayed time zone: Tijuana, Baja California change

09:15 - 10:55
Concurrency IIResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Suresh JagannathanPurdue University
09:15
25m
Talk
Composing Concurrency Control
Research Papers
Ofri ZivTel Aviv University, Alex AikenStanford University, Guy Golan-GuetaYahoo Labs, G. RamalingamMicrosoft Research, Mooly SagivTel Aviv University
Media Attached
09:40
25m
Talk
Dynamic Partial Order Reduction for Relaxed Memory Models
Research Papers
Naling ZhangVirginia Tech, Markus KusanoVirginia Tech, Chao WangVirginia Tech
Media Attached
10:05
25m
Talk
Monitoring Refinement via Symbolic Reasoning
Research Papers
Michael Emmi, Constantin EneaLIAFA, Université Paris Diderot, Jad HamzaLIAFA, Université Paris Diderot
Media Attached
10:30
25m
Talk
Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications
Research Papers
Stephen LongfieldCornell University, Brittany NkounkouCornell University, Rajit ManoharCornell University, Ross TateCornell University
Media Attached