sleep1.p

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