From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To: paulmck@kernel.org
Cc: Alan Stern <stern@rowland.harvard.edu>,
parri.andrea@gmail.com, will@kernel.org, peterz@infradead.org,
boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com,
j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com,
dlustig@nvidia.com, joel@joelfernandes.org, urezki@gmail.com,
quic_neeraju@quicinc.com, frederic@kernel.org,
linux-kernel@vger.kernel.org, lkmm@lists.linux.dev,
hernan.poncedeleon@huaweicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA
Date: Thu, 16 Jan 2025 20:13:28 +0100 [thread overview]
Message-ID: <cbde6574-cf5d-4160-a0fe-46fcafa69eac@huaweicloud.com> (raw)
In-Reply-To: <3b3a7c1a-c40f-4a98-b328-bb4327876606@paulmck-laptop>
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
next prev parent reply other threads:[~2025-01-16 19:13 UTC|newest]
Thread overview: 59+ messages / expand[flat|nested] mbox.gz Atom feed top
2025-01-06 21:40 [RFC] tools/memory-model: Rule out OOTA Jonas Oberhauser
2025-01-07 10:06 ` Peter Zijlstra
2025-01-07 11:02 ` Jonas Oberhauser
2025-01-07 15:46 ` Jonas Oberhauser
2025-01-07 16:09 ` Alan Stern
2025-01-07 18:47 ` Paul E. McKenney
2025-01-08 17:39 ` Jonas Oberhauser
2025-01-08 18:09 ` Paul E. McKenney
2025-01-08 19:17 ` Jonas Oberhauser
2025-01-09 17:54 ` Paul E. McKenney
2025-01-09 18:35 ` Jonas Oberhauser
2025-01-10 14:54 ` Paul E. McKenney
2025-01-10 16:21 ` Jonas Oberhauser
2025-01-13 22:04 ` Paul E. McKenney
2025-01-16 18:40 ` Paul E. McKenney
2025-01-16 19:13 ` Jonas Oberhauser [this message]
2025-01-16 19:31 ` Paul E. McKenney
2025-01-16 20:21 ` Jonas Oberhauser
2025-01-16 19:28 ` Jonas Oberhauser
2025-01-16 19:39 ` Paul E. McKenney
2025-01-17 12:08 ` Jonas Oberhauser
2025-01-16 19:08 ` Jonas Oberhauser
2025-01-16 23:02 ` Alan Stern
2025-01-17 8:34 ` Hernan Ponce de Leon
2025-01-17 11:29 ` Jonas Oberhauser
2025-01-17 20:01 ` Alan Stern
2025-01-21 10:36 ` Jonas Oberhauser
2025-01-21 16:39 ` Alan Stern
2025-01-22 3:46 ` Jonas Oberhauser
2025-01-22 19:11 ` Alan Stern
2025-01-17 15:52 ` Alan Stern
2025-01-17 16:45 ` Jonas Oberhauser
2025-01-17 19:02 ` Alan Stern
2025-01-09 20:37 ` Peter Zijlstra
2025-01-09 21:13 ` Paul E. McKenney
2025-01-08 17:33 ` Jonas Oberhauser
2025-01-08 18:47 ` Alan Stern
2025-01-08 19:22 ` Jonas Oberhauser
2025-01-09 16:17 ` Alan Stern
2025-01-09 16:44 ` Jonas Oberhauser
2025-01-09 19:27 ` Alan Stern
2025-01-09 20:09 ` Jonas Oberhauser
2025-01-10 3:12 ` Alan Stern
2025-01-10 12:21 ` Jonas Oberhauser
2025-01-10 21:51 ` Alan Stern
2025-01-11 12:46 ` Jonas Oberhauser
2025-01-11 21:19 ` Alan Stern
2025-01-12 15:55 ` Jonas Oberhauser
2025-01-13 19:43 ` Alan Stern
2025-07-23 0:43 ` Paul E. McKenney
2025-07-23 7:26 ` Hernan Ponce de Leon
2025-07-23 16:39 ` Paul E. McKenney
2025-07-24 14:14 ` Paul E. McKenney
2025-07-25 5:23 ` Hernan Ponce de Leon
2025-07-29 20:34 ` Paul E. McKenney
2025-07-23 17:13 ` Alan Stern
2025-07-23 17:27 ` Paul E. McKenney
2025-07-23 19:25 ` Alan Stern
2025-07-23 19:57 ` Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=cbde6574-cf5d-4160-a0fe-46fcafa69eac@huaweicloud.com \
--to=jonas.oberhauser@huaweicloud.com \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=frederic@kernel.org \
--cc=hernan.poncedeleon@huaweicloud.com \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=linux-kernel@vger.kernel.org \
--cc=lkmm@lists.linux.dev \
--cc=luc.maranget@inria.fr \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=quic_neeraju@quicinc.com \
--cc=stern@rowland.harvard.edu \
--cc=urezki@gmail.com \
--cc=will@kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).