You take hardware properties as axioms (for instance, ARMv6 cache coherency is specified in detail as part of the lengthy spec, even though you have no guarantees that the hardware actually is faithful to the spec)