University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > A promising semantics for relaxed-memory concurrency

A promising semantics for relaxed-memory concurrency

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity