13.2 Modeling Condition Synchronization

13.2 Modeling Condition Synchronization

In Chapter 5, we explained how a guarded action in a design model can be translated into a synchronized method as shown below:

  FSP:   when cond act -> NEWSTAT Java: public synchronized void act()              throws InterruptedException       {         while (!cond) wait();         // modify monitor data         notifyAll()       }

We noted that if an action modifies the data of the monitor, it can call notifyAll() to awaken all other threads that may be waiting for a particular condition to hold with respect to this data. We also noted that if it is not certain that only a single thread needs to be awakened, it is safer to call notifyAll() than notify() to make sure that threads are not kept waiting unnecessarily. We use an implementation model to investigate this particular aspect further in the rest of this chapter.

13.2.1 Wait, Notify and NotifyAll

To verify that a program using this translation satisfies the required safety and progress properties, we must model the behavior of wait(), notify() and notifyAll(). We can then rigorously check the use of notify() versus notifyAll(). A model for the interaction of these methods is developed in the following. Firstly, we define a process ELEMENT to manage the BLOCKED state of each thread that accesses a monitor.

 ELEMENT   = (wait -> BLOCKED | unblockAll -> ELEMENT), BLOCKED   = ({unblock,unblockAll} -> UNBLOCK), UNBLOCK   = (endwait -> ELEMENT).

The wait action, representing a call to wait(), puts the process into the BLOCKED state. Then either an unblock action caused by a notify() or an unblockAll action caused by a notifyAll() causes the process to move to UNBLOCK and signal the return of the wait() method by the endwait action. We will deal with the way that the monitor lock is released and acquired by wait() later.

The CONTROL process manages how notify and notifyAll actions, representing the eponymous Java methods, cause unblock and unblockAll actions:

 CONTROL = EMPTY, EMPTY   = (wait -> WAIT[1]           | {notifyAll,notify} -> EMPTY           ), WAIT[i:1..Nthread]         = (when (i<Nthread) wait -> WAIT[i+1]           |notifyAll -> unblockAll -> EMPTY                     |notify -> unblock ->            if (i==1) then EMPTY else WAIT[i-1]           ).

Since we can only check systems with a finite set of states, we must define a static set of identifiers Threads to represent the set of threads that can potentially access a monitor object. The cardinality of this set is defined by the constant Nthread. The CONTROL process maintains a count of the number of processes in the BLOCKED state. If there are no blocked processes then notify and notifyAll have no effect. If there are many blocked processes then a notify action unblocks any one of them. The set of threads waiting on a monitor and the effect of the wait(), notify() and notifyAll() methods are modeled by the composition:

 const Nthread = 3       //cardinality of Threads set   Threads = {a,b,c} //set of thread indentifiers set   SyncOps = {notify,notifyAll,wait} ||WAITSET       = (Threads:ELEMENT || Threads::CONTROL)         /{unblockAll/Threads.unblockAll}.

The composition defines an ELEMENT process for each thread identifier in the set Threads. The CONTROL process is shared by all the threads in this set. The relabeling ensures that when any thread calls notifyAll(), then all waiting threads are unblocked. The behavior of WAITSET is best illustrated using the animation facilities of LTSA.

Figure 13.5 shows a trace in which thread b calls wait, then thread a calls wait. A call by thread c to notify unblocks thread a. Note that while thread b was blocked before a, it is a that is unblocked first. In other words, the model does not assume that blocked threads are held in a FIFO queue, although many Java Virtual Machines implement thread blocking this way. The Java Language Specification specifies only that blocked threads are held in a set and consequently may be unblocked in any order by a sequence of notifications. An implementation that assumes FIFO blocking may not work correctly on a LIFO implementation. The WAITSET model permits all possible unblocking orders and consequently, when we use it in verification, it ensures that if an implementation model is correct, it is correct for all possible orders of blocking/unblocking actions.

Figure 13.5: WAITSET trace for notify.

Figure 13.6 illustrates the behavior for notifyAll when threads a and b are blocked.

Figure 13.6: WAITSET trace for notifyAll.