Mark Batty

Date: 17:00, Thursday, October 3, 2013
Speaker: Mark Batty
Venue: IST Austria

When constructing complex concurrent systems, abstraction is vital:
programmers should be able to reason about programming languages in
terms of an abstract specification, augmented by libraries with
complimentary specifications. Relaxed memory systems complicate these
aims: they do not provide sequential consistency, testing our ability
to specify the languages themselves, and revealing nuances in the
behaviour of libraries that current specification techniques do not
capture. This talk will cover two related problems:

The C/C++11 memory model specifies the behaviour of a relaxed-memory
programming language, but fails in one important regard: a restriction
that prevents reading arbitrary values from memory is broken. Part of
this talk will describe the problem, and discuss its implications on
memory model design.

In order to avoid unnecessary synchronisation, library implementations
may intentionally allow clients to observe relaxed memory effects, and
library specifications must capture these. I will describe a criterion
for sound library abstraction in the C/C++11 memory model that
generalises the standard sequentially consistent notion of
linearizability, capturing all client-library interactions, both
through call and return values, and through the subtle synchronisation
effects arising from the memory model.

Posted in RiSE Seminar