Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle A115, bâtiment A Mardi 27 novembre, 14h00 --------------- Simon Castellan --------------- Imperial College ======================================= Event structures and weak memory models ======================================= 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. [This is joint work with Jade Alglave and Jean-Marie Madiot.]