a relaxed memory model formalized in Alloy (4/5: Basic model rules) // =Basic model rules= // Ordering annotation groups fun Acquire : MemoryEvent { (r.~^gmo & Store