School of Computing

May 13
15:00 - 16:00
PLAS: Simon Castelan
PLAS Group Seminar
Reconciling nondeterminism and causality: Event structures for relaxed memory

Hardware optimisations come at the cost of programs behaving in ways so subtle that we need prediction models. Existing prediction models come in two kinds: operational models provide information about the nondeterministic branching points of programs, and axiomatic models provide causal information. We propose a methodology providing both, which interprets programs as event structures .  We give two applications of this methodology. First, we build a model of TSO in terms of event structures, strongly bisimilar to the standard operational model and use it to show a strong DRF theorem: the behaviours of race-free programs on SC and TSO are weakly bisimilar with respect to observable actions, which preserves not only safety but also liveness properties. Second, we give a new causal account of memory which does not enforce a linear order on writes to the same variable. We show this model is correct and work towards implementing it in Herd, a language to specify and simulate axiomatic memory models.This is joint work with Jade Alglave and Jean-Marie Madiot.

Location

SW101,
Cornwallis South West,
University of Kent,
Canterbury,
Kent,
CT2 7NF
United Kingdom
Map

Details

Contact: O.Chitil
E: oc@kent.ac.uk
School of Computing

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 14/08/2015