Memory model goals

[littledan]

The memory model in https://tc39.github.io/ecmascript_sharedmem/shmem.html#AtomicsObject.MemoryModel describes some of the challenges that the memory model faces. I think it would be good to write down somewhere (either in the spec or in an explainer somewhere) what goals the memory model is trying to address. This will help people who are trying to evaluate the model. Some possible goals we've discussed are

• No "quantum death" values
• No "out of thin air" values
• Provable "correctness"

Thanks @jyasskin for the suggestion

[lars-t-hansen]

OK. I agree it would be useful to summarize this, but I also don't think the spec is the right place for it (I'm a little self-conscious that the proposal already has a lot of expository text).

There is an existing document in this repo, DISCUSSION.md, that's intended for things like that. I'll see if it's possible to add something there, or I can create a new file for it if it becomes too large.

[jyasskin]

Specifically, I want to be able to call in external experts (like the http://www.cl.cam.ac.uk/~pes20/weakmemory/ group) to review the model and check that it implements your intent. To do that, they'll need to understand your intent. A file outside of the spec is totally fine for that.

[lars-t-hansen]

@jyasskin, noted. Also see Issue #88, in which @jfbastien is going for something similar.

It looks like "intent" won't be too voluminous, so it'll show up in DISCUSSION.md probably tomorrow, I'll make a note here when it does.

[lars-t-hansen]

I landed an expanded discussion (sections "Data Races" and "A summary of constraints on the memory model") that speaks to intent, though I expect it is probably still not enough for serious work. I'm going to leave this ticket open for a while, please do comment when you find that something is mystifying / missing / not to your liking. (Removing the milestone though - what's there is probably OK for stage 3.)

[lars-t-hansen]

Another concern that was brought up is compatibility with WebAssembly, as discussed in Issue #59. I have summarized the discussion in that bug and added it as a subsection to DISCUSSION.md.

[lars-t-hansen]

Scanning the list of closed Stage 3 issues, I find these concerns listed:

• Issue Investigate how/whether races "leak" into the normal semantics #37, do races "leak" into normal semantics
• Issue Data race spec allows an implementation to reveal passwords #71, do races allow eg passwords to be leaked by specifying the exposure of "garbage"
• Issue Memory model imprecision: blanket prohibition on impementation introducing races #48, can the implementation introduce data races

I will address all of those in DISCUSSION.md (to the extent they are not already addressed), but briefly:

• Clearly data races "affect" the semantics of racy programs, but that's not the concern here - this is more about quantum garbage and thin-air values. These effects are addressed in the spec and in DISCUSSION.md.
• Races no longer result in garbage, but in some combination of the bytes that go into the race, so this is addressed.
• The intent of the spec is that DRF programs should not be transformed to introduce observable races, but I'll need to go over the spec text again to see if that's properly restricted.