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

[Aviral Goel]

Hi,

A minor correction. This event is on 15th Februray, Friday. I mistakenly
wrote Thursday instead of Friday.
My sincere apologies for the day mix-up.

Best,
Aviral


On Tue, Feb 5, 2019 at 1:06 PM Aviral Goel <goel.av at husky.neu.edu> wrote:

> *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