School of Computing

Oct 19
15:00 - 16:00
PLAS: James Riely (DePaul University, USA)
PLAS Group Seminar
Pomsets with Preconditions: A Simple Model of Relaxed Memory

Relaxed memory models must simultaneously achieve efficient implementability and thread-compositional reasoning.  Is that why they have become so complicated?  We argue that the answer is no: It is possible to achieve these goals by combining an idea from the 60s (preconditions) with an idea from the80s (pomsets), at least for X64 and ARMv8.  We show that the resulting model (1) supports compositional reasoning for temporal safety properties, (2) supports all expected sequential compiler optimizations, (3) satisfies theDRF-SC criterion, and (4) compiles to X64 and ARMv8 microprocessors without requiring extra fences on relaxed accesses.


United Kingdom


Contact: O.Chitil
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