File: S%2Bpoonceonces.litmus

package info (click to toggle)
linux 4.19.249-2
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 968,784 kB
  • sloc: ansic: 16,810,930; asm: 272,263; makefile: 38,450; sh: 33,900; perl: 27,702; python: 21,148; cpp: 5,068; yacc: 4,650; lex: 2,584; awk: 1,386; ruby: 25; sed: 5
file content (28 lines) | stat: -rw-r--r-- 462 bytes parent folder | download | duplicates (37) 
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
 
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?
 *)

{}

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)