Title: A weak-memory program logic (at last, maybe)

Joint work with Matthew Parkinson (Microsoft Research) and Jade
Alglave (Microsoft Research and UCL)

Abstract: Weak memory (relaxed memory) is the way all modern computing
gets done, in phones, in laptops, in GPUs. Processors reorder
instruction execution and muddle up propagation of written values
between processors and stores and/or between processors and
processors. In sensible designs weak-memory effects are constrained,
but not every designer is sensible.

After three (or was it four?) years trying to make a logic that worked
for IBM Power processors, and scared by a paper (Crary and Sullivan; A
calculus for relaxed memory; POPL 2015) that seemed to scoop us, we
stumbled on a logic that seems to be machine-independent. It's based
on rely/guarantee or Owicki-Gries, with Hoare logic used to describe
the effects of individual commands, specific inter-command orderings
chosen by the programmer to describe the constraints that are
required, and summaries of threads in terms of their interference with
shared memory.

It is surprising simple, but I would say that, wouldn't I? Those who
were exposed to the Power attempt will, I think, be pleasantly
surprised. There are three kinds of orderings, three associated kinds
of parallelism, four stability rules. You should see enough to make
you understand what weak memory is all about.

It will definitely be a talk for programmers.

There is a proof checker in preparation (and there was one for
Power). There ought to be a proof of correctness being started Real
Soon Now.