Concurrency control poses significant challenges when composing computations over multiple data-structures (objects) with different concurrency-control implementations. We formalize the usually desired requirements (serializability, abort-safety, deadlock-safety, and opacity) as well as stronger versions of these properties that enable composition. We show how to compose protocols satisfying these properties so that the resulting combined protocol also satisfies these properties. Our approach generalizes well-known protocols (such as two-phase-locking and two-phase-commit) and leads to new protocols. We apply this theory to show how we can safely compose optimistic and pessimistic concurrency control. For example, we show how we can execute a transaction that accesses two objects, one controlled by an STM and another by locking.
Tue 16 JunDisplayed 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 25mTalk | 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 25mTalk | Dynamic Partial Order Reduction for Relaxed Memory Models Research Papers Media Attached | ||
10:05 25mTalk | 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 25mTalk | 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 |