DAJ - Li, Hudak - path compression
algorithm 2000-06-19 (
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 :
Sendi, j:=mapi.nextReceiver():
precondition : haveTokeni
not needTokeni
j exists
effect :
token.map := mapi;
mapi := new Map();
curDiri := j;
send Token from processi to processj
Receivej, i:
precondition : ---
effect :
if (msgi is a Token) then
mapi = merge msgi.map with mapi
haveTokeni := true;
elsif (msgi is a Request) then
if (curDiri = i) then
mapi.addReceiver(j);
else
forward msgi to curDiri;
curDiri := j;
end;
end;
Requesti, j:=curDiri:
precondition : not haveTokeni
needTokeni
effect :
send new Request from processi to processj
curDiri := i;
Criticali:
precondition : haveTockeni
needTokeni
effect :
do something in critical section
needTokeni := false;
Tasks :
{Senti,j, Requesti,j, Criticali | i,j i integer }
{Receivej,i | i,j i integer }