4.3 Modeling Mutual Exclusion

4.3 Modeling Mutual Exclusion

The simplest way to correct the model of the Ornamental Garden program listed in Figure 4.4 is to add locking in exactly the same way as it was added to the Java program. For simplicity, we ignore the detail that Java locks are recursive since whether or not the lock is recursive has no impact on this problem. A (non-recursive) lock can be modeled by the process:

 LOCK = (acquire->release->LOCK).

The composition LOCKVAR associates a lock with a variable. It is substituted for VAR in the definition of GARDEN.

 ||LOCKVAR = (LOCK || VAR).

The alphabet VarAlpha is modified as follows to include the additional locking actions:

 set VarAlpha = {value.{read[T],write[T],                        acquire, release}}

Finally, the definition of TURNSTILE must be modified to acquire the lock before accessing the variable and to release it afterwards:

 TURNSTILE = (go    -> RUN), RUN       = (arrive-> INCREMENT             |end   -> TURNSTILE), INCREMENT = (value.acquire              -> value.read[x:T]->value.write[x+1]              -> value.release->RUN             )+VarAlpha.

We can check this model in exactly the same way as before using TEST. An exhaustive search does not find any errors. Consequently, we have mechanically verified that this new version of the model satisfies the property that the count value is equal to the total number of arrivals when stop is pressed. A sample execution trace of the new model is shown below:

 go east.arrive east.value.acquire east.value.read.0 east.value.write.1 east.value.release west.arrive west.value.acquire west.value.read.1 west.value.write.2 west.value.release end display.value.read.2 right

Now that we have shown that we can make shared actions indivisible or atomic using locks, we can abstract the details of variables and locks and model shared objects directly in terms of their synchronized methods. We can perform abstraction mechanically by hiding actions. For example, we can describe the behavior of the SynchronizedCounter class (over a finite integer range) by:

 const N = 4 range T = 0..N VAR = VAR[0], VAR[u:T] = ( read[u]->VAR[u]            | write[v:T]->VAR[v]). LOCK = (acquire->release->LOCK). INCREMENT = (acquire->read[x:T]              -> (when (x<N) write[x+1]                  ->release->increment->INCREMENT                 )              )+{read[T],write[T]}. ||COUNTER = (INCREMENT||LOCK||VAR)@{increment}.

The definition of INCREMENT has been slightly modified from that used previously. The when clause ensures that the increment action can only occur when the value stored is less than N. In other words, increment is not allowed to overflow the range T. The alphabet declaration @{increment} means that read, write, acquire and release become internal actions (tau) of COUNTER. The LTS which results from minimizing COUNTER is depicted in Figure 4.8.

Figure 4.8: Minimized LTS for COUNTER.

We can describe a single process that generates exactly the same LTS:

 COUNTER = COUNTER[0], COUNTER[v:T] = (when (v<N) increment->COUNTER[v+1]).

This is a much more abstract and consequently simpler model of the shared Counter object with its synchronized increment method. We have demonstrated above (by LTSA minimization) that it has exactly the same observable behavior as the more complex definition. A display action to read the value of the counter can be added as shown below:

 DISPLAY_COUNTER = COUNTER[0], COUNTER[v:T] = (when (v<N) increment->COUNTER[v+1]                |display[v] -> COUNTER[v]).

The LTS which results from minimizing DISPLAY_COUNTER is depicted in Figure 4.9.

Figure 4.9: Minimized LTS for DISPLAY_COUNTER.

To implement this action in the Java class, we would simply add the synchronized method:

 public synchronized int display() {      return value; }

In the following chapters, we usually model shared objects at this level of abstraction, ignoring the details of locks and mutual exclusion (as provided by the use of synchronized methods in Java). Each shared object is modeled as an FSP process, in addition to modeling each Java thread as an FSP process. The model of a program does not distinguish active entities (threads) from passive entities (shared objects). They are both modeled as finite state machines. This uniform treatment facilitates analysis.