A Promising Semantics for Relaxed-Memory Concurrency
Chung-Kil Hur ( Seoul National University )
- 14:00 6th October 2017 ( week 0, Michaelmas Term 2017 )
The "promising semantics" is an operational semantics for
relaxed-memory concurrency that can account for concurrency features
of major programming languages such as C/C++ and Java. The semantics
is promising since (1) it adequately balances the conflicting
desiderata of programmers, compilers, and hardware, which has been a
long standing open problem; (2) it is (arguably) simple and easy to
understand because it is a standard interleaving operational semantics
with just two new notions: "view" and "promise"; and (3) most results
are fully formalized in Coq.
In this talk, I will introduce (1) the basics of relaxed memory concurrency, (2) the challenges with defining its model, and (3) the promising semantics showing how it solves the challenges. I assume no prior knowledge of relaxed memory concurrency
This is published at POPL'17 and joint work with Jeehoon Kang from Seoul National University, and Ori Lahav, Viktor Vafeiadis and Derek Dreyer from MPI-SWS.
Speaker 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 research interests are in C/C++/LLVM semantics, relaxed memory concurrency, software (esp. compiler) verification, interactive theorem proving, category theory, probabilistic programming and Bayesian inference.Share this:
