// ------------------------------------------------------------ // Fischer's EntryProtocol consists of waiting until the lock // variable holds no process id. Then, the process id of the // own process is assigned. If after the assignment lock has // still this value, the process can enter the critical section, // otherwise another process wrote its process id in the lock // after this process has done this and before this process has // left the EntryProtocol. // ------------------------------------------------------------ package Communication.MutexProtocols.Fischer; macro NumProc = 5; module EntryProtocol(nat{NumProc()} ?process_id, lock) { do { await(lock==0); next(lock) = process_id; pause; } while(lock != process_id); }