// ------------------------------------------------------------ // Peterson's EntryProtocol consists of several stages where // a two process solution of Peterson's protocol is implemented // to determine which processes get the advance to the next // stage. // ------------------------------------------------------------ package Communication.MutexProtocols.Peterson; // number of processes macro NumProc = 3; module EntryProtocol(nat{NumProc()} ?i, [NumProc()] nat{NumProc()} prev, level) { for(j=0 .. (NumProc()-2)) { next(level[i]) = j; next(prev[j]) = i; pause; for(k=0 .. (NumProc()-1)) { if(i!=k) // wait if process k is in higher numbered stage // and process i was the last to enter this stage await ((level[k] < level[i]) or (prev[j]!=i) ); } } }