Date: Fri, 12 Jun 2026 09:28:48 +0100
> I'm not convinced we need an acq_rel barrier. It may be that we do and the Standard should call out that now() calls should effectively have such a barrier, if not literally have one such. But I think we only need an acquire barrier, if we assume the clock ticking is a release barrier.
So you're misunderstanding something about the formal memory model, which is fine, it's a confusing subject. Basically the important part to understand here is that if you have a release and an acquire that reads the value written by the release (and for barriers it's maybe helpful to think that they "upgrade" all previous/subsequent relaxed reads/writes to be acquire/release) then all that means in the formal memory model is that all writes that precede the release must be visible to reads after the acquire. There's no further requirements about reordering, so if a variable that gets read after the acquire is never written to before the release, it's perfectly fine to move it before the acquire because there's no way the acquire could change the value it reads.
Since the clock ticking thread never writes to _any_ variable other than the time variable, that means that putting a release on the clock thread effectively does nothing, because _all_ variables after the acquires know that the corresponding acquire can't change the value that they read, and thus can be moved before the acquire, effectively making it relaxed.
The reason for making it acq_rel is to upgrade any subsequent writes to be releases, and any prior reads to be acquires, so that any attempt to directly compare time values between threads effectively becomes communicated via acquire-release, which would ensure that the two calls to now() happen-before eachother.
Of course last night I realised that even that doesn't work because it's trivial to launder the communication through a third thread which removes the acquire-release semantics, so this is all moot, you'd need to invent new formal semantics for the desired behaviour regardless:
```
T1:
x = TIME()
y.store(x,relaxed)
T2:
temp = y.load(relaxed) //reads x
w.store(temp, relaxed)
T3:
z = w.load(relaxed) //reads x
assert(z <= TIME())
```
On 11 June 2026 22:08:46 BST, Thiago Macieira <thiago_at_[hidden]> wrote:
>On Thursday, 11 June 2026 14:03:20 Pacific Daylight Time Jennifier Burnett
>wrote:
>> > I meant that if you can tell that x was stored to, then it must have been
>> > stored a value lesser than or equal to TIME().
>>
>> I think it's maybe just poorly formulated then - you need to both detect the
>> value written flag and then ensure that if the flag is set you read the
>> correct value from the dependent field, which you need to use
>> acquire-release for.
>
>Agreed it's poorly-formulated, but that's an effect of the OP's proposal being
>such poorly-formulated. In my exercise, we detect that it's been written by
>checking the value read against a sentinel.
>
>> Since this is a thought experiment you can just
>> declare that certain reads observe a particular value, so
>>
>> ```
>> T1:
>> x = TIME()
>> y.store(x,relaxed)
>> T2:
>> z = y.load(relaxed) //reads x
>> assert(z <= TIME())
>> ```
>>
>> should work fine at demonstrating the problem. The issue is that you need to
>> formulate a way of letting TIME establish a happens-before relationship
>> with the other call through the two relaxed operations, which are only
>> related by the coherence-ordered-before relation. Having an acquire barrier
>> before reading the time point and a release barrier after would do the
>> trick, and declaring that TIME acts as an acq_rel fence would also work as
>> a shortcut. Both of those work by upgrading the surrounding relaxed
>> operations to be tantamount to acq_rel, though, which you may or may not
>> think is a reasonable cost.
>
>I'm not convinced we need an acq_rel barrier. It may be that we do and the
>Standard should call out that now() calls should effectively have such a
>barrier, if not literally have one such. But I think we only need an acquire
>barrier, if we assume the clock ticking is a release barrier.
>
So you're misunderstanding something about the formal memory model, which is fine, it's a confusing subject. Basically the important part to understand here is that if you have a release and an acquire that reads the value written by the release (and for barriers it's maybe helpful to think that they "upgrade" all previous/subsequent relaxed reads/writes to be acquire/release) then all that means in the formal memory model is that all writes that precede the release must be visible to reads after the acquire. There's no further requirements about reordering, so if a variable that gets read after the acquire is never written to before the release, it's perfectly fine to move it before the acquire because there's no way the acquire could change the value it reads.
Since the clock ticking thread never writes to _any_ variable other than the time variable, that means that putting a release on the clock thread effectively does nothing, because _all_ variables after the acquires know that the corresponding acquire can't change the value that they read, and thus can be moved before the acquire, effectively making it relaxed.
The reason for making it acq_rel is to upgrade any subsequent writes to be releases, and any prior reads to be acquires, so that any attempt to directly compare time values between threads effectively becomes communicated via acquire-release, which would ensure that the two calls to now() happen-before eachother.
Of course last night I realised that even that doesn't work because it's trivial to launder the communication through a third thread which removes the acquire-release semantics, so this is all moot, you'd need to invent new formal semantics for the desired behaviour regardless:
```
T1:
x = TIME()
y.store(x,relaxed)
T2:
temp = y.load(relaxed) //reads x
w.store(temp, relaxed)
T3:
z = w.load(relaxed) //reads x
assert(z <= TIME())
```
On 11 June 2026 22:08:46 BST, Thiago Macieira <thiago_at_[hidden]> wrote:
>On Thursday, 11 June 2026 14:03:20 Pacific Daylight Time Jennifier Burnett
>wrote:
>> > I meant that if you can tell that x was stored to, then it must have been
>> > stored a value lesser than or equal to TIME().
>>
>> I think it's maybe just poorly formulated then - you need to both detect the
>> value written flag and then ensure that if the flag is set you read the
>> correct value from the dependent field, which you need to use
>> acquire-release for.
>
>Agreed it's poorly-formulated, but that's an effect of the OP's proposal being
>such poorly-formulated. In my exercise, we detect that it's been written by
>checking the value read against a sentinel.
>
>> Since this is a thought experiment you can just
>> declare that certain reads observe a particular value, so
>>
>> ```
>> T1:
>> x = TIME()
>> y.store(x,relaxed)
>> T2:
>> z = y.load(relaxed) //reads x
>> assert(z <= TIME())
>> ```
>>
>> should work fine at demonstrating the problem. The issue is that you need to
>> formulate a way of letting TIME establish a happens-before relationship
>> with the other call through the two relaxed operations, which are only
>> related by the coherence-ordered-before relation. Having an acquire barrier
>> before reading the time point and a release barrier after would do the
>> trick, and declaring that TIME acts as an acq_rel fence would also work as
>> a shortcut. Both of those work by upgrading the surrounding relaxed
>> operations to be tantamount to acq_rel, though, which you may or may not
>> think is a reasonable cost.
>
>I'm not convinced we need an acq_rel barrier. It may be that we do and the
>Standard should call out that now() calls should effectively have such a
>barrier, if not literally have one such. But I think we only need an acquire
>barrier, if we assume the clock ticking is a release barrier.
>
Received on 2026-06-12 08:28:57
