[Pl-seminar] 15th February: Chung-Kil Hur: Promising-ARM/RISC-V: a simpler and faster operational concurrency model

[Aviral Goel]

*Date:* Thursday, February 15th 2019
*Location:* Ryder 431 <https://goo.gl/maps/qcu64TNsemP2>
*Time:* 10:00 AM to 11:30 AM
*Faculty Host:* Amal Ahmed


*Promising-ARM/RISC-V: a simpler and faster operational concurrency model
<http://prl.ccs.neu.edu/seminars.html#hur-promising-arm-risc-v-a-simpler-and-faster-operational-concurrency-model>*

*Chung-Kil Hur*


*Abstract*

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 micro-architectural 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. In this talk, I
will 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 such as
Michael-Scott queue and Chase-Lev deque, compiled from C++ and Rust with
GCC or Clang -O3, and for interactively stepping through model-allowed
executions for debugging.

*Bio*

Chung-Kil Hur is an associate professor in Department of Computer Science
and Engineering at Seoul National University. Previously he worked as a
postdoctoral researcher at Microsoft Research Cambridge,Max Planck
Institute for Software Systems (MPI-SWS) and Laboratoire PPS. He obtained a
Ph.D. from University of Cambridge and a B.Sc. in both Computer Science and
Mathematics from Korea Advanced Institute of Science and Technology
(KAIST). His current research interests are in semantics of low-level
languages such as C,Rust,LLVM IR, relaxed memory concurrency, formal
verification of software such as compiler and OS, and interactive theorem
provers such as Coq.

Best,
Aviral
-------------- next part --------------
HTML attachment scrubbed and removed