University of Peloponnese
In order to explore programs on relaxed memory model, the authors need to specify the memory models in a way which is compatible with state exploration tools. Memory model specifications typically fall into two categories: axiomatic and operational. Memory models are often specified axiomatically, as a set of constraints on the order in which memory operations are observed by the various concurrent processes in the system. Axiomatic specifications are usually easier to write, and naturally decompose into a collection of simple axioms. However, these axioms describe global constraints on the complete execution trace, and therefore they are not well-suited for step-by-step execution where the complete execution trace is not known in advance.