>> Likewise, it does prevent the reordering if the loads in T2 against the TIME() load, so if x *was* updated, then the assertion holds.

I don't believe this is true because the loads and stores in your example are unordered wrt eachother, it's entirely legal to flip the order of them to get:

```
T1:
  temp = TIME()
  <load-store barrier>
  y.store(1, relaxed)
  x.store(temp, relaxed)

T2:
  w = x.load(relaxed)
  z = y.load(relaxed)
  <load-load barrier>
  temp = TIME()
  if (z) assert(w <= temp)
```

Which allows reading z == 1, w == INT64_MAX.

On 11 June 2026 18:01:40 BST, Thiago Macieira via Std-Discussion <std-discussion_at_[hidden]> wrote:
>On Thursday, 11 June 2026 00:44:31 Pacific Daylight Time Jennifier Burnett via
>Std-Discussion wrote:
>> ```
>> T1:
>> x = TIME()
>> y.store(x, relaxed)
>>
>> T2:
>> z = y.load(relaxed)
>> w = TIME()
>> ```
>> To my understanding the question as you understand it is whether when z ==
>> x, w must >= x, correct?
>
>Thank you for making this a more concrete example, but I don't think it went
>far enough: you didn't model x as an atomic, so it's hard to say how one can
>perform the w >= x check in the first place.
>
>Let's say though:
>x = INT64_MAX
>y = 0
>T1:
> x.store(TIME(), relaxed)
> y.store(1, relaxed)
>
>T2:
> z = y.load(relaxed)
> w = x.load(relaxed)
> if (z) assert(w <= TIME())
>
>If we didn't know what TIME() was (let's say it was a constant), this is the
>prototypical example of how loads and stores can bypass each other: it's
>entirely possible for y.store() to have become visible, but not x.store(),
>resulting in T2 seeing x's old value of INT64_MAX and failing the assertion.
>
>Nothing changes even if we model TIME() as a load(relaxed) of a global that
>monotonically increases at a frequency of 1 GHz. There would be no happens-
>before between the two pairs of variables, so in T1 it would be entirely
>allowable for the y.store(1) to finish and becoming readable before obtaining
>the time in the first place. Likewise in T2, the x.load() could happen earlier
>than the y.load(), so it might see the old value of x (INT64_MAX) even if y
>was seen as 1.
>
>What if TIME() has an acquire fence? In this case, the machine cannot reorder
>a younger store ahead of it. This ensures that neither store in T1 can become
>observable before the TIME() read. Likewise, it does prevent the reordering if
>the loads in T2 against the TIME() load, so if x *was* updated, then the
>assertion holds.
>
>But it doesn't help with the relative ordering of x and y between themselves.
>So this works:
> assert(w == INT64_MAX || w <= TIME());
>
>but not as written above, because nothing prevents observing y.load() from
>observing 1 while x.load() still observes the old value.
>