Mon 15 Jun 2015 17:15 - 17:40 at PLDI Main BLUE (Portland 254-255) - Concurrency I Chair(s): Santosh Nagarakatte

We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics in which concurrent transactions push their effects into the shared view (or unpush to recall effects) and pull the effects of potentially uncommitted concurrent transactions into their local view (or unpull to detangle). Each operation comes with simple side-conditions given in terms of commutativity (Lipton’s left-movers and right-movers).

The benefit of this model is that most of the elaborate reasoning (coinduction, simulation, subtle invariants, etc.) necessary for proving the serializability of a transactional algorithm is already proved within the semantic model. Thus, proving serializability (or opacity) amounts simply to mapping the algorithm on to our rules, and showing that it satisfies the rules’ side-conditions.

Mon 15 Jun

pldi2015-papers
16:00 - 17:40: Research Papers - Concurrency I at PLDI Main BLUE (Portland 254-255)
Chair(s): Santosh NagarakatteRutgers University
pldi2015-papers16:00 - 16:25
Talk
Pantazis DeligiannisImperial College London, Alastair DonaldsonImperial College London, Jeroen Ketema, Akash LalMicrosoft Research India, Paul ThomsonImperial College London
Media Attached
pldi2015-papers16:25 - 16:50
Talk
Jeff HuangTexas A&M University
Media Attached
pldi2015-papers16:50 - 17:15
Talk
Malavika SamakIndian Institute of Science, Bangalore, Murali Krishna RamanathanIndian Institute of Science, Bangalore, Suresh JagannathanPurdue University
Media Attached
pldi2015-papers17:15 - 17:40
Talk
Eric KoskinenIBM TJ Watson Research Center, Matthew ParkinsonMicrosoft Research, UK
Media Attached