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.