diff options
| -rw-r--r-- | sleep1.p | 134 | ||||
| -rwxr-xr-x | spinp | 16 |
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 +} + @@ -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 + |