diff options
Diffstat (limited to 'sleep1.p')
-rw-r--r-- | sleep1.p | 134 |
1 files changed, 0 insertions, 134 deletions
diff --git a/sleep1.p b/sleep1.p deleted file mode 100644 index af69772..0000000 --- a/sleep1.p +++ /dev/null @@ -1,134 +0,0 @@ -/* -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 -} - |