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.

Mon 24 Jun

Displayed time zone: Tijuana, Baja California change

08:45 - 09:45
Concurrency IPLDI Research Papers at 229AB
Chair(s): Alastair F. Donaldson Google and Imperial College London
Promising-ARM/RISC-V: A Simpler and Faster Operational Concurrency Model
PLDI Research Papers
Christopher Pulte University of Cambridge, Jean Pichon-Pharabod University of Cambridge, Jeehoon Kang KAIST, Sung-Hwan Lee Seoul National University, South Korea, Chung-Kil Hur Seoul National University
Media Attached
Accelerating Sequential Consistency for Java with Speculative Compilation
PLDI Research Papers
Lun Liu University of California at Los Angeles, USA, Todd Millstein University of California, Los Angeles, Madan Musuvathi Microsoft Research
DOI Pre-print Media Attached
Renaissance: Benchmarking Suite for Parallel Applications on the JVM
PLDI Research Papers
Aleksandar Prokopec Oracle Labs, Andrea Rosà University of Lugano, Switzerland, David Leopoldseder Johannes Kepler University Linz, Gilles Duboscq Oracle Labs, Petr Tuma Charles University, Martin Studener JKU Linz, Austria, Lubomír Bulej Charles University, Yudi Zheng Oracle Labs, Alex Villazón Universidad Privada Boliviana, Bolivia, Doug Simon Oracle Labs, Thomas Wuerthinger Oracle Labs, Walter Binder University of Lugano, Switzerland