9.2 Golf Club Model

9.2 Golf Club Model

In modeling the golf club program, we need only be concerned with the player threads and the allocator monitor that embody the concurrent behavior of the golf club. We can abstract away from the details of how the program’s display interface is constructed. We first model the allocator monitor and then examine the problem of modeling dynamically created threads. The model for the allocator is listed below:

 const N=5    //maximum #golf balls range B=0..N //available range ALLOCATOR = BALL[N], BALL[b:B] = (when (b>0) get[i:1..b]->BALL[b-i]             | put[j:1..N]          ->BALL[b+j]             ).

The ALLOCATOR process initially has N golf balls to allocate. In the state with b golf balls, the process accepts requests for 1..b. In other words, the process blocks requests to get more than b golf balls. The process moves into an ERROR state if more golf balls are put back than were previously requested (i.e. b+j > N). The behavior of ALLOCATOR can be clearly seen in Figure 9.3 where N = 2 to reduce the complexity of the diagram.

Figure 9.3: ALLOCATOR LTS for N = 2.

How do we model the potentially infinite stream of dynamically created player threads? The straightforward answer is that we cannot since this would involve an infinite state space. However, while we cannot model infinite state spaces, we can model infinite behaviors that are repetitive. In the golf club example, we do not need to model the fact that each player thread is distinct. Instead, we model a fixed population of golfers who continuously repeat the actions involved in playing golf – a situation not too far removed from real life! Effectively, our model constrains the maximum number of golfers who are concurrently trying to play golf. The maximum number of active player threads in the program is only constrained by the available storage. Our model generates an infinite stream of requests from a fixed set of golfers while the program generates a stream of requests with each request originating from a new player.

A player is modeled by a process that initially decides the number of golf balls it needs to play golf. Subsequently, the process continuously attempts to get and then put back that number of golf balls. The model for a player process is:

 range R=1..N //request range PLAYER      = (need[b:R]->PLAYER[b]), PLAYER[b:R] = (get[b]->put[b]->PLAYER[b]).

The behavior of PLAYER can be seen in Figure 9.4 where we have again set N = 2 to reduce the complexity of the diagram.

Figure 9.4: PLAYER LTS for N = 2.

We now need to distinguish between expert players and novices. The difference is, of course, that novices require more golf balls than experts. We define an additional process to constrain the numbers of golf balls requested by both novices and experts. We use named label sets to declare the names of players. Sets of labels were first used explicitly in Chapter 4. FSP also allows named sets to be declared as below:

 set Experts = {alice,bob,chris} set Novices = {dave,eve} set Players = {Experts,Novices}

FSP does not support sets of sets, simply sets of labels. Consequently, the set named Players is the union of the sets Experts and Novices. With these declarations, we can define the constraint that distinguishes experts from novices as:

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

The alphabet of the process HANDICAP consists of all the need actions that can be performed by all players. However, it only engages in actions in which experts need one or two golf balls and novices need between three and N golf balls. When composed with the PLAYER processes, HANDICAP inhibits these processes from performing any other need actions. The composition of players, allocator and constraint is described in Figure 9.5.

Figure 9.5: GOLFCLUB composition.

Analysis of the GOLFCLUB model of Figure 9.5 reveals no safety violations. The system is well-behaved in the sense that players return the same number of golf balls they get and consequently the allocator cannot get into the ERROR state. The problem with this system is not safety but liveness. The following progress properties assert for experts and novices that they make progress with respect to getting golf balls.

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

Notice that we have not specified any particular number of golf balls. Getting any number satisfies the property. Similarly, we have not specified a specific novice or expert. Consequently, if any novice regularly gets any number of golf balls, the property NOVICE is satisfied and similarly for experts. A progress check against these properties reveals no violations. To reveal the problem that occurred in the program, we must set up adverse scheduling conditions using the technique described in Chapter 7. We make the put action, which releases golf balls, low priority:

 ||ProgressCheck = GOLFCLUB >>{Players.put[R]}.

Progress analysis of this system detects a violation of the progress property NOVICE. One of the violating traces produced by the analyzer is listed below:

 Progress violation: NOVICE Path to terminal set of states:      alice.need.1      alice.get.1      bob.need.1      bob.get.1      chris.need.1      chris.get.1      dave.need.4      eve.need.4 Actions in terminal set: {alice.get.1, alice.put.1, bob.get.1, bob.put.1, chris.get.1, chris.put.1}

This is the situation in which each of the expert players alice, bob and chris needs a single ball and the novices dave and eve need four. The terminal set indicates an infinite execution, in which the experts repeatedly get and put the golf balls they need. However, novices do not get access because the situation does not occur in which two experts put their golf balls without an intermediate get. Consequently, the allocator never has four golf balls to give to a novice. As in the Java program, experts continuously overtake novices and consequently, the novices make no progress.