// -------------------------------------------------------------------- // This file implements a simple Mutex protocol that is implemented in // many stores as well. Upon entering the store, a customer draws a // number that is one larger than the number held by any other customer // currently waiting in the shop. The customer then waits until all // customers holding smaller numbers have been serviced. // A problem for the implementation of the protocol on an uniprocessor // is that it requires an atomic Fetch-And-Increment operation in order // to load the value of next_ticket and incrementing it at the same time. // // References: // G.R. Andrews' book, Concurrent Programming, chapter 3.3, 1991 // -------------------------------------------------------------------- package Communication.MutexProtocols.Ticket; // 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 { 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); }