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 }
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.
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).
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.
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.