xref: /linux/Documentation/litmus-tests/rcu/RCU+sync+free.litmus (revision be4a37973cb078fc64d541f396b7d4d80e45fbe2)
1*be4a3797SJoel Fernandes (Google)C RCU+sync+free
2*be4a3797SJoel Fernandes (Google)
3*be4a3797SJoel Fernandes (Google)(*
4*be4a3797SJoel Fernandes (Google) * Result: Never
5*be4a3797SJoel Fernandes (Google) *
6*be4a3797SJoel Fernandes (Google) * This litmus test demonstrates that an RCU reader can never see a write that
7*be4a3797SJoel Fernandes (Google) * follows a grace period, if it did not see writes that precede that grace
8*be4a3797SJoel Fernandes (Google) * period.
9*be4a3797SJoel Fernandes (Google) *
10*be4a3797SJoel Fernandes (Google) * This is a typical pattern of RCU usage, where the write before the grace
11*be4a3797SJoel Fernandes (Google) * period assigns a pointer, and the writes following the grace period destroy
12*be4a3797SJoel Fernandes (Google) * the object that the pointer used to point to.
13*be4a3797SJoel Fernandes (Google) *
14*be4a3797SJoel Fernandes (Google) * This is one implication of the RCU grace-period guarantee, which says (among
15*be4a3797SJoel Fernandes (Google) * other things) that an RCU read-side critical section cannot span a grace period.
16*be4a3797SJoel Fernandes (Google) *)
17*be4a3797SJoel Fernandes (Google)
18*be4a3797SJoel Fernandes (Google){
19*be4a3797SJoel Fernandes (Google)int x = 1;
20*be4a3797SJoel Fernandes (Google)int *y = &x;
21*be4a3797SJoel Fernandes (Google)int z = 1;
22*be4a3797SJoel Fernandes (Google)}
23*be4a3797SJoel Fernandes (Google)
24*be4a3797SJoel Fernandes (Google)P0(int *x, int *z, int **y)
25*be4a3797SJoel Fernandes (Google){
26*be4a3797SJoel Fernandes (Google)	int *r0;
27*be4a3797SJoel Fernandes (Google)	int r1;
28*be4a3797SJoel Fernandes (Google)
29*be4a3797SJoel Fernandes (Google)	rcu_read_lock();
30*be4a3797SJoel Fernandes (Google)	r0 = rcu_dereference(*y);
31*be4a3797SJoel Fernandes (Google)	r1 = READ_ONCE(*r0);
32*be4a3797SJoel Fernandes (Google)	rcu_read_unlock();
33*be4a3797SJoel Fernandes (Google)}
34*be4a3797SJoel Fernandes (Google)
35*be4a3797SJoel Fernandes (Google)P1(int *x, int *z, int **y)
36*be4a3797SJoel Fernandes (Google){
37*be4a3797SJoel Fernandes (Google)	rcu_assign_pointer(*y, z);
38*be4a3797SJoel Fernandes (Google)	synchronize_rcu();
39*be4a3797SJoel Fernandes (Google)	WRITE_ONCE(*x, 0);
40*be4a3797SJoel Fernandes (Google)}
41*be4a3797SJoel Fernandes (Google)
42*be4a3797SJoel Fernandes (Google)exists (0:r0=x /\ 0:r1=0)
43