We study two operational semantics for relaxed memory models. Our first formalization is based on the notion of write-buffers which is pervasive in the memory models literature. We instantiate the (Total Store Ordering) TSO and (Partial Store Ordering) PSO memory models in this framework. Memory models that support more aggressive relaxations (e.g. read-to-read reordering) are not easily described with write-buffers. Our second framework is based on a general notion of speculative computation. In particular we allow the prediction of function arguments, and execution ahead of time (e.g. by branch prediction). While technically more involved than write-buffers, this model is more expressive and can encode all the Sparc family of memory models: TSO, PSO and (Relaxed Memory Ordering) RMO. We validate the adequacy of our instantiations of TSO and PSO by formally comparing their write-buffer and speculative formalizations. The use of operational semantics techniques is paramount for the tractability of these proofs.
展开▼
