Wed 20 Jun 2018 16:10 - 16:35 at Grand Ballroom AB - Transactions and Races Chair(s): Tatiana Shpeisman

Weak memory models provide a complex, system-centric semantics for concurrent programs, while transactional memory (TM) provides a simpler, programmer-centric semantics. Both have been studied in detail, but their \emph{combined} semantics is not well understood. This is problematic because such widely-used architectures and languages as x86, Power, and C++ all support TM, and all have weak memory models.

Our work aims to clarify the interplay between weak memory and TM by extending existing axiomatic weak memory models (x86, Power, ARMv8, and C++) with new rules for TM. Our formal models are backed by automated tooling that enables (1) the synthesis of tests for validating our models against existing implementations and (2) the model-checking of TM-related transformations, such as lock elision and compiling C++ transactions to hardware. A key finding is that a proposed TM extension to ARMv8 currently being considered within ARM Research is incompatible with lock elision without sacrificing portability or performance.

Wed 20 Jun

pldi-2018-papers
16:10 - 17:25: PLDI Research Papers - Transactions and Races at Grand Ballroom AB
Chair(s): Tatiana ShpeismanGoogle Brain
pldi-2018-papers152950380000016:10 - 16:35
Talk
Nathan ChongARM Ltd., Tyler SorensenImperial College London, John WickersonImperial College London
Media Attached
pldi-2018-papers152950530000016:35 - 17:00
Talk
Matthew MilanoCornell University, Andrew MyersCornell University
Media Attached
pldi-2018-papers152950680000017:00 - 17:25
Talk
Stephen DolanUniversity of Cambridge, KC SivaramakrishnanUniversity of Cambridge, Anil MadhavapeddyOCaml Labs
Media Attached