Dr Chung-Kil Hur of the Seoul National University came to visit the group and to talk about a promising semantics for relaxed-memory concurrency, 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.

The talk abstract:

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.