Received-SPF: pass (google.com: domain of linux-kernel+bounces-169641-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:4601:e00::3 as permitted sender) client-ip=2604:1380:4601:e00::3;
Message-ID: <c97f0529-5a8f-4a82-8e14-0078d4372bdc@huaweicloud.com>
Date: Mon, 6 May 2024 12:05:39 +0200
Precedence: bulk
MIME-Version: 1.0
User-Agent: Mozilla Thunderbird
Subject: Re: [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate
 unordered failing cmpxchg
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
References: <42a43181-a431-44bd-8aff-6b305f8111ba@paulmck-laptop>
 <20240501232132.1785861-2-paulmck@kernel.org>
From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <20240501232132.1785861-2-paulmck@kernel.org>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit


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