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 for Android: free password hash cracker in your pocket
[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Date: Mon, 6 May 2024 18:30:45 +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/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].
> 
> 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 \ rmw) ; [RMW_MB] ; po^? ; [M]
>    | [M] ; po^? ; [RMW_MB] ; (po \ rmw) ; [M]
>    | ...
> 
> The po \ rmw is because ordering is not provided internally of the 
> rmw

(removed the unnecessary si since LKMM is still non-mixed-accesses)


This could also be written with a single rule:

      | [M] ; (po \ rmw) & (po^?; [RMW_MB] ; po^?) ; [M]


> I suspect that after we added [rmw] sequences it could 
> perhaps be simplified [...]
> 

No, my suspicion is wrong - this would incorrectly let full-barrier RMWs
act like strong fences when they appear in an rmw sequence.

  if (z==1)  ||  x = 2;     ||  xchg(&y,2)  || if (y==2)
    x = 1;   ||  y =_rel 1; ||              ||    z=1;


right now, we allow x=2 overwriting x=1 (in case the last thread does 
not propagate x=2 along with z=1) because on power, the xchg might be
implemented with a sync that doesn't get executed until the very end
of the program run.


Instead of its negative form (everything other than inside the rmw),
it could also be rewritten positively. Here's a somewhat short form:

let mb =
      [M] ; fencerel(Mb) ; [M]
    (* everything across a full barrier RMW is ordered. This includes up 
to one event inside the RMW. *)
    | [M] ; po ; [RMW_MB] ; po ; [M]
    (* full barrier RMW writes are ordered with everything behind the RMW *)
    | [W & RMW_MB] ; po ; [M]
    (* full barrier RMW reads are ordered with everything before the RMW *)
    | [M] ; po ; [R & RMW_MB]
    | ...



Good luck,
jonas


Powered by blists - more mailing lists

Powered by Openwall GNU/*/Linux Powered by OpenVZ