xref: /linux/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus (revision d0034a7a4ac7fae708146ac0059b9c47a1543f0d) 
11c27b644SPaul E. McKenneyC WRC+poonceonces+Once
21c27b644SPaul E. McKenney
38f32543bSPaul E. McKenney(*
48f32543bSPaul E. McKenney * Result: Sometimes
58f32543bSPaul E. McKenney *
68f32543bSPaul E. McKenney * This litmus test is an extension of the message-passing pattern,
78f32543bSPaul E. McKenney * where the first write is moved to a separate process.  Note that this
88f32543bSPaul E. McKenney * test has no ordering at all.
98f32543bSPaul E. McKenney *)
108f32543bSPaul E. McKenney
11*5c587f9bSAkira Yokosawa{}
121c27b644SPaul E. McKenney
131c27b644SPaul E. McKenneyP0(int *x)
141c27b644SPaul E. McKenney{
151c27b644SPaul E. McKenney	WRITE_ONCE(*x, 1);
161c27b644SPaul E. McKenney}
171c27b644SPaul E. McKenney
181c27b644SPaul E. McKenneyP1(int *x, int *y)
191c27b644SPaul E. McKenney{
201c27b644SPaul E. McKenney	int r0;
211c27b644SPaul E. McKenney
221c27b644SPaul E. McKenney	r0 = READ_ONCE(*x);
231c27b644SPaul E. McKenney	WRITE_ONCE(*y, 1);
241c27b644SPaul E. McKenney}
251c27b644SPaul E. McKenney
261c27b644SPaul E. McKenneyP2(int *x, int *y)
271c27b644SPaul E. McKenney{
281c27b644SPaul E. McKenney	int r0;
291c27b644SPaul E. McKenney	int r1;
301c27b644SPaul E. McKenney
311c27b644SPaul E. McKenney	r0 = READ_ONCE(*y);
321c27b644SPaul E. McKenney	r1 = READ_ONCE(*x);
331c27b644SPaul E. McKenney}
341c27b644SPaul E. McKenney
351c27b644SPaul E. McKenneyexists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
36