Sites Inria

Version française

Gallium Seminar

Gallium Seminar - Event structures and weak memory models

  • Date : 27/11/2018
  • Place : 2 rue Simone Iff 75012 - Salle A115, bât A
  • Guest(s) : Simon Castellan
  • Organiser(s) : Gallium Team

Event structures and weak memory models

Simon Castellan, Imperial College 

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.

Keywords: Gallium seminar Semantic Modele Memory