From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To: Alan Stern <stern@rowland.harvard.edu>,
"Paul E. McKenney" <paulmck@kernel.org>
Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
kernel-team@meta.com, mingo@kernel.org, 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: Tue, 7 May 2024 11:03:27 +0200 [thread overview]
Message-ID: <fd2369ed-1e84-4e44-ac80-cd316f8e7051@huaweicloud.com> (raw)
In-Reply-To: <c168f56f-dfae-4cac-bc61-fc5a93ee3aed@rowland.harvard.edu>
Am 5/6/2024 um 9:21 PM schrieb Alan Stern:
> On Mon, May 06, 2024 at 11:00:42AM -0700, 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].
>
> It's more accurate to say that RMW operations without a suffix that
> return a value will be interpreted that way. So for example,
> atomic_inc() doesn't imply any ordering, because it doesn't return a
> value.
>
I see, thanks.
>>>> barriers explicitlyinside the cat model, instead of relying on implicit
>>>> conversions internal to herd.
>
> Don't the annotations in linux-kernel.def and linux-kernel.bell (like
> "noreturn") already make this explicit?
Not that I'm aware. All I can see there is that according to .bell RMW
don't have an mb mode, but according to .def they do.
How this mb disappears between parsing the code (.def) and interpreting
it (.bell) is totally implicit. Including how noreturn affects this
disappeareance.
In fact most tool developers that support LKMM (Viktor, Hernan, and Luc)
were at least once confused about it. And I think they read those files
more carefully than I.
https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904
Note that while there's no explicit annotation of noreturn in the .def
file, at least I can guess based on context that it should be annotated
on all the functions that don't have _return and for which also a
version with _return exists.
have fun,
jonas
next prev parent reply other threads:[~2024-05-07 9:03 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 [this message]
2024-05-08 1:17 ` Andrea Parri
2024-05-07 9:11 ` Jonas Oberhauser
2024-05-15 6:44 ` Hernan Ponce de Leon
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=fd2369ed-1e84-4e44-ac80-cd316f8e7051@huaweicloud.com \
--to=jonas.oberhauser@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=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 NNTP newsgroup(s).