9.3 Fair Allocation

Having successfully detected the liveness problem in the model, the next step is to look at ways of solving the problem and to check that they work correctly in the model. We can then change the program to reflect the updated model. In the model, we could simply increase the number of golf balls with which the allocator is initialized. Since we have a fixed population of golfers, we can easily increase the number such that there is no contention. This would not be a general solution since it would always be possible for expert players to arrive at a faster rate and, as a result, novices would starve. Instead, we arrange it such that players wait in an orderly line for golf balls such that experts cannot overtake novices.

Rather than make players line up in first-in-first-out (FIFO) order, we use a ticketing scheme. New tickets are generated in ascending numerical order. Players take a new ticket from a dispenser when they arrive at the golf club and they are subsequently served with golf balls in ticket order. In the model, we do not require an infinite number of tickets since, as long as we have at least as many tickets as players, we can restart the numbering sequence when the last ticket has been handed out.

The ticket dispenser is modeled by the following process:

 const TM = 5    // maximum ticket range T = 1..TM // ticket values TICKET    = NEXT[1], NEXT[t:T] = (ticket[t]->NEXT[t%TM+1]).

We must modify the PLAYER process to get tickets and modify the ALLOCATOR to only accept requests in ticket order. The modified processes are shown below.

 PLAYER     = (need[b:R]->PLAYER[b]), PLAYER[b:R]= (ticket[t:T]               ->get[b][t]->put[b]->PLAYER[b]). ALLOCATOR      = BALL[N][1], BALL[b:B][t:T] =   (when (b>0) get[i:1..b][t]->BALL[b-i][t%TM+1]   |put[j:1..N]              ->BALL[b+j][t]   ).

The revised PLAYER process requests a ticket and uses it when requesting golf balls i.e. get[b][t]. The revised ALLOCATOR accepts get actions in ticket order starting with ticket number 1. The ticket scheme increases the size of the model considerably. To compensate for the increase, we modify the HANDICAP constraint such that expert players always request a single golf ball and novices request four:

 HANDICAP =      ({Novices.{need[4]},Experts.need[1]}            -> HANDICAP)      +{Players.need[R]}.

The golf club system is now modeled as follows:

 ||GOLFCLUB =(Players:PLAYER              ||Players::(ALLOCATOR||TICKET)              ||HANDICAP              ).

To analyze progress for this system, the progress properties must be slightly revised to take into account the addition of the ticket value in the get action.

 progress NOVICE = {Novices.get[R][T]} progress EXPERT = {Experts.get[R][T]}

Using ProgressCheck, as defined before, no progress violations are detected. The next section discusses the implementation of the revised allocator.