summaryrefslogtreecommitdiff
path: root/Documentation/litmus-tests/locking/RM-fixed.litmus
blob: b628175596160f1792c27ce9f634bb924a87ce2d (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
32
33
34
35
36
37
38
39
40
41
C RM-fixed

(*
 * Result: Never
 *
 * This litmus test demonstrates that the old "roach motel" approach
 * to locking, where code can be freely moved into critical sections,
 * cannot be used in the Linux kernel.
 *)

{
	int x;
	atomic_t y;
}

P0(int *x, atomic_t *y, spinlock_t *lck)
{
	int r2;

	spin_lock(lck);
	r2 = atomic_inc_return(y);
	WRITE_ONCE(*x, 1);
	spin_unlock(lck);
}

P1(int *x, atomic_t *y, spinlock_t *lck)
{
	int r0;
	int r1;
	int r2;

	r0 = READ_ONCE(*x);
	r1 = READ_ONCE(*x);
	spin_lock(lck);
	r2 = atomic_inc_return(y);
	spin_unlock(lck);
}

locations [x;0:r2;1:r0;1:r1;1:r2]
filter (1:r0=0 /\ 1:r1=1)
exists (1:r2=1)