7.4 Liveness of the Single-Lane Bridge

7.4 Liveness of the Single-Lane Bridge

Using progress properties and action priorities, we are now in a position to investigate the liveness problems of the single-lane bridge. In particular, we are interested in the following two progress properties when the bridge is heavily loaded or congested.

 progress BLUECROSS = {blue[ID].enter} progress REDCROSS = {red[ID].enter}

BLUECROSS asserts that it is always the case that one of the blue cars will be able to enter the bridge; REDCROSS asserts the same for red cars. This leaves the problem of how to model congestion using action priority. If we give all the actions related to red cars priority over blue cars we get the situation where BLUECROSS is violated and similarly if we give blue cars priority REDCROSS is violated. Neither of these scheduling policies is a good model of the program. Neither red nor blue cars have priority in the implementation. Instead, we give car exit from the bridge low priority. This models the situation where the bridge is congested since in any choice between another car entering the bridge and a car leaving the bridge, we choose to let a car enter. The congested bridge is modeled by:

 ||CongestedBridge = (SingleLaneBridge)                     >>{red[ID].exit,blue[ID].exit}.

Progress analysis of this system against the properties BLUECROSS and REDCROSS produces the following output:

 Progress violation: BLUECROSS Path to terminal set of states:      red.1.enter      red.2.enter Actions in terminal set: {red.1.enter, red1.exit, red.2.enter, red.2.exit, red.3.enter, red.3.exit} Progress violation: REDCROSS Path to terminal set of states:      blue.1.enter      blue.2.enter Actions in terminal set: {blue.1.enter, blue.1.exit, blue.2.enter, blue.2.exit, blue.3.enter, blue.3.exit}

The output corresponds with observations of the program. When there are three cars and a red car enters first then the bridge is continuously occupied by red cars and blue cars never cross. Similarly, red cars never cross if a blue car enters first. However, the model abstracts from a number of program details such as the length of the bridge and consequently, the number of cars needed to continuously occupy it. As a result, the model detects lack of progress when there are only two cars moving in each direction. The terminal sets of states for this scenario can clearly be seen in the transition system depicted in Figure 7.11.

Figure 7.11: CongestedBridge model with two cars.

When there is only one car moving in each direction, the bridge does not become congested and both red and blue cars make progress. The transition system for the one car scenario is depicted in Figure 7.12.

Figure 7.12: CongestedBridge model with one car.

Will we receive the same progress results if we instead model congestion by giving car entry to the bridge high priority? The interested reader should check that this is indeed the case.

What we must now do is devise a model which does not exhibit progress problems when there is more than one car moving in each direction.

7.4.1 Revised Single-Lane Bridge Model

A bridge which decides dynamically at any given point whether to admit blue cars or red cars needs to have more information about the state of cars than is currently available in the model. In particular, the bridge needs to know whether cars are waiting to cross. To this end, the model for a car is modified so that it requests access to the bridge before attempting to enter. The revised model for a car is:

 CAR = (request->enter->exit->CAR).

The bridge model can now count the number of cars waiting at each end. The count is incremented when a car requests access and decremented when the car enters the bridge. Our first attempt at a revised BRIDGE process uses this count of waiting cars as follows. Red cars are only allowed to enter the bridge if there are no blue cars on the bridge and there are no blue cars waiting. Blue cars are only allowed to enter the bridge if there are no red cars on the bridge and no red cars waiting to enter the bridge. The revised BRIDGE process is as follows:

 /* nr - number of red cars on the bridge    nb - number of blue cars on the bridge    wr - number of red cars waiting to enter    wb - number of blue cars waiting to enter */ BRIDGE = BRIDGE[0][0][0][0], BRIDGE[nr:T][nb:T][wr:T][wb:T] =   (red[ID].request  -> BRIDGE[nr][nb][wr+1][wb]   |when (nb==0 && wb==0)     red[ID].enter   -> BRIDGE[nr+1][nb][wr-1][wb]   |red[ID].exit     -> BRIDGE[nr-1][nb][wr][wb]   |blue[ID].request -> BRIDGE[nr][nb][wr][wb+1]   |when (nr==0 && wr==0)     blue[ID].enter  -> BRIDGE[nr][nb+1][wr][wb-1]   |blue[ID].exit    -> BRIDGE[nr][nb-1][wr][wb]   ).

The problem with this model is that when we check the safety properties of the new SingleLaneBridge system, a deadlock is reported:

 Trace to DEADLOCK:       red.1.request       red.2.request       red.3.request       blue.1.request       blue.2.request       blue.3.request

The trace is the scenario in which there are cars waiting at both ends, and consequently, the bridge does not allow either red or blue cars to enter. To solve this problem, we must introduce some asymmetry into the problem (as was done for the Dining Philosophers in Chapter 6). This takes the form of a boolean variable (bt) which indicates whether it is the turn of blue cars or red cars to enter the bridge. Initially, bt is set to true indicating it is blue’s turn. As soon as a blue car exits the bridge, bt is set to false. When a red car exits, bt is set to true again. The BRIDGE process becomes:

 const True = 1 const False = 0 range B = False..True /* nr - number of red cars on the bridge    nb - number of blue cars on the bridge    wr - number of red cars waiting to enter    wb - number of blue cars waiting to enter    bt - true indicates blue turn,         false indicates red turn */ BRIDGE = BRIDGE[0][0][0][0][True], BRIDGE[nr:T][nb:T][wr:T][wb:T][bt:B] =   (red[ID].request ->BRIDGE[nr][nb][wr+1][wb][bt]   |when (nb==0 && (wb==0||!bt))     red[ID].enter  ->BRIDGE[nr+1][nb][wr-1][wb][bt]   |red[ID].exit    ->BRIDGE[nr-1][nb][wr][wb][True]   |blue[ID].request->BRIDGE[nr][nb][wr][wb+1][bt]   |when (nr==0 && (wr==0||bt))     blue[ID].enter ->BRIDGE[nr][nb+1][wr][wb-1][bt]   |blue[ID].exit   ->BRIDGE[nr][nb-1][wr][wb][False] ).

The condition under which the bridge permits a red car to enter is that there are no blue cars on the bridge and either there are no blue cars waiting or it is not blue’s turn: nb==0 &&(wb==0 || !bt). The condition for a blue car to enter is that there are no red cars on the bridge and either there are no red cars waiting or it is blue’s turn: nr==0 &&(wr==0 || bt).

This corrected model no longer deadlocks. Further, a progress analysis reports that BLUECROSS and REDCROSS properties are not violated.

7.4.2 Revised Single-Lane Bridge Implementation

The revision to the program involves a new version of the bridge monitor which implements precisely the BRIDGE process from the model developed in the last section. In fact, we do not need to introduce a new monitor method to implement the request action made by cars. The existing enter methods can be modified to increment a wait count before testing whether or not the caller can access the bridge. As before, the tests are simply the negation of the guards in the model BRIDGE process. The new implementation is listed in Program 7.5.

Program 7.5: FairBridge class.

 class FairBridge extends Bridge {   private int nred = 0;  //count of red cars on the bridge   private int nblue = 0;  //count of blue cars on the bridge   private int waitblue = 0;    //count of waiting blue cars   private int waitred = 0;     //count of waiting red cars   private boolean blueturn = true;   synchronized void redEnter()       throws InterruptedException {     ++waitred;     while (nblue>0||(waitblue>0 && blueturn)) wait();     --waitred;     ++nred;   }   synchronized void redExit(){     --nred;     blueturn = true;     if (nred==0)notifyAll();   }   synchronized void blueEnter(){       throws InterruptedException {     ++waitblue;     while (nred>0||(waitred>0 && !blueturn)) wait();     --waitblue;     ++nblue;   }   synchronized void blueExit(){     --nblue;     blueturn = false;     if (nblue==0) notifyAll();   } }

In the demonstration applet, this implementation of the monitor is used when the Fair check box is clicked.