Subversion Repositories planix.SVN

Rev

Rev 2 | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 1 
/*
2 
spin -a semaphore.p
3 
pcc -DSAFETY -DREACH -DMEMLIM'='500 -o pan pan.c
4 
pan -i
5 
rm pan.* pan
6 
 
7 
*/
8 
 
9 
#define N 3
10 
 
11 
bit listlock;
12 
byte value;
13 
bit onlist[N];
14 
bit waiting[N];
15 
bit sleeping[N];
16 
bit acquired[N];
17 
 
18 
inline lock(x)
19 
{
20 
	atomic { x == 0; x = 1 }
21 
}
22 
 
23 
inline unlock(x)
24 
{
25 
	assert x==1;
26 
	x = 0
27 
}
28 
 
29 
inline sleep(cond)
30 
{
31 
	assert !sleeping[_pid];
32 
	assert !interrupted;
33 
	if
34 
	:: cond
35 
	:: atomic { else -> sleeping[_pid] = 1 } ->
36 
		!sleeping[_pid]
37 
	fi;
38 
	if
39 
	:: skip
40 
	:: interrupted = 1
41 
	fi
42 
}
43 
 
44 
inline wakeup(id)
45 
{
46 
	if
47 
	:: sleeping[id] == 1 -> sleeping[id] = 0
48 
	:: else
49 
	fi
50 
}
51 
 
52 
inline semqueue()
53 
{
54 
	lock(listlock);
55 
	assert !onlist[_pid];
56 
	onlist[_pid] = 1;
57 
	unlock(listlock)
58 
}
59 
 
60 
inline semdequeue()
61 
{
62 
	lock(listlock);
63 
	assert onlist[_pid];
64 
	onlist[_pid] = 0;
65 
	waiting[_pid] = 0;
66 
	unlock(listlock)
67 
}
68 
 
69 
inline semwakeup(n)
70 
{
71 
	byte i, j;
72 
 
73 
	lock(listlock);
74 
	i = 0;
75 
	j = n;
76 
	do
77 
	:: (i < N && j > 0) ->
78 
		if
79 
		:: onlist[i] && waiting[i] ->
80 
			atomic { printf("kicked %d\n", i);
81 
			waiting[i] = 0 };
82 
			wakeup(i);
83 
			j--
84 
		:: else
85 
		fi;
86 
		i++
87 
	:: else -> break
88 
	od;
89 
	/* reset i and j to reduce state space */
90 
	i = 0;
91 
	j = 0;
92 
	unlock(listlock)
93 
}
94 
 
95 
inline semrelease(n)
96 
{
97 
	atomic { value = value+n; printf("release %d\n", n); };
98 
	semwakeup(n)
99 
}
100 
 
101 
inline canacquire()
102 
{
103 
	atomic { value > 0 -> value--; };
104 
	acquired[_pid] = 1
105 
}
106 
 
107 
#define semawoke() !waiting[_pid]
108 
 
109 
inline semacquire(block)
110 
{
111 
	if
112 
	:: atomic { canacquire() -> printf("easy acquire\n"); } ->
113 
		goto out
114 
	:: else
115 
	fi;
116 
	if
117 
	:: !block -> goto out
118 
	:: else
119 
	fi;
120 
 
121 
	semqueue();
122 
	do
123 
	:: skip ->
124 
		waiting[_pid] = 1;
125 
		if
126 
		:: atomic { canacquire() -> printf("hard acquire\n"); } ->
127 
			break
128 
		:: else
129 
		fi;
130 
		sleep(semawoke())
131 
		if
132 
		:: interrupted ->
133 
			printf("%d interrupted\n", _pid);
134 
			break
135 
		:: !interrupted
136 
		fi
137 
	od;
138 
	semdequeue();
139 
	if
140 
	:: !waiting[_pid] ->
141 
		semwakeup(1)
142 
	:: else
143 
	fi;
144 
out:
145 
	assert (!block || interrupted || acquired[_pid]);
146 
	assert !(interrupted && acquired[_pid]);
147 
	assert !waiting[_pid];
148 
	printf("%d done\n", _pid);
149 
}
150 
 
151 
active[N] proctype acquire()
152 
{
153 
	bit interrupted;
154 
 
155 
	semacquire(1);
156 
	printf("%d finished\n", _pid);
157 
	skip
158 
}
159 
 
160 
active proctype release()
161 
{
162 
	byte k;
163 
 
164 
	k = 0;
165 
	do
166 
	:: k < N ->
167 
		semrelease(1);
168 
		k++;
169 
	:: else -> break
170 
	od;
171 
	skip
172 
}
173 
 
174 
/*
175 
 * If this guy, the highest-numbered proc, sticks
176 
 * around, then everyone else sticks around.
177 
 * This makes sure that we get a state line for
178 
 * everyone in a proc dump.
179 
 */
180 
active proctype dummy()
181 
{
182 
end:	0;
183 
}