…
LISA rcu-B-cumulativity-failure.litmus
(* If write-release is B-cumulative, this test should be forbidden.
P0 P1 P2 P3 P4
rcu_read_lock d: Wa=1 g: Ry=1 k: Wu=1 m: Rz=1
a: Ra=0 synchronize_rcu data dep. l: Wv=r1 smp_rmb
b: Wx=1 f: Wy=1 h: Wz=1 n: Ru=0
rcu_read_unlock i: Rv=a1
j: Rx=0
("=r" means write-release and "=a" means read-acquire.)
a: in P0's critical section does not see d:Wa=1, so the c.s. starts
before the grace period in P1. Therefore it must end before the
g.p. ends, which means it must be possible to add a write-release
c: after b: with a corresponding read-acquire e: followed by smp_mb
at the end of the synchronize_rcu.
But then we have:
j: ->fre b: ->rel c: ->rfe e: ->mb f: ->rfe g:
and this forms an instance of the "obs" relation:
(fre ; propbase+; rfe) & int.
From this we obtain j: ->hb g:, which yields:
n: ->fre k: ->rel l: ->rfe i: ->acq j: ->hb g: ->data h: ->rfe m:
which is another instance of the "obs" relation (if write-release is
B-cumulative). Therefore we get:
n: ->hb m: ->rmb n:
which violates the Causality axiom. But if write-release isn't
B-cumulative then this reasoning does not go through and the test is
allowed.
*)
{
}
P0 | P1 | P2 | P3 | P4 ;
f[rcu_read_lock] | w[once] a 1 | r[once] r2 y | w[once] u 1 | r[once] r5 z ;
r[once] r1 a | f[sync] | w[once] z r2 | w[release] v 1 | f[rmb] ;
w[once] x 1 | w[once] y 1 | r[acquire] r3 v | | r[once] r6 u ;
f[rcu_read_unlock] | | r[once] r4 x | | ;
Observed
4:r6=1; 4:r5=1; 2:r4=1; 2:r3=1; 2:r2=1; 0:r1=1;
and 4:r6=0; 4:r5=1; 2:r4=1; 2:r3=1; 2:r2=1; 0:r1=1;
and 4:r6=0; 4:r5=0; 2:r4=1; 2:r3=1; 2:r2=1; 0:r1=1;
and 4:r6=1; 4:r5=1; 2:r4=0; 2:r3=1; 2:r2=1; 0:r1=1;
and 4:r6=0; 4:r5=1; 2:r4=0; 2:r3=1; 2:r2=1; 0:r1=1;
and 4:r6=1; 4:r5=0; 2:r4=0; 2:r3=1; 2:r2=1; 0:r1=1;
and 4:r6=0; 4:r5=0; 2:r4=0; 2:r3=1; 2:r2=1; 0:r1=1;
and 4:r6=1; 4:r5=1; 2:r4=1; 2:r3=0; 2:r2=1; 0:r1=1;
and 4:r6=0; 4:r5=1; 2:r4=1; 2:r3=0; 2:r2=1; 0:r1=1;
and 4:r6=1; 4:r5=0; 2:r4=1; 2:r3=0; 2:r2=1; 0:r1=1;
and 4:r6=0; 4:r5=0; 2:r4=1; 2:r3=0; 2:r2=1; 0:r1=1;
and 4:r6=1; 4:r5=1; 2:r4=0; 2:r3=0; 2:r2=1; 0:r1=1;
and 4:r6=0; 4:r5=1; 2:r4=0; 2:r3=0; 2:r2=1; 0:r1=1;
and 4:r6=1; 4:r5=0; 2:r4=0; 2:r3=0; 2:r2=1; 0:r1=1;
and 4:r6=0; 4:r5=0; 2:r4=0; 2:r3=0; 2:r2=1; 0:r1=1;
and 4:r6=1; 4:r5=1; 2:r4=1; 2:r3=1; 2:r2=1; 0:r1=0;
and 4:r6=0; 4:r5=1; 2:r4=1; 2:r3=1; 2:r2=1; 0:r1=0;
and 4:r6=0; 4:r5=0; 2:r4=1; 2:r3=1; 2:r2=1; 0:r1=0;
and 4:r6=1; 4:r5=1; 2:r4=0; 2:r3=1; 2:r2=1; 0:r1=0;
and 4:r6=0; 4:r5=1; 2:r4=0; 2:r3=1; 2:r2=1; 0:r1=0;
and 4:r6=1; 4:r5=0; 2:r4=0; 2:r3=1; 2:r2=1; 0:r1=0;
and 4:r6=0; 4:r5=0; 2:r4=0; 2:r3=1; 2:r2=1; 0:r1=0;
and 4:r6=1; 4:r5=1; 2:r4=1; 2:r3=0; 2:r2=1; 0:r1=0;
and 4:r6=0; 4:r5=1; 2:r4=1; 2:r3=0; 2:r2=1; 0:r1=0;
and 4:r6=1; 4:r5=0; 2:r4=1; 2:r3=0; 2:r2=1; 0:r1=0;
and 4:r6=0; 4:r5=0; 2:r4=1; 2:r3=0; 2:r2=1; 0:r1=0;
and 4:r6=1; 4:r5=1; 2:r4=0; 2:r3=0; 2:r2=1; 0:r1=0;
and 4:r6=0; 4:r5=1; 2:r4=0; 2:r3=0; 2:r2=1; 0:r1=0;
and 4:r6=1; 4:r5=0; 2:r4=0; 2:r3=0; 2:r2=1; 0:r1=0;
and 4:r6=0; 4:r5=0; 2:r4=0; 2:r3=0; 2:r2=1; 0:r1=0;