swap.pml

// tjadam, jawaterm
// 2014.3.18
// Group Assignment 1, parallel swapping

#define N 4;  // number of cells and swappers
byte A[4];
bool lock[4];
chan finished = [4] of {byte};
bool safe = true;

proctype swapper(byte index) {
	// select a random number, bound by N-1 steps, the max index of A
	byte random = 0;
	do
		:: random +1 < N -> random++
		:: break
	od;
	
	// wait until both locks are open, and lock both atomically.
	//   this can't be solved with an oddball swapper because a deadlock
	//   could form between ANY two or more processes.
waitlock:
	atomic{
		if
			:: !lock[index] && !lock[random] ->	lock[index] = true;
												lock[random] = true;
												goto locked
			:: else -> goto waitlock
		fi;
	}

locked: skip;
	// perform swap, unlock both
	byte temp = A[random];
	A[random] = A[index];
	A[index] = temp;
	atomic{
		lock[index] = false;
		lock[random] = false;
	}

	finished ! index;
end:
}

init {
	// fill array with 1..n
	byte i = 0;
	do
		:: i < N ->	A[i] = i + 1;
					lock[i] = false;
					i++;
		:: else -> break
	od;
	// start n swappers
	i = 0;
	do
		:: i < N ->	run swapper(i);
					i++
		:: else -> break
	od;

	// wait for swappers to finish
	byte temp, x = 0;
	do
		:: x < N -> finished ? temp;
					x++
		:: x == N -> break
	od;

	// check safety property, store result in bool safe
	byte y = 0;
	x = 0;
	do
		:: x == N -> break
		:: y == N -> safe = false;
					 break
		:: A[y] == x + 1 && x < N -> y = 0;
									 x++
		:: A[y] != x + 1 && x < N -> y++
	od;
}

ltl liveness { <> swapper@end};
ltl safety   { [] safe };