summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorrsc <rsc>2007-10-12 04:21:04 +0000
committerrsc <rsc>2007-10-12 04:21:04 +0000
commit949352af6695cfbfc91a5c0e24ddae95c497b008 (patch)
tree8c71eb07cff4d0e226639de07ef9d343b8d594e5
parent943fd378a1324ca60da72b271769fea4a86e36cb (diff)
downloadxv6-labs-949352af6695cfbfc91a5c0e24ddae95c497b008.tar.gz
xv6-labs-949352af6695cfbfc91a5c0e24ddae95c497b008.tar.bz2
xv6-labs-949352af6695cfbfc91a5c0e24ddae95c497b008.zip
Model verifying that wakeup really
can be called after release without causing deadlock.
-rw-r--r--sleep1.p134
-rwxr-xr-xspinp16
2 files changed, 150 insertions, 0 deletions
diff --git a/sleep1.p b/sleep1.p
new file mode 100644
index 0000000..af69772
--- /dev/null
+++ b/sleep1.p
@@ -0,0 +1,134 @@
+/*
+This file defines a Promela model for xv6's
+acquire, release, sleep, and wakeup, along with
+a model of a simple producer/consumer queue.
+
+To run:
+ spinp sleep1.p
+
+(You may need to install Spin, available at http://spinroot.com/.)
+
+After a successful run spin prints something like:
+
+ unreached in proctype consumer
+ (0 of 37 states)
+ unreached in proctype producer
+ (0 of 23 states)
+
+After an unsuccessful run, the spinp script prints
+an execution trace that causes a deadlock.
+
+The safe body of producer reads:
+
+ acquire(lk);
+ x = value; value = x + 1; x = 0;
+ wakeup(0);
+ release(lk);
+ i = i + 1;
+
+If this is changed to:
+
+ x = value; value = x + 1; x = 0;
+ acquire(lk);
+ wakeup(0);
+ release(lk);
+ i = i + 1;
+
+then a deadlock can happen, because the non-atomic
+increment of value conflicts with the non-atomic
+decrement in consumer, causing value to have a bad value.
+Try this.
+
+If it is changed to:
+
+ acquire(lk);
+ x = value; value = x + 1; x = 0;
+ release(lk);
+ wakeup(0);
+ i = i + 1;
+
+then nothing bad happens: it is okay to wakeup after release
+instead of before, although it seems morally wrong.
+*/
+
+#define ITER 4
+#define N 2
+
+bit lk;
+byte value;
+bit sleeping[N];
+
+inline acquire(x)
+{
+ atomic { x == 0; x = 1 }
+}
+
+inline release(x)
+{
+ assert x==1;
+ x = 0
+}
+
+inline sleep(cond, lk)
+{
+ assert !sleeping[_pid];
+ if
+ :: cond ->
+ skip
+ :: else ->
+ atomic { release(lk); sleeping[_pid] = 1 };
+ sleeping[_pid] == 0;
+ acquire(lk)
+ fi
+}
+
+inline wakeup()
+{
+ w = 0;
+ do
+ :: w < N ->
+ sleeping[w] = 0;
+ w = w + 1
+ :: else ->
+ break
+ od
+}
+
+active[N] proctype consumer()
+{
+ byte i, x;
+
+ i = 0;
+ do
+ :: i < ITER ->
+ acquire(lk);
+ sleep(value > 0, lk);
+ x = value; value = x - 1; x = 0;
+ release(lk);
+ i = i + 1;
+ :: else ->
+ break
+ od;
+ i = 0;
+ skip
+}
+
+active[N] proctype producer()
+{
+ byte i, x, w;
+
+ i = 0;
+ do
+ :: i < ITER ->
+ acquire(lk);
+ x = value; value = x + 1; x = 0;
+ release(lk);
+ wakeup();
+ i = i + 1;
+ :: else ->
+ break
+ od;
+ i = 0;
+ skip
+}
+
diff --git a/spinp b/spinp
new file mode 100755
index 0000000..db9614b
--- /dev/null
+++ b/spinp
@@ -0,0 +1,16 @@
+#!/bin/sh
+
+if [ $# != 1 ] || [ ! -f "$1" ]; then
+ echo 'usage: spinp file.p' 1>&2
+ exit 1
+fi
+
+rm -f $1.trail
+spin -a $1 || exit 1
+cc -DSAFETY -DREACH -DMEMLIM=500 -o pan pan.c
+pan -i
+rm pan.* pan
+if [ -f $1.trail ]; then
+ spin -t -p $1
+fi
+