From: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
To: paulmck@kernel.org, Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
kernel-team@meta.com, mingo@kernel.org,
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,
Frederic Weisbecker <frederic@kernel.org>,
Daniel Lustig <dlustig@nvidia.com>,
Joel Fernandes <joel@joelfernandes.org>,
Mark Rutland <mark.rutland@arm.com>,
Jonathan Corbet <corbet@lwn.net>,
linux-doc@vger.kernel.org
Subject: Re: [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg
Date: Wed, 15 May 2024 08:44:30 +0200 [thread overview]
Message-ID: <143273e9-1243-60bc-4fb0-eea6fb3de355@huaweicloud.com> (raw)
In-Reply-To: <2a695f63-6c9a-4837-ac03-f0a5c63daaaf@paulmck-laptop>
On 5/6/2024 8:00 PM, Paul E. McKenney wrote:
> On Mon, May 06, 2024 at 06:30:45PM +0200, Jonas Oberhauser wrote:
>> Am 5/6/2024 um 12:05 PM schrieb Jonas Oberhauser:
>>> Am 5/2/2024 um 1:21 AM schrieb Paul E. McKenney:
>>>> This commit adds four litmus tests showing that a failing cmpxchg()
>>>> operation is unordered unless followed by an smp_mb__after_atomic()
>>>> operation.
>>>
>>> So far, my understanding was that all RMW operations without suffix
>>> (xchg(), cmpxchg(), ...) will be interpreted as F[Mb];...;F[Mb].
>>>
>>> I guess this shows again how important it is to model these full
>>> barriers explicitly inside the cat model, instead of relying on implicit
>>> conversions internal to herd.
>>>
>>> I'd like to propose a patch to this effect.
>>>
>>> What is the intended behavior of a failed cmpxchg()? Is it the same as a
>>> relaxed one?
>
> Yes, and unless I am too confused, LKMM currently does implement this.
> Please let me know if I am missing something.
>
>>> My suggestion would be in the direction of marking read and write events
>>> of these operations as Mb, and then defining
>>>
>>> (* full barrier events that appear in non-failing RMW *)
>>> let RMW_MB = Mb & (dom(rmw) | range(rmw))
>>>
>>>
>>> let mb =
>>> [M] ; fencerel(Mb) ; [M]
>>> | [M] ; (po \ rmw) ; [RMW_MB] ; po^? ; [M]
>>> | [M] ; po^? ; [RMW_MB] ; (po \ rmw) ; [M]
>>> | ...
>>>
>>> The po \ rmw is because ordering is not provided internally of the rmw
>>
>> (removed the unnecessary si since LKMM is still non-mixed-accesses)
>
> Addition of mixed-access support would be quite welcome!
>
>> This could also be written with a single rule:
>>
>> | [M] ; (po \ rmw) & (po^?; [RMW_MB] ; po^?) ; [M]
>>
>>> I suspect that after we added [rmw] sequences it could perhaps be
>>> simplified [...]
>>
>> No, my suspicion is wrong - this would incorrectly let full-barrier RMWs
>> act like strong fences when they appear in an rmw sequence.
>>
>> if (z==1) || x = 2; || xchg(&y,2) || if (y==2)
>> x = 1; || y =_rel 1; || || z=1;
>>
>>
>> right now, we allow x=2 overwriting x=1 (in case the last thread does not
>> propagate x=2 along with z=1) because on power, the xchg might be
>> implemented with a sync that doesn't get executed until the very end
>> of the program run.
>>
>>
>> Instead of its negative form (everything other than inside the rmw),
>> it could also be rewritten positively. Here's a somewhat short form:
>>
>> let mb =
>> [M] ; fencerel(Mb) ; [M]
>> (* everything across a full barrier RMW is ordered. This includes up to
>> one event inside the RMW. *)
>> | [M] ; po ; [RMW_MB] ; po ; [M]
>> (* full barrier RMW writes are ordered with everything behind the RMW *)
>> | [W & RMW_MB] ; po ; [M]
>> (* full barrier RMW reads are ordered with everything before the RMW *)
>> | [M] ; po ; [R & RMW_MB]
>> | ...
>
> Does this produce the results expected by the litmus tests in the Linux
> kernel source tree and also those at https://github.com/paulmckrcu/litmus?
>
> Thanx, Paul
I implemented in the dartagnan tool the changes proposed by Jonas (i.e.
changing the mb definition in the cat model and removing the fences that
were added programmatically).
I run this using the ~5K litmus test I have (it should include
everything from the source tree + the non-LISA ones from your repo). I
also checked with the version of qspinlock discussed in [1].
I do get the expected results.
Hernan
[1] https://lkml.org/lkml/2022/8/26/597
next prev parent reply other threads:[~2024-05-15 6:45 UTC|newest]
Thread overview: 23+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-04-04 19:26 [PATCH memory-model 0/3] LKMM updates for v6.10 Paul E. McKenney
2024-04-04 19:26 ` [PATCH memory-model 1/3] Documentation/litmus-tests: Add locking tests to README Paul E. McKenney
2024-04-04 19:26 ` [PATCH memory-model 2/3] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg Paul E. McKenney
2024-04-05 10:05 ` Andrea Parri
2024-04-08 20:46 ` Paul E. McKenney
2024-04-09 10:43 ` Andrea Parri
2024-04-04 19:26 ` [PATCH memory-model 3/3] Documentation/atomic_t: Emphasize that failed atomic operations give no ordering Paul E. McKenney
2024-05-01 23:21 ` [PATCH v2 memory-model 0/3] LKMM updates for v6.10 Paul E. McKenney
2024-05-01 23:21 ` [PATCH memory-model 1/4] Documentation/litmus-tests: Add locking tests to README Paul E. McKenney
2024-05-01 23:21 ` [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg Paul E. McKenney
2024-05-06 10:05 ` Jonas Oberhauser
2024-05-06 16:30 ` Jonas Oberhauser
2024-05-06 18:00 ` Paul E. McKenney
2024-05-06 19:21 ` Alan Stern
2024-05-07 9:03 ` Jonas Oberhauser
2024-05-08 1:17 ` Andrea Parri
2024-05-07 9:11 ` Jonas Oberhauser
2024-05-15 6:44 ` Hernan Ponce de Leon [this message]
2024-05-15 15:01 ` Paul E. McKenney
2024-05-01 23:21 ` [PATCH memory-model 3/4] Documentation/atomic_t: Emphasize that failed atomic operations give no ordering Paul E. McKenney
2024-05-01 23:21 ` [PATCH memory-model 4/4] Documentation/litmus-tests: Make cmpxchg() tests safe for klitmus Paul E. McKenney
2024-05-02 9:36 ` [PATCH v2 memory-model 0/3] LKMM updates for v6.10 Andrea Parri
2024-05-02 13:46 ` 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=143273e9-1243-60bc-4fb0-eea6fb3de355@huaweicloud.com \
--to=hernan.poncedeleon@huaweicloud.com \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=corbet@lwn.net \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=frederic@kernel.org \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=jonas.oberhauser@huaweicloud.com \
--cc=kernel-team@meta.com \
--cc=linux-arch@vger.kernel.org \
--cc=linux-doc@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=mark.rutland@arm.com \
--cc=mingo@kernel.org \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--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).