Relaxed memory models must simultaneously achieve efficient implementability
and thread-compositional reasoning. Is that why they have become so
complicated? We argue that the answer is no: It is possible to achieve these
goals by combining an idea from the 60s (preconditions) with an idea from the
80s (pomsets), at least for X64 and ARMv8. We show that the resulting model
(1) supports compositional reasoning for temporal safety properties, (2)
supports all expected sequential compiler optimizations, (3) satisfies the
DRF-SC criterion, and (4) compiles to X64 and ARMv8 microprocessors without
requiring extra fences on relaxed accesses.