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

[Amal Ahmed]

Reminder: This seminar is today, starts in 10 mins.

-Amal

> Begin forwarded message:
> 
> From: Aviral Goel <goel.av at husky.neu.edu>
> Subject: [Pl-seminar] 15th February: Chung-Kil Hur: Promising-ARM/RISC-V: a simpler and faster operational concurrency model
> Date: February 5, 2019 at 1:06:46 PM EST
> To: pl-seminar at ccs.neu.edu
> 
> Date: Friday, 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
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar

-------------- next part --------------
HTML attachment scrubbed and removed