A Promising Semantics for Relaxed-Memory Concurrency
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.
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.