Normative: fix axiomatic model to be SC-DRF, and allow ARMv8 compilation

[conrad-watt]

(PR submitted following co-ordination with @syg)

Background

In the November TC39 meeting, consensus was reached to strengthen the axiomatic model to provide Sequential Consistency of Data-Race-Free Programs (SC-DRF). This property was always intended to be provided by the model (but see #1354 for a counter-example).

A PR to amend the model was drafted (#1362), but I asked for a delay in landing it after @stedolan noticed that the JS model (independent of our fix) appeared to be too strong to allow compilation of SC atomics to ARMv8 lda/stl instructions. We've confirmed that this compilation scheme is used "in the wild" in Chrome (introducing commit), and the violation can be observed experimentally in multi-threaded WebAssembly programs running end-to-end in Chrome on ARMv8 machines. Other engines are also discussing/in the process of implementing this compilation scheme.

In the January TC39 meeting, consensus was reached to amend the axiomatic model to support compilation from JS SC atomics to ARMv8 lda/stl instructions. To be clear, this makes the model weaker than before, since it previously provided a guarantee on interleaving (racy) non-atomics with SC atomics that ARMv8 does not (see slides for a counter-example).

This PR

This PR incorporates both fixes as normative changes, based on previously proposed wording by @syg for the SC-DRF fix (#1362). The fixes are split imprecisely between two commits so the change that weakens the model for the ARMv8 fix can be seen in isolation. That being said, both commits should be taken as a package.

Note that the SC-DRF fix has changed slightly from the precise formulation of the original PR, but the "weak fix" philosophy remains the same. In fact, the new version is a slightly weaker strengthening (I shouldn't have called the previous version "weakest"), and makes one of the SC-DRF conditions more closely mirror an analogous condition in the C++ model.

In support of our changes, we have some proof work/verification that I'd be happy to talk about in more detail over email, including a Coq proof done by @anlun. These proofs don't handle every feature of the memory model (really every proof in this field has a caveat attached), but we've verified at least that the previous model was incorrect, and the revised model isn't incorrect in the same way.

We also observed that one of the SC-DRF additions makes a clause about synchronizing init events redundant, and therefore include a separate editorial change to remove it. init events were originally included in synchronizes-with so that the following shape is not permitted, where R_sc reads-from W_init and W_sc and R_sc have equal ranges

• W_init memory-order W_sc
• W_sc memory-order R_sc

However, it is guaranteed that W_init happens-before W_sc and W_init happens-before R_sc, and our SC-DRF fix disallows exactly this shape anyway. The third bullet disallows the following shape (for all consistencies of W), where R_sc reads-from W and W_sc and R_sc have equal ranges

• W happens-before W_sc
• W happens-before R_sc
• W_sc memory-order R_sc

[ljharb]

@conrad-watt does/can this have test262 tests?

[conrad-watt]

I can write tests which embody the difference between the memory models, but they would work very differently from (my understanding of) a traditional test262 test.

Under perfect conditions, using WebAssembly to "force" efficient code generation, I've been able to make a test which shows the ARMv8 behaviour roughly 1 in 100,000 times. There was some previous discussion here about adding tests like this to a test262 addendum, but it's not gone anywhere so far. The model as a whole is not being validated currently.

Another factor might be that, the majority of the time, if an implementation is doing something the model doesn't allow, it's the model that should change, not the implementation. That's the case with all of these changes.

[syg]

Yeah, I'm still pretty stumped on how to check in litmus tests. Litmus tests are qualitatively different from unit tests -- we can certainly put them into test262 for now, but running them along with the other ones doesn't really make sense.

[syg]

Thank you for the great long-form explanation @conrad-watt, especially the reasoning for why synchronizes-with can be simplified to not care about "Init".

My only suggestion is a non-normative note that the happens-before subclauses are now what constrains "Init" events would be helpful.

[conrad-watt]

My only suggestion is a non-normative note that the happens-before subclauses are now what constrains "Init" events would be helpful.

done