Mon 24 Jun 2019 08:45 - 09:05 at 229AB - Concurrency I Chair(s): Alastair F. Donaldson

For ARMv8 and RISC-V, there are concurrency models in two styles,
extensionally equivalent: axiomatic models, expressing the concurrency
semantics in terms of global properties of complete executions; and
operational models, that compute incrementally. The latter are in an
abstract microarchitectural style: they execute each instruction in
multiple steps, out-of-order and with explicit branch speculation.
This similarity to hardware implementations has been important in
developing the models and in establishing confidence, but involves
complexity that, for programming and model-checking, one would prefer
to avoid.

We present new more abstract operational models for ARMv8 and RISC-V,
and an exploration tool based on them. The models compute the allowed
concurrency behaviours incrementally based on thread-local conditions
and are significantly simpler than the existing operational models:
executing instructions in a single step and (with the exception of
early writes) in program order, and without branch speculation. We
prove the models equivalent to the existing ARMv8 and RISC-V axiomatic
models in Coq. The exploration tool is the first such tool for ARMv8
and RISC-V fast enough for exhaustively checking the concurrency
behaviour of a number of interesting examples. We demonstrate using
the tool for checking several standard concurrent datastructure and
lock implementations, and for interactively stepping through
model-allowed executions for debugging.

Conference Day
Mon 24 Jun

Displayed time zone: Tijuana, Baja California change

08:45 - 09:45
Concurrency IPLDI Research Papers at 229AB
Chair(s): Alastair F. DonaldsonGoogle and Imperial College London
Promising-ARM/RISC-V: A Simpler and Faster Operational Concurrency Model
PLDI Research Papers
Christopher PulteUniversity of Cambridge, Jean Pichon-PharabodUniversity of Cambridge, Jeehoon KangKAIST, Sung-Hwan LeeSeoul National University, South Korea, Chung-Kil HurSeoul National University
Media Attached
Accelerating Sequential Consistency for Java with Speculative Compilation
PLDI Research Papers
Lun LiuUniversity of California at Los Angeles, USA, Todd MillsteinUniversity of California, Los Angeles, Madan MusuvathiMicrosoft Research
DOI Pre-print Media Attached
Renaissance: Benchmarking Suite for Parallel Applications on the JVM
PLDI Research Papers
Aleksandar ProkopecOracle Labs, Andrea RosàUniversity of Lugano, Switzerland, David LeopoldsederJohannes Kepler University Linz, Gilles DuboscqOracle Labs, Petr TumaCharles University, Martin StudenerJKU Linz, Austria, Lubomír BulejCharles University, Yudi ZhengOracle Labs, Alex VillazónUniversidad Privada Boliviana, Bolivia, Doug SimonOracle Labs, Thomas WuerthingerOracle Labs, Walter BinderUniversity of Lugano, Switzerland