Personal tools
You are here: Home Events LFCS seminar: Chung-Kil Hur: A promising semantics for relaxed-memory concurrency

LFCS seminar: Chung-Kil Hur: A promising semantics for relaxed-memory concurrency

— filed under: ,

What
  • LFCS Seminar
  • Upcoming events
When Dec 05, 2017
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal
iCal
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.
 
Document Actions