7.5 ReadersWriters Problem

7.5 Readers–Writers Problem

The Readers–Writers problem is concerned with access to a shared database by two kinds of processes. Readers execute transactions that examine the database while Writers both examine and update the database. For the database to be updated correctly, Writers must have exclusive access to the database while they are updating it. If no Writer is accessing the database, any number of Readers may concurrently access it. In this section, we develop a solution to the problem. As usual, we construct a model of the problem to examine its safety and liveness properties before proceeding to an implementation.

7.5.1 Readers–Writers Model

In modeling the problem, the first step is to decide on the actions of interest. These are acquiring and releasing read access to the shared database and acquiring and releasing write access. The actions are declared below as the set Actions:

 set Actions = {acquireRead,releaseRead,                acquireWrite,releaseWrite}

As for the Ornamental Garden model in section 4.1.2, we use a set constant simply as a way of abbreviating the model description. The processes that model Readers and Writers are:

 READER =   (acquireRead->examine->releaseRead->READER)   +Actions   \ {examine}. WRITER =   (acquireWrite->modify->releaseWrite->WRITER)   +Actions   \ {modify}.

A READER process must acquire read access before examining the database and a WRITER must acquire write access before modifying the database. The alphabets of both processes have been defined to be the full set of access actions by the alphabet extension +Actions. This ensures that while a READER only engages in the acquireRead and releaseRead actions, the acquireWrite and releaseWrite actions cannot occur freely for any prefixed instance of the process. Similarly, for WRITER processes, the acquireRead and releaseRead actions cannot occur freely. The examine and modify actions are hidden since they are irrelevant to the problem of synchronizing access to the shared database.

Access to the shared database is controlled by a read/write lock. The lock accepts acquireRead actions when it has not been acquired for write access by acquireWrite. It permits only a single write access when it has not been acquired for read access. The lock is modeled by the RW_LOCK process:

 const False = 0   const True = 1 range Bool  = False..True const Nread = 2           // Maximum readers const Nwrite= 2           // Maximum writers RW_LOCK = RW[0][False], RW[readers:0..Nread][writing:Bool] =       (when (!writing)          acquireRead ->RW[readers+1][writing]       |releaseRead   ->RW[readers-1][writing]       |when (readers==0 && !writing)          acquireWrite->RW[readers][True]       |releaseWrite  ->RW[readers][False]       ).

The RW_LOCK process maintains a count of the number of concurrent read accesses (readers) and a boolean (writing) which is set to true when the lock is acquired for write access. The action to acquire read access is only accepted when writing is false and the action to acquire write access is only accepted when readers==0 and writing is false.

Safety Property

To check that the lock behaves as desired, we define a safety property, RW_SAFE, as follows:

 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 property asserts that initially either an acquireRead action or a acquireWrite action can be accepted. In other words when the lock is free, it can be acquired for either read or write access. When acquired for read access (READING), further acquireRead actions are permitted but no acquireWrite actions. The lock does not become free until all the releaseRead actions which correspond to the acquireRead actions have happened. When the lock has been acquired for write access (WRITING), only the releaseWrite action should occur. To check that the lock implementation RW_LOCK satisfies the property, the lock is composed with the property as follows:

 ||READWRITELOCK = (RW_LOCK || SAFE_RW).

The resulting LTS is depicted in Figure 7.13.

Figure 7.13: READWRITELOCK LTS.

The transitions to the ERROR state in Figure 7.13 occur if a Reader or Writer is badly behaved. For example, if a Reader performs a releaseRead without previously having performed an acquireRead then a safety violation will occur. A violation will also occur if more than two acquireRead requests are made.

The composition of READER and WRITER processes with the read/write lock is described in Figure 7.14. Analysis of this system reveals no deadlocks or safety violations. The addition of well-behaved READER and WRITER processes ensures that the error transitions of Figure 7.13 cannot occur.

Figure 7.14: READERS_WRITERS model.

Progress Property

The progress properties that are important in the Readers–Writers system are that both Readers and Writers should eventually acquire access to the shared database. We can express the required progress properties as follows:

 progress WRITE = {writer[1..Nwrite].acquireWrite} progress READ  = {reader[1..Nread].acquireRead}

The WRITE property asserts that it should always be the case that at least one of the WRITER processes can perform an acquireWrite action. Since WRITER sare completely symmetric, we can reasonably expect that if one can acquireWrite then so can the others. READ specifies the same property for READER processes and acquireRead. A progress check reports no violations of these properties in the system specified by READERS_WRITERS. Because of the fair choice assumption, progress problems only occur in complete system models that are erroneous. To find how the system performs when loaded or “stressed”, we must specify adverse scheduling conditions using action priority. This is exactly the procedure we adopted to find the progress problems in the single-lane bridge model. Indeed, the adverse conditions are similar to those used in the bridge problem. To model a heavily loaded system, we give lower priority to release actions in the same way we gave lower priority to exit actions in the bridge problem. (Alternatively, we could give higher priority to the acquire actions.) The system model used for progress analysis is described by:

 ||RW_PROGRESS = READERS_WRITERS                 >>{reader[1..Nread].releaseRead,                    writer[1..Nread].releaseWrite}.

Analysis of this system leads to the violation:

 Progress violation: WRITE Path to terminal set of states:      reader.1.acquireRead Actions in terminal set: {reader.1.acquireRead, reader.1.releaseRead,  reader.2.acquireRead, reader.2.releaseRead}

The violation describes the scenario in which Writers cannot access the shared database because a Reader always has read access. In other words, the number of Readers never drops to zero and consequently, the read/write lock denies access to Writers. The terminal set of states that describes this behavior can clearly be seen in Figure 7.15. It contains the states numbered 3, 4 and 5. Before exploring solutions to this progress problem, we translate the existing model into an implementation in the next section.

Figure 7.15: RW_PROGRESS LTS.

7.5.2 Readers–Writers Implementation

In the interests of brevity, we describe only the monitor that synchronizes the accesses of Readers and Writers to a shared database. This synchronization is the essence of the problem. In the same way that we defined the set of actions of interest in the Readers–Writers model, we define an interface that identifies the monitor methods that must be implemented. In the sections that follow, we develop a number of alternative implementations of this interface. The interface is listed in Program 7.6.

Program 7.6: ReadWrite interface.

 interface ReadWrite {      public void acquireRead()          throws InterruptedException;      public void releaseRead();      public void acquireWrite()         throws InterruptedException;      public void releaseWrite(); }

Each method in the ReadWrite interface corresponds directly to the action of the same name in the model. Our first implementation of ReadWrite, which corresponds exactly to the RW_LOCK process from the model, is listed in Program 7.7.

Program 7.7: ReadWriteSafe class.

 class ReadWriteSafe implements ReadWrite {   private int readers =0;   private boolean writing = false;   public synchronized void acquireRead()              throws InterruptedException {     while (writing) wait();     ++readers;   }   public synchronized void releaseRead() {     --readers;     if(readers==0) notify();   }   public synchronized void acquireWrite()               throws InterruptedException {     while (readers>0 || writing) wait();     writing = true;   }   public synchronized void releaseWrite() {     writing = false;     notifyAll();   } }

The guarded actions from the model become synchronized methods containing waits. However, in the implementation, we must decide on notification to awake threads blocked in waits. The simple solution, as discussed in Chapter 5, is to include a call to notifyAll() in every monitor method that modifies the state of the monitor. However, this can lead to unnecessary thread switches. In the ReadWriteSafe monitor, notification is required only when the last Reader has relinquished access and when a Writer releases. When the last Reader calls releaseRead() (i.e. readers==0), notify() rather than notifyAll() can be used since only Writers can be waiting and it is only necessary to unblock a single Writer. When a Writer is finished it calls releaseWrite() which then calls notifyAll(). This is because it may be necessary to unblock either one or more Readers or a Writer.

The implementation suffers from the progress problem detected in the model. If the number of Readers accessing the shared database never drops to zero, then Writers can never gain access. This behavior can be seen in the demonstration applet when the two Reader threads are started such that there is always one holding the lock. The applet display is depicted in Figure 7.16.

Figure 7.16: Readers–Writers applet display.

7.5.3 Revised Readers–Writers Model and Implementation

To address the progress problem discovered with our first model and implementation of the Readers–Writers problem, we adopt an approach in which Readers are denied access if there are Writers waiting to acquire access. This should give Writers priority in acquiring the lock and avoid the situation in which they wait forever for access. To detect that a Writer is waiting for access, we must add another action to its repertoire. A Writer must request access before attempting to acquire it. This is exactly the same solution we adopted in the single-lane bridge solution to detect whether cars were waiting. The additional action is requestWrite and the revised WRITER process is shown below:

 set Actions = {acquireRead,releaseRead,        acquireWrite,releaseWrite,requestWrite} WRITER =    (requestWrite->acquireWrite->modify                 ->releaseWrite->WRITER    )+Actions\{modify}.

The READER process remains unchanged. RW_LOCK is modified to maintain a count of waiting Writers (waitingW). The count is incremented when a Writer requests access and decremented when it actually acquires access. Readers are only allowed to acquire the lock when the number of waiting Writers is zero. The revised lock process is listed below:

 RW_LOCK = RW[0][False][0], RW[readers:0..Nread]   [writing:Bool]   [waitingW:0..Nwrite] =   (when (!writing && waitingW==0)      acquireRead -> RW[readers+1][writing][waitingW]   |releaseRead   -> RW[readers-1][writing][waitingW]   |when (readers==0 && !writing)      acquireWrite-> RW[readers][True][waitingW-1]   |releaseWrite  -> RW[readers][False][waitingW]   |requestWrite  -> RW[readers][writing][waitingW+1]   ).

This definition of RW_LOCK still satisfies the RW_SAFE property. Note that we have not had to change the definition of the safety property. The request action (requestWrite) is not relevant to the safe operation of the lock and so does not appear in the alphabet of the safety property. Safety is determined only by the correct sequencing of acquire and release actions.

A progress analysis of RW_PROGRESS now produces the output:

 Progress violation: READ Path to terminal set of states:      writer.1.requestWrite      writer.2.requestWrite Actions in terminal set: {writer.1.requestWrite, writer.1.acquireWrite,  writer.1.releaseWrite, writer.2.requestWrite,  writer.2.acquireWrite, writer.2.releaseWrite}

We no longer have a violation of the WRITE property, demonstrating that in this Writers priority system, Writers can always access the shared database. However, we now have a READ progress violation. This occurs since, if there is always a Writer waiting to acquire the lock, then Readers will never gain access. However, in the practical application of read/write locks, the Writers priority solution is often satisfactory since there are usually many more read accesses to a database than write accesses. In addition, it may be important that Readers get the most up-to-date information. The implementation of a Writers priority lock is listed in Program 7.8. It follows directly from the revised definition of RW_LOCK.

Program 7.8: ReadWritePriority class.

 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) notifyAll();   }   public synchronized void acquireWrite()              throws InterruptedException {     ++waitingW;     while (readers>0 || writing) wait();     --waitingW;     writing = true;   }   public synchronized void releaseWrite() {     writing = false;     notifyAll();   } }

A version of the read/write lock that satisfies both the READ and WRITE properties involves the addition of a boolean which indicates whether it is the Readers’ turn or the Writers’ turn. Readers only defer to waiting Writers when it is not their turn to acquire the lock. This turn variable plays exactly the same role in the Readers–Writers problem as the turn variable in the single-lane bridge. The final version of the read/write lock model is listed below. The implementation is left as an exercise.

 RW_LOCK = RW[0][False][0][False], RW[readers:0..Nread]   [writing:Bool]   [waitingW:0..Nwrite]   [readersturn:Bool] = (when (!writing && (waitingW==0||readersturn))       acquireRead ->RW[readers+1][writing][waitingW][readersturn]   |releaseRead    ->RW[readers-1][writing][waitingW][False]   |when (readers==0 && !writing)      acquireWrite  ->RW[readers][True][waitingW-1][readersturn]   |releaseWrite    ->RW[readers][False][waitingW][True]   |requestWrite    ->RW[readers][writing][waitingW+1][readersturn] ).