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.
Cornwallis South West,
University of Kent,