Improve memory model

[lars-t-hansen]

The memory model text is currently fairly weak. There's an email discussion ongoing regarding tighter prose for that section, this bug is a placeholder for that work item.

Also see other bugs labeled "Memory model".

[lars-t-hansen]

I have incorporated much of the discussion, though there's still the lingering concern about what the "poisoning" means, really, and that's left open with a note in the current spec document. I will leave this bug open for now.

[lars-t-hansen]

Something like the following would probably be an improvement:

Suppose two threads T1 and T2 race by accessing sets of locations L1 and L2 where the intersection of L1 and L2 is necessarily nonempty. Let L=union(L1,L2) be a set of racy locations and T_L={T1,T2} be the set of threads that raced on L. If another thread T3 accesses some locations L3 that overlaps L then L3 is unioned into L to enlarge L and T3 is unioned into T_L to enlarge T_L.

In the algorithm for GetValueFromBuffer, let step 6, rather than reading from memory, instead pick an appropriate number of arbitrary byte values if any of the locations accessed by the operation intersect any set L of racy locations (and this access may enlarge L and its corresponding T_L, as outlined above). Note NaN canonicalization will still apply as that happens after reading the bytes; all racy reads are type-safe but return otherwise random data.

A set of racy locations L is deleted only when all the threads in T_L have had their last racy interaction with the elements of L and have synchronized properly on some locations S not in any set of racy locations, creating the necessary dividing line after the racy accesses that they can all agree on. Once L has been deleted accesses on locations in L become predictable again.

(The intent here is to allow a poisoned location to provide any value and to allow poisoned locations to settle on some reliable value following proper synchronization so that they become usable again. What this does not account for is certain effects resulting from optimization, such as a value changing after it has been read from a racy location, as can happen if a value is read twice though there's only one read in the source syntax.)

[jfbastien]

I'm confused by the NaN canonicalization bit: at least in C++ cmpxchg is defined in terms of memcpy and memcmp so there's no special treatment of floating-point. It's defined this way to fit with how hardware works, so I don't think SAB should deviate.

[lars-t-hansen]

This is for regular loads and stores (we don't have floating point atomics). The existing language requires that when a float is read out of a TypedArray anything that looks like a NaN is read as the canonical NaN, this matters since NaNs can be forged in memory thru eg Uint8Array. The reference to "step 6" above is crucial, that's the step that obtains bytes from memory, after which they are subject to further processing. (Should have included the link: http://www.ecma-international.org/ecma-262/6.0/#sec-getvaluefrombuffer.)

[jfbastien]

Ah OK: to do an atomic FP load/store you need to treat it as i32 or i64 and then cast back? FWIW C++ has atomic FP load / store defined that way. We're working on adding other operations too.

[lars-t-hansen]

At the moment one can use int32 atomics for float32, but as we don't have int64 there's nothing for float64. I had a draft of float atomics but there was significant pushback on it and I just left it out.

[lars-t-hansen]

In addition to the prose I outlined above there should probably be wording to the effect that the cell value that the system settles on when the race is over need not be related to any of the values observed by any worker during the race.

Also, the locations in L must be address-free.

(The notion of a poisoned read would replace the notion of a poisoned write - any writes that participate in the race cause the race and thus the poisoning to happen, but having a poisoned arbitrary-values read operation allows the value to change unpredictably, which a poisoned write would not. It still does not account for the introduced-read transformation.)

[lars-t-hansen]

Issue #51 tracks the introduced-read transformation.

[lars-t-hansen]

The memory model has been broadly rewritten (draft forthcoming today), so let's critique that by opening new bugs if necessary.