On Fri, Feb 14, 2020 at 09:18:26AM +0100, Andrea Parri wrote: > > > @@ -0,0 +1,29 @@ > > > +C Atomic-RMW+mb__after_atomic-is-strong-acquire > > > + > > > +(* > > > + * Result: Never > > > + * > > > + * Test of an atomic RMW followed by a smp_mb__after_atomic() is > > > + * "strong-acquire": both the read and write part of the RMW is ordered before > > > + * the subsequential memory accesses. > > > + *) > > > + > > > +{ > > > +} > > > + > > > +P0(int *x, atomic_t *y) > > > +{ > > > + r0 = READ_ONCE(*x); > > > + smp_rmb(); > > > + r1 = atomic_read(y); > > IIRC, klitmus7 needs a declaration for these local variables, say > (trying to keep herd7 happy): > Got it. I will add the declaration in the next version. It's just that herd doesn't need those so I haven't put them in this version ;-) Thanks! Regards, Boqun > P0(int *x, atomic_t *y) > { > int r0; > int r1; > > r0 = READ_ONCE(*x); > smp_rmb(); > r1 = atomic_read(y); > } > > Thanks, > Andrea