13.5 Readers Writers Example | Concurrency: State Models and Java Programs

13.5 Readers – Writers Example

Program 13.2 reproduces the version of the Readers – Writers program from Chapter 7, Program 7.8 that gives Writers priority. This version is again taken from the first printing, first edition of this book.

Program 13.2: Class ReadWritePriority.

 class ReadWritePriority implements ReadWrite{   private int readers =0;   private boolean writing = false;   private int waitingW = 0; // no of waiting Writers.   public synchronized void acquireRead()              throws InterruptedException {     while (writing || waitingW>0) wait();      ++readers;   }   public synchronized void releaseRead() {     --readers;     if (readers==0) notify();   }   public synchronized void acquireWrite()              throws InterruptedException {     ++waitingW;     while (readers>0 || writing) wait();     --waitingW;     writing = true;   }   public synchronized void releaseWrite() {     writing = false;     notifyAll();   } }

To verify this program, we proceed as before and translate the Java into FSP using the model construction developed in sections 13.2 and 13.3. The first step is to model the state of the monitor. This consists of the wait set, the monitor lock and the variables specific to the ReadWritePriority class. The class has three variables – readers, writing and waitingW – which all play apart in synchronization. Consequently, in this example, we model the state of the monitor by:

 ||RWPRIORMON = ( Threads::LOCK || WAITSET || SAFEMON                ||Threads::( readers:VAR                           ||writing:BOOLVAR                           ||waitingW:VAR                           )                ).

The set Threads is defined by:

 const Nread  = 2                   // #readers const Nwrite = 2                   // #writers set   Read   = {reader[1..Nread]}  // reader threads set   Write  = {writer[1..Nwrite]} // writer threads const Nthread = Nread + Nwrite set   Threads = {Read,Write}

The alphabet that must be added to each monitor method is:

 set ReadWriteAlpha =  {{readers,waitingW}.VarAlpha, writing.BoolAlpha,    LockOps, SyncOps,    acquireRead,acquireWrite,releaseRead,releaseWrite  }

13.5.1 ReadWritePriority Methods

The next step in verifying an implementation is to derive an FSP sequential process for each monitor method. These processes for acquireRead(), releaseRead(), acquireWrite() and releaseWrite() are listed below.

 /* * acquireRead() method */ ACQUIREREAD   = (acquire -> WHILE), WHILE                   // while (writing ———— waitingW>0) wait();   = (writing.read[v:Bool] -> waitingW.read[u:Int] ->      if (v || u>0) then WAIT;WHILE else CONTINUE     ), CONTINUE   = (acquireRead      -> readers.inc           // ++readers;      -> release -> END      ) + ReadWriteAlpha. /* * releaseRead() method */ RELEASEREAD   = (acquire -> releaseRead     -> readers.dec            // --readers;     -> readers.read[v:Int] -> // if (readers==0) notify();        if (v==0) then (notify -> CONTINUE) else CONTINUE      ), CONTINUE   = (release -> END) + ReadWriteAlpha. /* * acquireWrite() method */ ACQUIREWRITE               // ++waitingW;   = (acquire -> waitingW.inc -> WHILE), WHILE                      // while (readers>0 ———— writing) wait();   = (writing.read[b:Bool] -> readers.read[v:Int]->      if (v>0 || b) then WAIT;WHILE else CONTINUE     ), CONTINUE   = (acquireWrite      -> waitingW.dec        // --waitingW;      -> writing.write[True] // writing = true;      -> release -> END     )+ ReadWriteAlpha. /* * releaseWrite() method */ RELEASEWRITE    = (acquire -> releaseWrite      -> writing.write[False] // writing = false;      -> notifyAll            // notifyAll();      -> release-> END      ) + ReadWriteAlpha.

We have included the actions acquireRead, acquireWrite, releaseRead and releaseWrite in the model, which correspond to the actions in the design model of Chapter 7.

READER and WRITER Processes

Models for READER and WRITER processes are listed below. In this case, we have included actions to represent the calling of the monitor method in addition to modeling the execution of the method. We will see in the next section that these actions are needed to define the required progress property analysis conditions.

 READER  = (acquireRead.call -> ACQUIREREAD;READING), READING = (releaseRead.call -> RELEASEREAD;READER). WRITER  = (acquireWrite.call -> ACQUIREWRITE;WRITING), WRITING = (releaseWrite.call -> RELEASEWRITE;WRITER).

13.5.2 Analysis

To verify that the implementation model satisfies the desired safety properties, we use the safety property RW_SAFE originally specified in section 7.5.1 to check the correct behavior of the design model.

 property SAFE_RW   = (acquireRead -> READING[1]     |acquireWrite->WRITING     ), READING[i:1..Nread]   = (acquireRead -> READING[i+1]     |when(i>1)  releaseRead -> READING[i-1]     |when(i==1) releaseRead -> SAFE_RW     ), WRITING = (releaseWrite -> SAFE_RW).

The system we perform safety analysis on consists of the reader and writer threads, the monitor state and the safety property as shown below:

 ||RWSYS = (Read:READER || Write:WRITER           || RWPRIORMON           || Threads::SAFE_RW           ).

Safety analysis detects the following deadlock:

 Trace to DEADLOCK:       reader.1.acquireRead.call       reader.1.acquire       reader.1.writing.read.0       reader.1.waitingW.read.0       reader.1.acquireRead       reader.1.readers.inc       reader.1.release         // reader 1 acquires RW lock       reader.1.releaseRead.call       reader.2.acquireRead.call       writer.1.acquireWrite.call       writer.1.acquire       writer.1.waitingW.inc       writer.1.writing.read.0       writer.1.readers.read.1       writer.1.wait  // writer 1 blocked as reader has RW lock       writer.1.release       reader.2.acquire       reader.2.writing.read.0       reader.2.waitingW.read.1       reader.2.wait  // reader 2 blocked as writer 1 waiting       reader.2.release       writer.2.acquireWrite.call       writer.2.acquire       writer.2.waitingW.inc       writer.2.writing.read.0       writer.2.readers.read.1       writer.2.wait     // writer 2 blocked as reader has RW lock       writer.2.release       reader.1.acquire       reader.1.releaseRead       reader.1.readers.dec       reader.1.readers.read.0       reader.1.notify   // reader 1 releases RW lock & notifies       writer.2.release       reader.1.release       reader.1.acquireRead.call       reader.1.acquire       reader.1.writing.read.0       reader.1.waitingW.read.2       reader.2.unblock  // reader 2 unblocked by notify       reader.1.wait       reader.1.release       reader.2.endwait       reader.2.acquire       reader.2.writing.read.0       reader.2.waitingW.read.2       reader.2.wait     // reader 2 blocks as writers waiting       reader.2.release

The deadlock happens because the notify operation performed by Reader 1 when it releases the read – write lock unblocks another Reader rather than a Writer. This unblocked Reader subsequently blocks again since there are Writers waiting. The solution is again to use a notifyAll to awake all waiting threads and thus permit a Writer to run. Changing the notify action to notifyAll in the RELEASEREAD part of the model and rerunning the safety analysis confirms that the deadlock does not occur and that the implementation model satisfies the safety property.

Why did we not observe this deadlock in the actual implementation of ReadWritePriority when running the demonstration applet? The reason is quite subtle. In most Java Virtual Machines, the set of threads waiting on notification is implemented as a first-in-first-out (FIFO) queue. With this queuing discipline, the deadlock cannot occur as for the second Reader to block, a Writer must have previously blocked. This Writer will be unblocked by the notification when the first Reader releases the read – write lock and, consequently, the deadlock does not occur. However, although the implementation works for some JVMs, it is not guaranteed to work on all JVMs since, as noted earlier, the Java Language Specification specifies only that blocked threads are held in a set. Our implementation would exhibit the deadlock on a JVM that used a stack for the wait set. Consequently, the implementation is clearly erroneous and the notify() in the releaseRead() method should be replaced with notifyAll(). Again the lesson is that notify() should only be used with extreme care! However, it should be noted that the use of notify() in the ReadWriteSafe version of the read – write lock is correct since it is not possible in that implementation to have both Readers and Writers waiting simultaneously.

Progress Analysis

Having demonstrated that the implementation model satisfies the required safety properties, it now remains to show that it exhibits the same progress properties as the design model. These properties assert lack of starvation for acquireRead and acquireWrite actions.

 progress WRITE[i:1..Nwrite] = writer[i].acquireWrite progress READ [i:1..Nwrite] = reader[i].acquireRead

The adverse scheduling conditions needed to check progress in the presence of competition for the read – write lock are arranged by making the actions, representing calls to release read and write access to the lock, low priority:

 ||RWPROGTEST = RWSYS >> {Read.releaseRead.call,                          Write.releaseWrite.call}.

Progress analysis reveals that the RWPROGTEST system satisfies the WRITE progress properties but violates the READ progress properties. In other words, the Writers priority implementation of the read – write lock satisfies its design goal of avoiding Writer starvation, but, as with the design model, it permits Reader starvation.