> @@ -131,7 +159,7 @@ let rec rcu-fence = rcu-gp | srcu-gp | > (rcu-fence ; rcu-link ; rcu-fence) > > (* rb orders instructions just as pb does *) > -let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb* > +let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb* ; [marked]
Testing has revealed some subtle semantics changes for some RCU tests _without_ unmarked memory accesses; an example is reported at the end of this email. I suspect that the improvements you mentioned in this thread can restore the original semantics but I'm reporting this here for further reference. With the above definition of 'rb', we're losing links which originate or target RCU fences, so that this definition is in fact a relaxation w.r.t. the current semantics (even when limiting to marked accesses). The test below, for example, is currently forbidden by the LKMM, but it becomes allowed with this patch. FWIW, I checked that including the RCU fences in 'marked' can restore the original semantics of these tests; I'm still not sure whether this change can make sense though.... Thoughts? Oh, one last (and unrelated) nit before I forget: IIUC, we used to upper-case set names, so I'd also suggest s/marked/Marked, s/plain/Plain and similarly for the other sets to be introduced. Andrea C sync-rcu-is-not-idempotent { } P0(int *x, int *y) { int r0; WRITE_ONCE(*x, 1); synchronize_rcu(); synchronize_rcu(); r0 = READ_ONCE(*y); } P1(int *y, int *z) { int r0; rcu_read_lock(); WRITE_ONCE(*y, 1); r0 = READ_ONCE(*z); rcu_read_unlock(); } P2(int *z, int *x) { int r0; rcu_read_lock(); WRITE_ONCE(*z, 1); r0 = READ_ONCE(*x); rcu_read_unlock(); } exists (0:r0=0 /\ 1:r0=0 /\ 2:r0=0) > > irreflexive rb as rcu >