Event structures and weak memory models

[This is joint work with Jade Alglave and Jean-Marie Madiot.]

In this talk I will present a model of shared-memory concurrent
programs using event structures, which represents faithfully both the
nondeterministic branching behaviour of the program, and the causality
between memory actions. As a result, the model combines the
theoretical advantages of operational semantics (using LTSs) and
axiomatic semantics (using sets of execution). I will illustrate the
methodology on the case of sequential consistency before presenting
two applications of the methodology:

- A model for TSO where reordering are represented as concurrency. Our
  model allows to show a strong DRF guarantee: that the behaviour of a
  race-free program is weakly bisimilar on TSO and SC.  This stronger
  version implies that a program satisfies the same formulas from
  Hennessy-Milner logic on SC and TSO.

- A model where actions on the same variable need not to be
  sequentialised (as is the case in usual axiomatic semantics). This
  alternate model has the same traces as the usual model but exhibits
  fewer executions in the sense of axiomatic semantics. We have
  implemented this alternate model in Herd and have observed both a
  performance speedup and a decrease in the number of executions
  generated for programs with concurrent writes to the same variables.

Time allowing, I will then talk briefly of the research programme this
work is part of, which aims at using event structures for giving
operational models of programming languages which are causal and
compositional.