Import sources from 2011-03-30 iso image

1 files changed, 183 insertions, 0 deletions

diff --git a/sys/src/9/port/semaphore.p b/sys/src/9/port/semaphore.p
new file mode 100755
index 000000000..8284ffd7f
--- /dev/null
+++ b/sys/src/9/port/semaphore.p
@@ -0,0 +1,183 @@
+/*
+spin -a semaphore.p
+pcc -DSAFETY -DREACH -DMEMLIM'='500 -o pan pan.c
+pan -i
+rm pan.* pan
+
+*/
+
+#define N 3
+
+bit listlock;
+byte value;
+bit onlist[N];
+bit waiting[N];
+bit sleeping[N];
+bit acquired[N];
+
+inline lock(x)
+{
+	atomic { x == 0; x = 1 }
+}
+
+inline unlock(x)
+{
+	assert x==1;
+	x = 0
+}
+
+inline sleep(cond)
+{
+	assert !sleeping[_pid];
+	assert !interrupted;
+	if
+	:: cond
+	:: atomic { else -> sleeping[_pid] = 1 } -> 
+		!sleeping[_pid]
+	fi;
+	if
+	:: skip
+	:: interrupted = 1
+	fi
+}
+
+inline wakeup(id)
+{
+	if
+	:: sleeping[id] == 1 -> sleeping[id] = 0
+	:: else
+	fi
+}
+
+inline semqueue()
+{
+	lock(listlock);
+	assert !onlist[_pid];
+	onlist[_pid] = 1;
+	unlock(listlock)
+}
+
+inline semdequeue()
+{
+	lock(listlock);
+	assert onlist[_pid];
+	onlist[_pid] = 0;
+	waiting[_pid] = 0;
+	unlock(listlock)
+}
+
+inline semwakeup(n)
+{
+	byte i, j;
+
+	lock(listlock);
+	i = 0;
+	j = n;
+	do
+	:: (i < N && j > 0) ->
+		if
+		:: onlist[i] && waiting[i] -> 
+			atomic { printf("kicked %d\n", i);
+			waiting[i] = 0 };
+			wakeup(i);
+			j--
+		:: else
+		fi;
+		i++
+	:: else -> break
+	od;
+	/* reset i and j to reduce state space */
+	i = 0;
+	j = 0;
+	unlock(listlock)
+}
+
+inline semrelease(n) 
+{
+	atomic { value = value+n; printf("release %d\n", n); };
+	semwakeup(n)
+}
+
+inline canacquire()
+{
+	atomic { value > 0 -> value--; };
+	acquired[_pid] = 1
+}
+
+#define semawoke() !waiting[_pid]
+
+inline semacquire(block)
+{
+	if
+	:: atomic { canacquire() -> printf("easy acquire\n"); } -> 
+		goto out
+	:: else
+	fi;
+	if
+	:: !block -> goto out
+	:: else
+	fi;
+
+	semqueue();
+	do
+	:: skip ->
+		waiting[_pid] = 1;
+		if
+		:: atomic { canacquire() -> printf("hard acquire\n"); } ->
+			break
+		:: else
+		fi;
+		sleep(semawoke())
+		if
+		:: interrupted -> 
+			printf("%d interrupted\n", _pid);
+			break
+		:: !interrupted
+		fi
+	od;
+	semdequeue();
+	if
+	:: !waiting[_pid] ->
+		semwakeup(1)
+	:: else
+	fi;
+out:
+	assert (!block || interrupted || acquired[_pid]);
+	assert !(interrupted && acquired[_pid]);
+	assert !waiting[_pid];
+	printf("%d done\n", _pid);
+}
+
+active[N] proctype acquire()
+{
+	bit interrupted;
+
+	semacquire(1);
+	printf("%d finished\n", _pid);
+	skip
+}
+
+active proctype release()
+{
+	byte k;
+
+	k = 0;
+	do
+	:: k < N -> 
+		semrelease(1);
+		k++;
+	:: else -> break
+	od;
+	skip
+}
+
+/*
+ * If this guy, the highest-numbered proc, sticks
+ * around, then everyone else sticks around.  
+ * This makes sure that we get a state line for
+ * everyone in a proc dump.  
+ */
+active proctype dummy()
+{
+end:	0;
+}