xv6-cs450/sleep1.p
rsc 949352af66 Model verifying that wakeup really
can be called after release without
causing deadlock.
2007-10-12 04:21:04 +00:00

134 lines
1.9 KiB
OpenEdge ABL

/*
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
}