/*************************************************************************** * * Copyright (c) 1998 * by Helsinki University of Technology, Digital Systems Laboratory. * All rights reserved. * * Author of ticketme.net: Keijo Heljanko * * Current version: * $Id$ * * Description: * This is a version of the TicketME algorithm for solving * the mutual exclusion problem. * * Note! This is the home exercise version which might * not be 100% correct! So don't use the algorithm * here for anything. * * * Version history: * $Log$ ***************************************************************************/ /* Number of processes in the mutex algorithm. */ #define n 3 /* Process identifiers are from min_proc to max_proc. */ #define min_proc 0 #define max_proc ((n)-1) /* Addition modulo n. */ #define INC(x) (((x) + 1) % n) /* Program counter values. (PROD speciality: leave_exit < rem.) */ #enum rem, enter, test, leave_try, crit, reset, leave_exit /* Special value used in ticket variable. */ #define no_val (n) /* Global shared variable pair. (Accessed atomically.) */ #place next_granted lo(<.min_proc,min_proc.>) \ hi(<.max_proc,max_proc.>) \ mk(<.min_proc,min_proc.>) /* Program counter pc for each process. */ #place pc lo(<.min_proc,leave_exit.>) \ hi(<.max_proc,rem.>) \ mk(<.min_proc..max_proc,rem.>) /* Local variable ticket for each process. */ #place vars lo(<.min_proc,0.>) \ hi(<.max_proc,no_val.>) \ mk(<.min_proc..max_proc,no_val.>) /* Decide to enter critical section. */ #trans try in { pc: <.i,rem.>; } out { pc: <.i,enter.>; } #endtr /* Enter the critical section by getting a ticket and checking if we can get in. */ #trans enter in { pc: <.i,enter.>; vars: <.i,ticket.>; next_granted: <.next,granted.>; } out { pc: (next == granted) <.i,leave_try.> + (next != granted) <.i,test.>; vars: <.i,next.>; next_granted: <.INC(next),granted.>; } #endtr /* Spin until the ticket has been granted. */ #trans test in { pc: <.i,test.>; vars: <.i,ticket.>; next_granted: <.next,granted.>; } out { pc: (ticket == granted) <.i,leave_try.> + (ticket != granted) <.i,test.>; vars: <.i,ticket.>; next_granted: <.next,granted.>; } #endtr /* Go to critical section. */ #trans leave_try in { pc: <.i,leave_try.>; } out { pc: <.i,crit.>; } #endtr /* Enter the exit section. */ #trans exit in { pc: <.i,crit.>; } out { pc: <.i,reset.>; } #endtr /* Do the exit. */ #trans reset in { pc: <.i,reset.>; vars: <.i,ticket.>; next_granted: <.next,granted.>; } out { pc: <.i,leave_exit.>; vars: <.i,no_val.>; next_granted: <.next,INC(granted).>; } #endtr /* Leave the exit section. */ #trans rem in { pc: <.i,leave_exit.>; } out { pc: <.i,rem.>; } #endtr