Documentation: LKMM: Add litmus test for RCU GP guarantee where reader stores

============

LITMUS TESTS

============

RCU (/rcu directory)

--------------------

RCU+sync+read.litmus

RCU+sync+free.litmus

    Both the above litmus tests demonstrate the RCU grace period guarantee

    that an RCU read-side critical section can never span a grace period.

C RCU+sync+read

(*

 * Result: Never

 *

 * This litmus test demonstrates that after a grace period, an RCU updater always

 * sees all stores done in prior RCU read-side critical sections. Such

 * read-side critical sections would have ended before the grace period ended.

 *

 * This is one implication of the RCU grace-period guarantee, which says (among

 * other things) that an RCU read-side critical section cannot span a grace period.

 *)

{

int x = 0;

int y = 0;

}

P0(int *x, int *y)

{

	rcu_read_lock();

	WRITE_ONCE(*x, 1);

	WRITE_ONCE(*y, 1);

	rcu_read_unlock();

}

P1(int *x, int *y)

{

	int r0;

	int r1;

	r0 = READ_ONCE(*x);

	synchronize_rcu();

	r1 = READ_ONCE(*y);

}

exists (1:r0=1 /\ 1:r1=0)