We present a new methodology to model relaxed memory, interpreting a program on a given architecture by an event structure, expressing the causality between instructions, according to the optimisations performed by the hardware. The methodology uses standard tools of event structure theory, in particular product of event structures and the correspondence between event-based and execution-based representations.

In the talk, we will demonstrate the methodology on a simple weak memory specification: TSO (corresponding to Intel x86 processors). We will then present two applications of this model: one theoretical, showing a strong DRF guarantee, and another, more practical, showing how the model allows tinkering to generate smaller program representation than the state of the art.