Mon 24 Jun 2019 08:45 - 09:05 at 229AB - Concurrency I Chair(s): Alastair 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.

Mon 24 Jun

pldi-2019-papers
08:45 - 09:45: PLDI Research Papers - Concurrency I at 229AB
Chair(s): Alastair DonaldsonGoogle and Imperial College London
pldi-2019-papers08:45 - 09:05
Talk
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
pldi-2019-papers09:05 - 09:25
Talk
Lun LiuUniversity of California at Los Angeles, USA, Todd MillsteinUniversity of California, Los Angeles, Madan MusuvathiMicrosoft Research
DOI Pre-print Media Attached
pldi-2019-papers09:25 - 09:45
Talk
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