// -------------------------------------------------------------------- // // This file implements Fischer's protocol which is used to control // // mutual exclusive access of NumProc processes to a shared ressource. // // In the Quartz module below, we use a shared variable crit_var that // // is incremented and afterwards decremented during such an access of // // one process. Hence, the variable should be invariantly zero or one. // // The protocol goes back to Lamport and Fischer, and works as // // follows: Each thread has a unique process identifier i, which is a // // positive number. The access to the critical section is controlled // // via a lock variable that either holds an id of a process or is zero. // // The former is the case if a process has obtained access to the // // shared resource. // // -------------------------------------------------------------------- // package Communication.MutexProtocols.Fischer; macro NumProc = 5; module FischerMutex (event ?leave_cs, // instructs to leave the critical section nat{NumProc()} ?go, // used to control interleaved execution nat{NumProc()} lock, // lock variable holding process ids nat{4} crit_var, // shared variable used in critic section [NumProc()] bool done) // to check successful termination { for(i=1 .. (NumProc()-1)) suspend loop { EntryProtocol(i,lock); CriticalSection(leave_cs,crit_var); ExitProtocol(done[i],lock); } when(go!=i); } satisfies { // ============================================================ MutualExclusive: // ------------------------------------------------------------ // at most one process can enter critical section // ------------------------------------------------------------ assert A G (crit_var<=1); // ============================================================ EventualEntry: // ------------------------------------------------------------ // fairness is very hard to achieve in Fischer's protocol; // as the specification below shows, it may even happen // that none of the processes will eventually enter the // critical section, which makes the protocol impractical // ------------------------------------------------------------ assert E G forall(i=0 .. (NumProc()-1)) !done[i]; // ============================================================ }