// -------------------------------------------------------------------- // This file is the same as Ticket.qrz except that the default is to // use unbounded integers and that the specifications were given in // mu-calculus. // // References: // G.R. Andrews' book, Concurrent Programming, chapter 3.3, 1991 // -------------------------------------------------------------------- package Communication.MutexProtocols.TicketMu; // number of processes macro NumProc = 4; module TicketProtocol (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 int{NumProc()} next_ticket, // ticket to be drawn by next customer int{NumProc()} served_ticket, // ticket number of currently served customer [NumProc()] int{NumProc()} ticket, // tickets already drawn by customers [NumProc()] bool !done, // to check successful termination [NumProc()] bool spin) // to see that process applies for CS { for(i=0 .. (NumProc()-1)) do || suspend loop { pause; EntryProtocol(served_ticket,ticket[i],next_ticket); CriticalSection(leave_cs,crit_var); ExitProtocol(served_ticket,done[i]); } when(go!=i); }satisfies { // ============================================================ MutualExclusive: // ------------------------------------------------------------ // at most one process can enter critical section // ------------------------------------------------------------ assert nu z.( (crit_var<=1) & [] z); // ============================================================ EnterLemma: // ------------------------------------------------------------ // a process will enter its critical section if it currently // is enabled by the scheduler in a stage where it applies // for the critical section and the critical section is free // note that // ------------------------------------------------------------ assert nu z.( forall(i = 0 .. (NumProc()-1)) ( spin[i] & (ticket[i]==served_ticket) & (go==i) -> [] !spin[i] ) & [] z); // ============================================================ NoDeadlock: // ------------------------------------------------------------ // if several processes apply for accessing the critical section // and the critical section is free, then one of them enters it // ------------------------------------------------------------ assert nu z.( ((crit_var == 0) -> forall(i = 0 .. (NumProc()-1)) (spin[i] & (go==i) -> [] (!spin[i] & (crit_var > 0))) ) & [] z); // ============================================================ 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(leave_cs & (go==i))) -> G forall(i = 0 .. (NumProc()-1)) (F done[i]) ); // ============================================================ }