ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In
particular, the model was originally non-multicopy-atomic: writes could
become visible to some other threads before becoming visible to all —
but this has not been exploited in production implementations, the
corresponding potential hardware optimisations are thought to have
insufficient benefits in the ARM context, and it gives rise to subtle
complications when combined with other ARMv8 features. The ARMv8
architecture has therefore been revised: it now has a multicopy-atomic
model. It has also been simplified in other respects, including more
straightforward notions of dependency, and the architecture now includes
a formal concurrency model.

This is work presented in POPL this year. I will also present some of
the background and context on relaxed memory which is absent from the
necessarily compressed talk format of POPL.