/*
spin -a semaphore.p
pcc -DSAFETY -DREACH -DMEMLIM'='500 -o pan pan.c
pan -i
rm pan.* pan

*/

#define N 3

bit listlock;
byte value;
bit onlist[N];
bit waiting[N];
bit sleeping[N];
bit acquired[N];

inline lock(x)
{
	atomic { x == 0; x = 1 }
}

inline unlock(x)
{
	assert x==1;
	x = 0
}

inline sleep(cond)
{
	assert !sleeping[_pid];
	assert !interrupted;
	if
	:: cond
	:: atomic { else -> sleeping[_pid] = 1 } -> 
		!sleeping[_pid]
	fi;
	if
	:: skip
	:: interrupted = 1
	fi
}

inline wakeup(id)
{
	if
	:: sleeping[id] == 1 -> sleeping[id] = 0
	:: else
	fi
}

inline semqueue()
{
	lock(listlock);
	assert !onlist[_pid];
	onlist[_pid] = 1;
	unlock(listlock)
}

inline semdequeue()
{
	lock(listlock);
	assert onlist[_pid];
	onlist[_pid] = 0;
	waiting[_pid] = 0;
	unlock(listlock)
}

inline semwakeup(n)
{
	byte i, j;

	lock(listlock);
	i = 0;
	j = n;
	do
	:: (i < N && j > 0) ->
		if
		:: onlist[i] && waiting[i] -> 
			atomic { printf("kicked %d\n", i);
			waiting[i] = 0 };
			wakeup(i);
			j--
		:: else
		fi;
		i++
	:: else -> break
	od;
	/* reset i and j to reduce state space */
	i = 0;
	j = 0;
	unlock(listlock)
}

inline semrelease(n) 
{
	atomic { value = value+n; printf("release %d\n", n); };
	semwakeup(n)
}

inline canacquire()
{
	atomic { value > 0 -> value--; };
	acquired[_pid] = 1
}

#define semawoke() !waiting[_pid]

inline semacquire(block)
{
	if
	:: atomic { canacquire() -> printf("easy acquire\n"); } -> 
		goto out
	:: else
	fi;
	if
	:: !block -> goto out
	:: else
	fi;

	semqueue();
	do
	:: skip ->
		waiting[_pid] = 1;
		if
		:: atomic { canacquire() -> printf("hard acquire\n"); } ->
			break
		:: else
		fi;
		sleep(semawoke())
		if
		:: interrupted -> 
			printf("%d interrupted\n", _pid);
			break
		:: !interrupted
		fi
	od;
	semdequeue();
	if
	:: !waiting[_pid] ->
		semwakeup(1)
	:: else
	fi;
out:
	assert (!block || interrupted || acquired[_pid]);
	assert !(interrupted && acquired[_pid]);
	assert !waiting[_pid];
	printf("%d done\n", _pid);
}

active[N] proctype acquire()
{
	bit interrupted;

	semacquire(1);
	printf("%d finished\n", _pid);
	skip
}

active proctype release()
{
	byte k;

	k = 0;
	do
	:: k < N -> 
		semrelease(1);
		k++;
	:: else -> break
	od;
	skip
}

/*
 * If this guy, the highest-numbered proc, sticks
 * around, then everyone else sticks around.  
 * This makes sure that we get a state line for
 * everyone in a proc dump.  
 */
active proctype dummy()
{
end:	0;
}