Add a note in the spec about causality cycles/out-of-thin air reads

[RobinMorisset]

This memory model appears to have inherited from C++ the issue of allowing causality cycles (a.k.a. out-of-thin-air reads). For example, the following program (in pseudo-code):

Thread 1:
  r = load_relaxed(x);
  store_relaxed(y, r);
Thread 2:
  r2 = load_relaxed(y);
  store_relaxed(x, r2);

can end with any value in both x and y. This is both unwanted (I don't know of any hardware that can actually write 42 in both x and y, with no reference to 42 anywhere in the program) and rather fundamental to the C++ style of axiomatic models. Fixing this in the model is way out-of-scope (it is a hard problem that academia has been trying to fix for several years, and the only solution I consider satisfactory rewrites the entire model in a different style), but we could include a comment similar to that in the C++ spec (note 9 in section 29.3 of http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4296.pdf):

9 Implementations should ensure that no “out-of-thin-air” values are computed that circularly depend on their own computation.
[ Note: For example, with x and y initially zero,
// Thread 1:
r1 = y.load(memory_order_relaxed);
x.store(r1, memory_order_relaxed);
// Thread 2:
r2 = x.load(memory_order_relaxed);
y.store(r2, memory_order_relaxed);
should not produce r1 == r2 == 42, since the store of 42 to y is only possible if the store to x stores 42, which circularly depends on the store to y storing 42. Note that without this restriction, such an execution ispossible. —endnote]

[jeffbolznv]

I think the Alloy model doesn't allow out of thin air reads because of these rules on reads-from/RFINIT/R:

  // reads-from maps writes to reads (that don't read-from init)
  // at the same location.
  rf in (W->(R-RFINIT)) & (sloc-iden)

  // reads-from is one-to-one
  rf . ~rf in iden

  // reads may read from the initial value
  RFINIT in R

  // All reads must read from some write or from init (the size of rf and
  // RFINIT must equal the size of R)
  #(rf + (stor[RFINIT])) = #R

Maybe what is missing is just to take some of this "reads-from" stuff and add it into the text spec. It doesn't really say anything about it right now.

[RobinMorisset]

I don't see at all how these rules prevent the example I listed. Out-of-thin-air reads are justified by some write. It is just that this write is justified by the read in turn.

And it is really a rather fundamental issue with any language-level axiomatic memory-model that accepts the LB (load buffering) pattern. We want to allow the following (because it actually occurs on some hardware, I am not sure about GPUs but at least ARM and Power processors and GPUs seem to offer even weaker guarantees):

Thread 1:
  r = load_relaxed(x);
  store_relaxed(y, 42);
Thread 2:
  r2 = load_relaxed(y);
  store_relaxed(x, 42);
r == r2 == 42 at the end

And forbid the following (because it is rather non-sensical, not allowed by any hardware I know of, and makes formal reasoning about programs extremely hard):

Thread 1:
  r = load_relaxed(x);
  store_relaxed(y, r);
Thread 2:
  r2 = load_relaxed(y);
  store_relaxed(x, r2);
r == r2 == 42 at the end

But they have exactly the same events and relations between these event. This is why I am suggesting a mere note in the spec and no change to the alloy model: it is litterally impossible to fix formally with this kind of model.

[jeffbolznv]

Ah, I see. I'm fine with adding a note if that's the best we can do.