A promising semantics for relaxed-memory concurrency

Add to your list(s) Download to your calendar using vCal

• Chung-Kil Hur, Seoul National University
• Friday 08 September 2017, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Dominic Mulligan.

Despite many years of research, it has proven very difficult to develop a model for relaxed-memory concurency that satisfies all the requirements of programmers, compilers, and hardware.

In this talk, I will introduce the first relaxed-memory model, called “promising semantics”, that fulfills (most of) the requirements. It (1) accounts for a broad spectrum of features from the C++11 concurrency model, (2) is implementable, in the sense that it provably validates many standard compiler optimizations and reorderings, as well as standard compilation schemes to x86-TSO and Power, (3) justifies simple invariant-based reasoning, thus demonstrating the absence of bad “out-of-thin-air” behaviors, (4) supports “DRF” guarantees, ensuring that programmers who use sufficient synchronization need not understand the full complexities of relaxed-memory semantics, and (5) defines the semantics of racy programs without relying on undefined behaviors, which is a prerequisite for applicability to type-safe languages like Java. To establish confidence in our model, we have formalized most of our key results in Coq.

Also, in this talk, no prior knowledge of relaxed memory concurrency (in particular, existing axiomatic semantics) is assumed. This is particularly because the promising semantics is a standard interleaving operational semantics with just two new notions: “view” and “promise”.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.