Constructing a Weak Memory Model

TL;DR

This paper introduces the General Atomic Memory Model (GAM), a constructive approach to defining a weak memory model that preserves uniprocessor optimizations and provides insights into the inherent nature of weak memory behaviors.

Contribution

It presents a novel constructive method to develop a weak memory model, offering a clear foundation and operational semantics, unlike previous empirical models.

Findings

GAM allows all four load/store reorderings.

GAM's performance is comparable to existing models.

The model provides new insights into weak memory behaviors.

Abstract

Weak memory models are a consequence of the desire on part of architects to preserve all the uniprocessor optimizations while building a shared memory multiprocessor. The efforts to formalize weak memory models of ARM and POWER over the last decades are mostly empirical -- they try to capture empirically observed behaviors -- and end up providing no insight into the inherent nature of weak memory models. This paper takes a constructive approach to find a common base for weak memory models: we explore what a weak memory would look like if we constructed it with the explicit goal of preserving all the uniprocessor optimizations. We will disallow some optimizations which break a programmer's intuition in highly unexpected ways. The constructed model, which we call General Atomic Memory Model (GAM), allows all four load/store reorderings. We give the construction procedure of GAM, and provide insights which are used to define its operational and axiomatic semantics. Though no attempt is made to match GAM to any existing weak memory model, we show by simulation that GAM has comparable performance with other models. No deep knowledge of memory models is needed to read this paper.