Skip to main content

A Promising Semantics for Relaxed-Memory Concurrency

Chung-Kil Hur ( Seoul National University )
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: