From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To: "Paul E. McKenney" <paulmck@kernel.org>,
linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
kernel-team@meta.com, mingo@kernel.org
Cc: 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: Mon, 6 May 2024 12:05:39 +0200 [thread overview]
Message-ID: <c97f0529-5a8f-4a82-8e14-0078d4372bdc@huaweicloud.com> (raw)
In-Reply-To: <20240501232132.1785861-2-paulmck@kernel.org>
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?
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 \ si ; rmw) ; [RMW_MB] ; po^? ; [M]
| [M] ; po^? ; [RMW_MB] ; (po \ rmw ; si) ; [M]
| ...
The po \ si;rmw is because ordering is not provided internally of the
rmw, although I suspect that after we added release sequences it could
perhaps be simplified to
let mb =
[M] ; fencerel(Mb) ; [M]
| [M] ; po ; [RMW_MB] ; po^? ; [M]
| [M] ; po^? ; [RMW_MB] ; po ; [M]
| ...
or
let mb =
[M] ; fencerel(Mb) ; [M]
| [M] ; po & (po^? ; [RMW_MB] ; po^?) ; [M]
| ...
(the po & is necessary to avoid trivial hb cycles of an RMW event
happening before itself)
Any interest?
Have fun,
jonas
next prev parent reply other threads:[~2024-05-06 10:06 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
[not found] <42a43181-a431-44bd-8aff-6b305f8111ba@paulmck-laptop>
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 [this message]
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
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
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=c97f0529-5a8f-4a82-8e14-0078d4372bdc@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 read-only IMAP folder(s) and NNTP newsgroup(s).