A multitude of weak memory models exists supporting various types of relaxations and different synchronization primitives. On one hand, they must be lax enough to allow for hardware and compiler optimizations; on the other, the more lax the model, the harder it is to reason about programs. Though the right balance is up for debate, a memory model should provide what is known as the SC-DRF guarantee, meaning that data-race free programs behave in a sequentially consistent manner.
In this work we present a weak memory model for a calculus inspired by Go. Thus, different from previous approaches, we focus on a memory model with buffered channel communication as the sole synchronization primitive. While memory models are often defined axiomatically where the notion of a program is abstracted away (often as a graph with memory events as nodes), we formalize our model via an operational semantics. This allows us to prove the SC-DRF guarantee using a standard simulation technique that highlights invariants and gives insight into the how the memory works. Finally, we provide a concrete implementation in K, a rewrite-based executable semantic framework, which allows us to derive an interpreter for the proposed language.