A multitude of weak memory models exists supporting various types of relaxations and different synchronization primitives. On one hand, such models must be lax enough to account for hardware and compiler optimizations; on the other, the more lax the model, the harder it is to understand and program for. 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.
We present a weak memory model for a calculus inspired by the Go programming language. Thus, different from previous approaches, we focus on a memory model with buffered channel communication as the sole synchronization primitive. We formalize our model via an operational semantics, which allows us to prove the SC-DRF guarantee using a standard simulation technique. Contrasting against an axiomatic semantics, where the notion of a program is abstracted away as a graph with memory events as nodes, we believe our semantics and simulation proof can be clearer and easier to understand. Finally, we provide a concrete implementation in K, a rewrite-based executable semantic framework, and derive an interpreter for the proposed language.