summaryrefslogtreecommitdiff
path: root/tools/memory-model/litmus-tests/S+poonceonces.litmus
blob: 7775c23143a0caa635cff6873ae5edd04ae8c174 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
C S+poonceonces

(*
 * Result: Sometimes
 *
 * Starting with a two-process release-acquire chain ordering P0()'s
 * first store against P1()'s final load, if the smp_store_release()
 * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
 * READ_ONCE(), is ordering preserved?
 *)

{
	int x;
	int y;
}

P0(int *x, int *y)
{
	WRITE_ONCE(*x, 2);
	WRITE_ONCE(*y, 1);
}

P1(int *x, int *y)
{
	int r0;

	r0 = READ_ONCE(*y);
	WRITE_ONCE(*x, 1);
}

exists (x=2 /\ 1:r0=1)