xref: /xv6-public/sleep1.p (revision 949352af) 
1/*
2This file defines a Promela model for xv6's
3acquire, release, sleep, and wakeup, along with
4a model of a simple producer/consumer queue.
5
6To run:
7	spinp sleep1.p
8
9(You may need to install Spin, available at http://spinroot.com/.)
10
11After a successful run spin prints something like:
12
13	unreached in proctype consumer
14		(0 of 37 states)
15	unreached in proctype producer
16		(0 of 23 states)
17
18After an unsuccessful run, the spinp script prints
19an execution trace that causes a deadlock.
20
21The safe body of producer reads:
22
23		acquire(lk);
24		x = value; value = x + 1; x = 0;
25		wakeup(0);
26		release(lk);
27		i = i + 1;
28
29If this is changed to:
30
31		x = value; value = x + 1; x = 0;
32		acquire(lk);
33		wakeup(0);
34		release(lk);
35		i = i + 1;
36
37then a deadlock can happen, because the non-atomic
38increment of value conflicts with the non-atomic
39decrement in consumer, causing value to have a bad value.
40Try this.
41
42If it is changed to:
43
44		acquire(lk);
45		x = value; value = x + 1; x = 0;
46		release(lk);
47		wakeup(0);
48		i = i + 1;
49
50then nothing bad happens: it is okay to wakeup after release
51instead of before, although it seems morally wrong.
52*/
53
54#define ITER 4
55#define N 2
56
57bit lk;
58byte value;
59bit sleeping[N];
60
61inline acquire(x)
62{
63	atomic { x == 0; x = 1 }
64}
65
66inline release(x)
67{
68	assert x==1;
69	x = 0
70}
71
72inline sleep(cond, lk)
73{
74	assert !sleeping[_pid];
75	if
76	:: cond ->
77		skip
78	:: else ->
79		atomic { release(lk); sleeping[_pid] = 1 };
80		sleeping[_pid] == 0;
81		acquire(lk)
82	fi
83}
84
85inline wakeup()
86{
87	w = 0;
88	do
89	:: w < N ->
90		sleeping[w] = 0;
91		w = w + 1
92	:: else ->
93		break
94	od
95}
96
97active[N] proctype consumer()
98{
99	byte i, x;
100
101	i = 0;
102	do
103	:: i < ITER ->
104		acquire(lk);
105		sleep(value > 0, lk);
106		x = value; value = x - 1; x = 0;
107		release(lk);
108		i = i + 1;
109	:: else ->
110		break
111	od;
112	i = 0;
113	skip
114}
115
116active[N] proctype producer()
117{
118	byte i, x, w;
119
120	i = 0;
121	do
122	:: i < ITER ->
123		acquire(lk);
124		x = value; value = x + 1; x = 0;
125		release(lk);
126		wakeup();
127		i = i + 1;
128	:: else ->
129		break
130	od;
131	i = 0;
132	skip
133}
134
135