summaryrefslogtreecommitdiff
path: root/sleep1.p
diff options
context:
space:
mode:
Diffstat (limited to 'sleep1.p')
-rw-r--r--sleep1.p134
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
-}
-