These papers take forever to read (take it from me, I am doing research in this area, in particular proofs of correctness for lock free programs). I recommend focusing on the C/C++ ones if only for the practical value.
As for comparison, the C/C++ memory model is more general and is operational. It is also formalized in coq and has some good theorems (data race free sequential consistency being the most obvious).
The RISC memory model is axiomatic and follows the standard axiomatic approach adopted for many other memory models like Java and the current C/C++ standard. That's not a dig, they just don't care as much about rigor.
Axiomatic models consider the every possible execution and then weed out bad ones, where as the operational semantics defines the set of all possible executions using a transition relation. If you're into math you might see these vaguely as extensional and intensional respectively.
thanks! I think the RISC/WMM folks provide an operational model too, using their own "I2E" formalism. The end of the paper seems to have a proof of equivalence between their axiomatic and operational models.
As for comparison, the C/C++ memory model is more general and is operational. It is also formalized in coq and has some good theorems (data race free sequential consistency being the most obvious).
The RISC memory model is axiomatic and follows the standard axiomatic approach adopted for many other memory models like Java and the current C/C++ standard. That's not a dig, they just don't care as much about rigor.
Axiomatic models consider the every possible execution and then weed out bad ones, where as the operational semantics defines the set of all possible executions using a transition relation. If you're into math you might see these vaguely as extensional and intensional respectively.