// -------------------------------------------------------------------- // This file implements Peterson's Mutex protocol that is also known // as the Tie-Breaker algorithm. In contrast to SpinLocks, Peterson's // protocol is fair, provided that all processes eventually leave the // critical section after they entered it, and provided that the // scheduler enables every process infinitely often. // // References: // G.R. Andrews' book, Concurrent Programming, Chapter 3.2, 1991 // -------------------------------------------------------------------- package Communication.MutexProtocols.Peterson; // number of processes macro NumProc = 3; module PetersonMutexProtocol (event ?leave_cs, // instructs to leave the critical section nat{NumProc()} ?go, // used to control interleaved execution nat{4} crit_var, // shared variable used in critic section [NumProc()] bool done, // to check successful termination [NumProc()] nat{NumProc()} prev, [NumProc()] nat{NumProc()} level) { crit_var = 0; for(i=0 .. (NumProc()-1)) do || suspend loop { EntryProtocol(i,prev,level); CriticalSection(leave_cs,crit_var); ExitProtocol(done[i],level[i]); } when(go!=i); }satisfies { // ============================================================ Reactive: // ------------------------------------------------------------ // all initial states have at least one infinite path // ------------------------------------------------------------ assert nu z. <> z; // ============================================================ MutualExclusive: // ------------------------------------------------------------ // at most one process can enter critical section // ------------------------------------------------------------ assert A G (crit_var<=1); // ============================================================ EventualEntry: // ------------------------------------------------------------ // fairness is very hard to achieve: it only holds if the // scheduler does not always choose the same process out of // the processes that are applying for the critical section // ------------------------------------------------------------ assert A ( (G forall(i=0 .. (NumProc()-1)) F((level[i]>0) & (go==i))) -> G forall(i=0 .. (NumProc()-1)) F done[i] ); // ============================================================ }