[linux-block.git] / tools / memory-model / litmus-tests / MP+onceassign+derefonce.litmus

C MP+onceassign+derefonce

(*
 * Result: Never
 *
 * This litmus test demonstrates that rcu_assign_pointer() and
 * rcu_dereference() suffice to ensure that an RCU reader will not see
 * pre-initialization garbage when it traverses an RCU-protected data
 * structure containing a newly inserted element.
 *)

{
	int *p=y;
	int x;
	int y=0;
}

P0(int *x, int **p) // Producer
{
	WRITE_ONCE(*x, 1);
	rcu_assign_pointer(*p, x);
}

P1(int *x, int **p) // Consumer
{
	int *r0;
	int r1;

	rcu_read_lock();
	r0 = rcu_dereference(*p);
	r1 = READ_ONCE(*r0);
	rcu_read_unlock();
}

exists (1:r0=x /\ 1:r1=0) (* Bad outcome. *)
Commit	Line	Data
8f32543b PM	1	C MP+onceassign+derefonce
	2
	3	(*
	4	* Result: Never
	5	*
	6	* This litmus test demonstrates that rcu_assign_pointer() and
	7	* rcu_dereference() suffice to ensure that an RCU reader will not see
	8	* pre-initialization garbage when it traverses an RCU-protected data
	9	* structure containing a newly inserted element.
	10	*)
1c27b644 PM	11
1c27b644 PM	12	{
acc4bdc5	13	int *p=y;
1947bfcf	14	int x;
acc4bdc5	15	int y=0;
1c27b644 PM	16	}
1c27b644 PM	17
b6ff3084	18	P0(int x, int *p) // Producer
1c27b644 PM	19	{
1c27b644 PM	20	WRITE_ONCE(*x, 1);
acc4bdc5	21	rcu_assign_pointer(*p, x);
1c27b644 PM	22	}
1c27b644 PM	23
b6ff3084	24	P1(int x, int *p) // Consumer
1c27b644 PM	25	{
	26	int *r0;
	27	int r1;
	28
	29	rcu_read_lock();
acc4bdc5	30	r0 = rcu_dereference(*p);
1c27b644 PM	31	r1 = READ_ONCE(*r0);
	32	rcu_read_unlock();
	33	}
	34
b6ff3084	35	exists (1:r0=x /\ 1:r1=0) (* Bad outcome. *)