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
| ||
|
Date: Fri, 14 Feb 2020 18:40:03 +0800 From: Boqun Feng <boqun.feng@...il.com> To: Andrea Parri <parri.andrea@...il.com> Cc: linux-kernel@...r.kernel.org, Alan Stern <stern@...land.harvard.edu>, Will Deacon <will@...nel.org>, Peter Zijlstra <peterz@...radead.org>, Nicholas Piggin <npiggin@...il.com>, David Howells <dhowells@...hat.com>, Jade Alglave <j.alglave@....ac.uk>, Luc Maranget <luc.maranget@...ia.fr>, "Paul E. McKenney" <paulmck@...nel.org>, Akira Yokosawa <akiyks@...il.com>, Daniel Lustig <dlustig@...dia.com>, Jonathan Corbet <corbet@....net>, linux-arch@...r.kernel.org, linux-doc@...r.kernel.org Subject: Re: [RFC 2/3] tools/memory-model: Add a litmus test for atomic_set() On Fri, Feb 14, 2020 at 09:12:13AM +0100, Andrea Parri wrote: > > @@ -0,0 +1,24 @@ > > +C Atomic-set-observable-to-RMW > > + > > +(* > > + * Result: Never > > + * > > + * Test of the result of atomic_set() must be observable to atomic RMWs. > > + *) > > + > > +{ > > + atomic_t v = ATOMIC_INIT(1); > > +} > > + > > +P0(atomic_t *v) > > +{ > > + (void)atomic_add_unless(v,1,0); > > We blacklisted this primitive some time ago, cf. section "LIMITATIONS", > entry (6b) in tools/memory-model/README; the discussion was here: > > https://lkml.kernel.org/r/20180829211053.20531-3-paulmck@linux.vnet.ibm.com > And in an email replying to that email, you just tried and seemed atomic_add_unless() works ;-) > but unfortunately I can't remember other details at the moment: maybe > it is just a matter of or the proper time to update that section. > I spend a few time looking into the changes in herd, the dependency problem seems to be as follow: For atomic_add_unless(ptr, a, u), the return value (true or false) depends on both *ptr and u, this is different than other atomic RMW, whose return value only depends on *ptr. Considering the following litmus test: C atomic_add_unless-dependency { int y = 1; } P0(int *x, int *y, int *z) { int r0; int r1; int r2; r0 = READ_ONCE(*x); if (atomic_add_unless(y, 2, r0)) WRITE_ONCE(*z, 42); else WRITE_ONCE(*z, 1); } P1(int *x, int *y, int *z) { int r0; r0 = smp_load_acquire(z); WRITE_ONCE(*x, 1); } exists (1:r0 = 1 /\ 0:r0 = 1) , the exist-clause will never trigger, however if we replace "atomic_add_unless(y, 2, r0)" with "atomic_add_unless(y, 2, 1)", the write on *z and the read from *x on CPU 0 are not ordered, so we could observe the exist-clause triggered. I just tried with the latest herd, and herd can work out this dependency. So I think we are good now and can change the limitation section in the document. But I will wait for Luc's input for this. Luc, did I get this correct? Is there any other limitation on atomic_add_unless() now? Regards, Boqun > Thanks, > Andrea
Powered by blists - more mailing lists