9.5 Bounded Overtaking

The ticketing scheme ensures that starvation does not occur. However, it does not use the available golf ball resources efficiently. Expert players are kept waiting by novices even though the golf balls they require are available. A modified scheme allows experts to overtake novices but denies starvation by setting an upper bound on the number of times a novice can be overtaken. Once that bound is reached, the novice can no longer be overtaken by an expert and must receive his/her allocation next.

The allocator algorithm for bounded overtaking was implemented but not modeled in the first edition of this book. One of our insightful readers pointed out that adverse scheduling by the Java Virtual Machine could result in the bound being violated. The lesson is clear: models are essential in helping to eliminate errors. Below is a new algorithm which has been carefully modeled to support analysis.

In the algorithm, we need to keep track of those players who have overtaken others. This can be modeled as a set, as shown below. Elements of the set are of type T and can be added, removed and checked for set membership. The set is modeled as the parallel composition of elements which preserve the property that an element is only added if it is not already a member of the set, and only removed if it is a member.

 const False = 0 const True  = 1 range Bool  = 0..1 ELEMENT(Id=0) = IN[False], IN[b:Bool]  = ( add[Id]         -> IN[True]               | remove[Id]      -> IN[False]               | contains[Id][b] -> IN[b]               ).  property   ONEADD(Id=0) = (add[Id]->remove[Id]->ONEADD). ||SET = (forall[i:T] (ELEMENT(i) ||  ONEADD(i))).

We model bounded overtaking using tickets as in the fair FIFO allocator, where ticket numbers are used to indicate the order in which players make their requests. The allocator records which ticket number is next. Overtaking occurs when we allocate balls to a player whose turn – indicated by his/her ticket number – is subsequent to a waiting player with the next ticket. The overtaking player is added to the overtaking set, and a count ot is incremented to indicate the number of times next has been overtaken. When the count equals the bound, we allow allocation to the next player only. When allocation is made to the next player, we need to update next to indicate the next (waiting) player. We skip the ticket numbers of those overtaking players who have already received their allocation, remove each of these intervening players from the overtaking set and decrement the overtaking count accordingly. This is achieved in the local process, WHILE, in the ALLOCATOR given below. Note that the maximum ticket value must not be less than the sum of the number of players and the bound so as to avoid ambiguity when the sequence of ticket numbers restarts.

 const N  = 5      // maximum #golf balls const Bd = 2      // bound on overtaking range B  = 0..N   // available range const TM = 5 + Bd // maximum ticket range T  = 1..TM  // ticket values TICKET    = TURN[1], TURN[t:T] = (ticket[t]->TURN[t%TM+1]). ALLOCATOR  = BALL[N][1][0], BALL[b:B][next:T][ot:0..Bd] =      (when (b>0 && ot<Bd) get[i:1..b][turn:T] ->           if (turn!=next) then              (add[turn] -> BALL[b-i][next][ot+1])           else               WHILE[b-i][next%TM+1][ot]      |when (b>0 && ot==Bd) get[i:1..b][next] ->              WHILE[b-i][next%TM+1][ot]      |put[j:1..N] -> BALL[b+j][next][ot]      ), WHILE[b:B][next:T][ot:0..Bd] =      (contains[next][yes:Bool] ->           if (yes) then           (remove[next] ->                WHILE[b][next%TM+1][ot-1])           else                BALL[b][next][ot]      )+{add[T],remove[T]}.

The golf club system is now modeled as follows:

 ||GOLFCLUB = (Players:PLAYER             || ALLOCATOR||TICKET||SET             || HANDICAP             )/ {Players.get/get,                Players.put/put,                Players.ticket/ticket}.

Using ProgressCheck, as defined before, no progress violations are detected for this bounded overtaking golf club. Using animation, we can step through to produce a trace which illustrates the bounded allocation algorithm:

 eve.need.4          Novices Eve and Dave dave.need.4 chris.need.1        Experts Alice, Bob and Chris alice.need.1 bob.need.1 alice.ticket.1 alice.get.1.1       Alice gets 1 ball, ticket 1 contains.2.0        Ticket 2 is next bob.ticket.2 bob.get.1.2         Two allocated, three available contains.3.0        Ticket 3 is next dave.ticket.3       Dave needs four balls: waits chris.ticket.4 chris.get.1.4       Chris overtakes add.4 eve.ticket.5        Eve needs four balls: waits alice.put.1 alice.ticket.6 alice.get.1.6       Alice overtakes add.6 bob.put.1 bob.ticket.7 bob.get.1.7         Bob overtakes: bound reached add.7 chris.put.1 chris.ticket.8      Chris waits: three available alice.put.1 alice.ticket.1      Alice waits: four available dave.get.4.3        Dave gets four balls contains.4.1        remove intervening overtaker remove.4 contains.5.0        Ticket 5 (Eve) is next dave.put.4 dave.ticket.2 alice.get.1.1       Alice overtakes: bound reached add.1 bob.put.1 bob.ticket.3 eve.get.4.5         Eve gets four balls contains.6.1        remove intervening overtakers remove.6 contains.7.1 remove.7 contains.8.0        Ticket 8 (Chris) is next ...

We can easily add a safety property BALLS to check that players return the same number of balls as allocated. This is shown below.

 property    BALLS = BALLS[N],    BALLS[b:0..N] =      (when b>0           Players.get[i:1..b][turn:T] -> BALLS[b-i]      |Players.put[j:1..N] -> BALLS[b+j]      ).

Can we also specify the bounded nature of this allocator as a safety property? This requires more ingenuity in which we check, for each player, that he/she is not overtaken more than bound times. Overtaking is indicated by an allocation to another player whose ticket t lies between the turn of the player and the latest ticket issued.

 property    BOUND(P='alice) =      ({Players {[P]}}.ticket[T] -> BOUND      |[P].ticket[t:T]  -> WAITING[t][t][0]      |[Players].get[R][T]       -> BOUND     ),    WAITING[turn:T][latest:T][overtaken:0..Bd] =      ([P].get[b:R][turn] -> BOUND      |{Players\{[P]}}.get[b:R][t:T] ->         if ((t>turn && (t<=latest ||  latest<turn))          || (t<turn && (t<=latest && latest<turn)))           then WAITING[turn][latest][overtaken+1]           else WAITING[turn][latest][overtaken]      |Players.ticket[last:T] ->                 WAITING[turn][last][overtaken]      ).

The golf club system is now modeled as below, where the property is checked for all players. This is a large model of over 4 million states and 10 million transitions. No safety (or progress) violations are found for CHECKGOLFCLUB.

 ||CHECKGOLFCLUB = (GOLFCLUB                   || BALLS                   || forall [p:Players] BOUND(p)                   ).

However, if we check for an overtaken bound of 2 in the property BOUND and leave the allocator with Bd set to 3, then we quickly get the violation below in which Alice is overtaken three times, twice by Bob and once by Chris. This confirms that the property BOUND does indeed detect violations in the overtaking bound.

 Trace to property violation in BOUND(alice):      alice.need.1      alice.ticket.1      bob.need.1      bob.ticket.2      bob.get.1.2      chris.need.1      chris.ticket.3      add.2      bob.put.1      bob.ticket.4      bob.get.1.4      add.4      chris.get.1.3