Mutual Exclusion by Path Compression (Li-Hudak):

Signature :

Output : Send(t)i,j t i Token

Request(r)i,j r i Request

Input : Receive(m)j,i m i {Token, Request}

States :

map ... FIFO queue of directions, initially

empty.

curDir ... current direction, pointer to the node

which has eventually the token.

needToken ... set if the node need's the token for

entering the critical section.

Transitions :

Send_{i, j:=mapi.nextReceiver()}:

precondition : haveToken_i

not needToken_i

j exists

effect :

token.map := map_i;

map_i := new Map();

curDir_i := j;

send Token from process_i to process_j

Receive_{j, i}:

precondition : ---

effect :

if (msg_i is a Token) then

map_i = merge msg_i.map with map_i

haveToken_i := true;

elsif (msg_i is a Request) then

if (curDir_i = i) then

map_i.addReceiver(j);

else

forward msg_i to curDir_i;

curDir_i := j;

end;

end;

Request_{i, j:=curDiri}:

precondition : not haveToken_i

needToken_i

effect :

send new Request from process_i to process_j

curDir_i := i;

Critical_i:

precondition : haveTocken_i

needToken_i

effect :

do something in critical section

needToken_i := false;

Tasks :

{Sent_i,j, Request_i,j, Critical_i | i,j i integer }

{Receive_j,i | i,j i integer }