7.2 Single-Lane Bridge Problem


7.2 Single-Lane Bridge Problem

The problem is depicted in Figure 7.4. A bridge over a river is only wide enough to permit a single lane of traffic. Consequently, cars can only move concurrently if they are moving in the same direction. A safety violation occurs if two cars moving in different directions enter the bridge at the same time.

image from book
Figure 7.4: Single-lane bridge.

To clarify the discussion, we refer to cars moving from left to right as red cars and cars moving from right to left as blue cars (see demonstration applet). In our concurrent-programming model, each car is a process and the problem is to ensure that cars moving in different directions cannot concurrently access the shared resource that is the bridge. To make the simulation more realistic, we must also ensure that cars moving in the same direction cannot pass each other.

In the following section, we develop a model of the system and a Java implementation that corresponds to the model. In this section, we are concerned primarily with the safety properties of the problem. Later in the chapter, we will address liveness issues.

7.2.1 Single-Lane Bridge Model

In modeling the single-lane bridge, we use the following constant and range definitions:

 const N = 3    // number of each type of car range T = 0..N // type of car count range ID= 1..N // car identities 

The essence of the problem is access to the bridge, so the only events of interest in which a car participates are entering the bridge and leaving the bridge. Consequently, a car is modeled by a process that repeatedly enters and leaves the bridge:

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

To model the fact that cars cannot pass each other on the bridge, we require the following processes which constrain the order of the enter and exit actions respectively:

 NOPASS1  = C[1], //preserves entry order C[i:ID]  = ([i].enter->C[i%N+1]). NOPASS2  = C[1], //preserves exit order C[i:ID]  = ([i].exit->C[i%N+1]). ||CONVOY = ([ID]:CAR||NOPASS1||NOPASS2).

The CONVOY process models a set of cars traveling in the same direction that enter the bridge one after the other and leave the bridge one after the other. However, it does not stop one car exiting the bridge before the next car enters. The behavior of all cars is captured by the following composition:

 ||CARS = (red:CONVOY || blue:CONVOY).

The remaining entity that must be modeled is the bridge itself. This must constrain CARS so that although one or more cars moving in the same direction may be on the bridge concurrently, cars moving in different directions may not. To enforce this, the bridge maintains a count of blue cars on the bridge and of red cars on the bridge. Red cars are only allowed to enter when the blue count is zero and vice versa. The BRIDGE process is listed below:

 BRIDGE = BRIDGE[0][0], // initially empty BRIDGE[nr:T][nb:T] =   //nr is the red count, nb the blue       (when (nb==0)          red[ID].enter -> BRIDGE[nr+1][nb]       |red[ID].exit    -> BRIDGE[nr-1][nb]       |when (nr==0)          blue[ID].enter-> BRIDGE[nr][nb+1]       |blue[ID].exit   -> BRIDGE[nr][nb-1]       ).

Note that the exit actions of the bridge permit the car counts, nr and nb, to be decremented even though their value is 0. As described in Chapter 5, the FSP compiler in the LTSA tool will automatically map these undefined states to the ERROR state, indicating this by issuing warnings:

 Warning - BRIDGE.-1.0 defined to be ERROR Warning - BRIDGE.0.-1 defined to be ERROR ...

In fact, when BRIDGE is composed with CARS, their behavior prevents cars which have not entered from exiting and the ERROR state is unreachable.

Before describing the overall system composition, we need to specify a safety property to compose with the system that verifies that cars do not collide on the bridge. The required property is listed below. It specifies that while red cars are on the bridge only red cars can enter and while blue cars are on the bridge only blue cars can enter. When the bridge is empty, either a red car or a blue car may enter. The index i is used to count the red (or blue) cars currently on the bridge.

 property ONEWAY =(red[ID].enter   -> RED[1]                  |blue[ID].enter -> BLUE[1]                  ), RED[i:ID] = (red[ID].enter -> RED[i+1]             |when(i==1)red[ID].exit -> ONEWAY             |when(i>1) red[ID].exit -> RED[i-1]             ), BLUE[i:ID]= (blue[ID].enter -> BLUE[i+1]             |when(i==1)blue[ID].exit -> ONEWAY             |when(i>1) blue[ID].exit -> BLUE[i-1]             ).

The entire system can now be modeled by the composite process specified in Figure 7.5.

image from book
Figure 7.5: SingleLaneBridge model.

Safety analysis using LTSA verifies that the ONEWAY safety property is not violated.

However, without the constraints provided by the BRIDGE, the composition (CARS||ONEWAY) yields the following safety violation:

 Trace to property violation in ONEWAY:      red.1.enter      blue.1.enter

7.2.2 Single-Lane Bridge Implementation

In the single-lane bridge problem, it is reasonably clear which are the active entities and which are the passive entities. Cars are implemented as Java threads and the bridge as a monitor. This leaves the model entities NOPASS1 and NOPASS2 concerned with constraining overtaking. These have no explicit representation in the implementation. The overtaking constraint is dealt with in the BridgeCanvas class which displays car movement. Figure 7.6 depicts the class diagram for the program.

image from book
Figure 7.6: Single-lane bridge class diagram.

An instance of the BridgeCanvas class is created by the SingleLaneBridge applet. A reference to it is passed to each newly created RedCar and BlueCar object. The methods provided by the BridgeCanvas class are listed in Program 7.1.

Program 7.1: BridgeCanvas class.

image from book
 class BridgeCanvas extends Canvas {   public void init(int ncars) {...} //set number of cars   //move red car with the identity i astep   //returns true for the period from just before,   // until just after car on bridge   public boolean moveRed(int i)          throws InterruptedException{...}   //move blue car with the identity i astep   //returns true for the period from just before,   //until just after car on bridge   public boolean moveBlue(int i)          throws InterruptedException{...}   public synchronized void freeze(){...} //freeze display   public synchronized void thaw(){...} //unfreeze display }
image from book

The code for the two classes representing cars is listed in Program 7.2. Each car moves until it is about to enter the bridge. It then requests access to the bridge by invoking control.redEnter() if it is a red car and control.blueEnter() if it is blue. When a car has crossed the bridge, it invokes the appropriate Exit method.

Program 7.2: RedCar and BlueCar classes.

image from book
 class RedCar implements Runnable {   BridgeCanvas display; Bridge control; int id;   RedCar(Bridge b, BridgeCanvas d, int id) {     display = d; this.id = id; control = b;   }   public void run() {     try {       while(true) {         while (!display.moveRed(id));            // not on bridge         control.redEnter();           // request access to bridge         while (display.moveRed(id));          // move over bridge         control.redExit();            // release access to bridge       }     } catch (InterruptedException e) {}   } } class BlueCar implements Runnable {   BridgeCanvas display; Bridge control; int id;   BlueCar(Bridge b, BridgeCanvas d, int id) {     display = d; this.id = id; control = b;   }   public void run() {     try {       while (true) {         while (!display.moveBlue(id));            // not on bridge         control.blueEnter();           // request access to bridge         while (display.moveBlue(id));          // move over bridge         control.blueExit();            // release access to bridge       }     } catch (InterruptedException e) {}   } }
image from book

The entry and exit bridge access methods are provided by an instance of the class Bridge or a class derived from Bridge. Class Bridge provides a null implementation as listed in Program 7.3. This enables us to view the results of an unsafe bridge implementation.

Program 7.3: Bridge class.

image from book
 class Bridge {   synchronized void redEnter()    throws InterruptedException {}   synchronized void redExit()  {}   synchronized void blueEnter()    throws InterruptedException {}   synchronized void blueExit() {} }
image from book

The SingleLaneBridge applet class creates one, two or three of each of the red and blue cars depending on which button is clicked. In addition, the check boxes select an implementation of the bridge monitor. Figure 7.7 depicts the consequences of using the null implementation of Program 7.3.

image from book
Figure 7.7: Single-lane bridge display using Bridge class.

Clicking the Safe check box creates a system that avoids the collisions of Figure 7.7. It uses the class SafeBridge which is a direct translation of the BRIDGE process from the model. Each of the guarded actions from the model becomes a conditionally synchronized method. Since this has been modeled and shown to preserve the ONEWAY safety property, we can be reasonably confident in the safety of the SafeBridge implementation. The code for the class is listed in Program 7.4.

Program 7.4: SafeBridge class.

image from book
 class SafeBridge extends Bridge {   private int nred  = 0;  //number of red cars on bridge   private int nblue = 0; //number of blue cars on bridge   //Monitor Invariant: nred0 and nblue0 and   //              not (nred>0 and nblue>0)   synchronized void redEnter()        throws InterruptedException {      while (nblue>0) wait();      ++nred;    }   synchronized void redExit(){       --nred; if (nred==0)notifyAll();    }   synchronized void blueEnter()        throws InterruptedException {      while (nred>0) wait();      ++nblue;    }   synchronized void blueExit(){      --nblue; if (nblue==0)notifyAll();    } }
image from book

The implementation of SafeBridge uses conditional notification. We only wake up waiting threads when the number of cars on the bridge – either red or blue – is decremented to zero. This avoids unnecessary thread switches since otherwise, blue cars would be woken up every time a red car leaves the bridge and vice versa. It is only the last car of a particular color to leave the bridge that should wake up waiting car threads.

SafeBridge ensures that cars do not collide on the bridge; however, it does not ensure that cars eventually get the opportunity to cross the bridge. With three cars of each color, if a red car crosses the bridge first there is always a red car on the bridge and consequently, blue cars never get to cross. This situation is called starvation: a form of liveness property discussed in the next section.




Concurrency(c) State Models & Java Programs
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net