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: Tue, 7 May 2024 11:03:27 +0200
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: Alan Stern <stern@...land.harvard.edu>,
 "Paul E. McKenney" <paulmck@...nel.org>
Cc: linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org,
 kernel-team@...a.com, mingo@...nel.org, 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/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