linux-kernel - Re: [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Date: Mon, 6 May 2024 12:05:39 +0200
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: "Paul E. McKenney" <paulmck@...nel.org>, linux-kernel@...r.kernel.org,
 linux-arch@...r.kernel.org, kernel-team@...a.com, mingo@...nel.org
Cc: stern@...land.harvard.edu, parri.andrea@...il.com, will@...nel.org,
 peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
 dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
 akiyks@...il.com, Frederic Weisbecker <frederic@...nel.org>,
 Daniel Lustig <dlustig@...dia.com>, Joel Fernandes <joel@...lfernandes.org>,
 Mark Rutland <mark.rutland@....com>, Jonathan Corbet <corbet@....net>,
 linux-doc@...r.kernel.org
Subject: Re: [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate
 unordered failing cmpxchg

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