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

Self-timed chip designs are commonly specified in a high-level message-passing language called CHP. This language is closely related to Hoare’s CSP except it admits erroneous behavior due to the necessary limitations of efficient hardware implementations. For example, two processes sending on the same channel at the same time causes glitches and short circuits in the physical chip implementation. If a CHP program maintains certain invariants, such as only one process is sending on any given channel at a time, it can guarantee an error-free execution that behaves much like a CSP program would. In this paper, we present an inferable effect system for ensuring that these invariants hold, drawing from model-checking methodologies while exploiting language-usage patterns and domain-specific specializations to achieve efficiency. This analysis is sound, and is even complete for the common subset of CHP programs without data-sensitive synchronization. We have implemented the analysis and demonstrated that it scales to validate even microprocessors.

PLDI 2015 Artifact Evaluated Badge

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 Jagannathan Purdue University
09:15
25m
Talk
Composing Concurrency Control
Research Papers
Ofri Ziv Tel Aviv University, Alex Aiken Stanford University, Guy Golan-Gueta Yahoo Labs, G. Ramalingam Microsoft Research, Mooly Sagiv Tel Aviv University
Media Attached
09:40
25m
Talk
Dynamic Partial Order Reduction for Relaxed Memory Models
Research Papers
Naling Zhang Virginia Tech, Markus Kusano Virginia Tech, Chao Wang Virginia Tech
Media Attached
10:05
25m
Talk
Monitoring Refinement via Symbolic Reasoning
Research Papers
Michael Emmi , Constantin Enea LIAFA, Université Paris Diderot, Jad Hamza LIAFA, Université Paris Diderot
Media Attached
10:30
25m
Talk
Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications
Research Papers
Stephen Longfield Cornell University, Brittany Nkounkou Cornell University, Rajit Manohar Cornell University, Ross Tate Cornell University
Media Attached