Re: [RFC] tools/memory-model: Rule out OOTA
From: Jonas Oberhauser
Date: Thu Jan 16 2025 - 14:14:24 EST
Am 1/16/2025 um 7:40 PM schrieb Paul E. McKenney:
On Mon, Jan 13, 2025 at 02:04:58PM -0800, Paul E. McKenney wrote:
On Fri, Jan 10, 2025 at 05:21:59PM +0100, Jonas Oberhauser wrote:
Am 1/10/2025 um 3:54 PM schrieb Paul E. McKenney:
On Thu, Jan 09, 2025 at 07:35:19PM +0100, Jonas Oberhauser wrote:
Am 1/9/2025 um 6:54 PM schrieb Paul E. McKenney:
On Wed, Jan 08, 2025 at 08:17:51PM +0100, Jonas Oberhauser wrote:
[ . . . ]
I currently can not come up with an example where there would be a
(semantic) control dependency from a load to a store that is not in the arm
of an if statement (or a loop / switch of some form with the branch
depending on the load).
I think the control dependency is just a red herring. It is only there to
avoid the data race.
Well, that red herring needs to have a companion fish to swim with in
order to enforce ordering, and I am not seeing that companion.
Or am I (yet again!) missing something subtle here?
It makes more sense to think about how people do message passing (or
seqlock), which might look something like this:
[READ_ONCE]
rmb
[plain read]
and
[plain write]
wmb
[WRITE_ONCE]
Clearly LKMM says that there is some sort of order (not quite happens-before
order though) between the READ_ONCE and the plain read, and between the
plain write and the WRITE_ONCE. This order is clearly defined in the data
race definition, in r-pre-bounded and w-post-bounded.
Now consider
[READ_ONCE]
rmb
[plain read]
// some code that creates order between the plain accesses
[plain write]
wmb
[WRITE_ONCE]
where for some specific reason we can discern that the compiler can not
fully eliminate/move across the barrier either this specific plain read, nor
the plain write, nor the ordering between the two.
In this case, is there order between the READ_ONCE and the WRITE_ONCE, or
not? Of course, we know current LKMM says no. I would say that in those very
specific cases, we do have ordering.
Agreed, for LKMM to deal with seqlock, the read-side critical section
would need to use READ_ONCE(), which is a bit unnatural. The C++
standards committee has been discussing this for some time, as that
memory model also gives data race in that case.
But it might be better to directly model seqlock than to try to make
LKMM deal with the underlying atomic operations.
Maybe I should give an example approach, perhaps inspiring a better
approach.
o Model reader-writer locks in LKMM, including a relaxed
write-lock-held primitive.
o Model sequence locks in terms of reader-writer locks:
o The seqlock writer maps to write lock.
o The seqlock reader maps to read lock, but with a
write-lock-held check. If the write lock is held at
that point, the seqlock tells the caller to retry.
Please note that the point is simply to exercise
the failure path.
o If a value is read in the seqlock reader and used
across a "you need to retry" indication, that
flags a seqlock data race.
But is there a better way?
You need to be careful with those hb edges. The reader critical section
does not have to happen-before the writer critical section, as would
with an actual read-write lock.
I think the solution would have to be along changing the definition of
r-post-bounded.
The read_enter() function reads from a write_exit() and establishes hb.
The read_exit() function also reads from a write_exit(), if the same as
the matching read_enter(), then it returns success, otherwise failure.
Reads po-before a successful read_exit() are bounded with regards to
subsequent write_enter() on the same lock.
Best wishes,
jonas