13.3 Modeling Variables and Synchronized Methods


13.3 Modeling Variables and Synchronized Methods

13.3.1 Variables

Variables are modeled in exactly the same way as presented in Chapter 4. However, for convenience, we add actions to model incrementing and decrementing integer variables. An integer variable is modeled as follows:

 const Imax = 5  // a maximum value that variable can take range Int  = 0..Imax set   VarAlpha = {read[Int],write[Int],inc,dec} VAR(Init=0)= VAR[Init], VAR[v:Int] = (read[v]     ->VAR[v]     // v              |inc         ->VAR[v+1]   // ++v              |dec         ->VAR[v-1]   // --v              |write[c:Int]->VAR[c]     // v = c              ).

A boolean variable is modeled by:

 const False = 0 const True  = 1 range Bool  = False..True set   BoolAlpha = {read[Bool],write[Bool]} BOOLVAR(Init=False) = BOOLVAR[Init], BOOLVAR[b:Bool]     = (read[b]      ->BOOLVAR[b] // b                       |write[c:Bool]->BOOLVAR[c] // b = c                       ).

13.3.2 Monitor Exit and Entry

In Chapter 4, we noted that synchronized methods acquire the monitor lock before accessing the variables of a monitor object and release the lock on exit. We will use the same simple model of a lock used in Chapter 4, ignoring the detail that locks in Java support recursive locking:

 set LockOps = {acquire,release} LOCK = (acquire -> release ->LOCK).

We can now model the state of a monitor by the set of processes that represent its wait set, lock and variables. For example, the state for a monitor M that encapsulates a single boolean variable cond is modeled as follows:

 ||Mstate = (Threads::LOCK  || WAITSET            || Threads::(cond:BOOLVAR)            ).

The definition of the Java wait() operation in Chapter 5 requires that a waiting thread releases the synchronization lock.We model this as a sequential process that releases the lock when it blocks and acquires it again when it unblocks and finishes waiting.

 WAIT = (wait ->release ->endwait ->acquire ->END).

In Java, the notification and waiting operations are only valid when the thread calling these operations holds the lock for the monitor object on which the operations are invoked. The following safety property checks that this is the case in the implementation models we construct:

 property SAFEMON    = ([t:Threads].acquire -> HELDBY[t]), HELDBY[t:Threads]    = ([t].{notify,notifyAll,wait} -> HELDBY[t]      |[t].release -> SAFEMON      ).

13.3.3 Synchronized Methods

A synchronized method of the form:

 synchronized void act()throws InterruptedException {       while (!cond) wait();       // modify monitor data       notifyAll() }

can now be modeled by the following FSP sequential process. As in Chapter 4, alphabet extension ensures that only intended interactions occur since it is usually the case that a process modeling a synchronized method will only use a subset of the data access actions (in this case only read is used on the boolean condition) and synchronization actions (in this case only notifyAll is used).

 ACT   // act()   = (acquire -> WHILE),     // monitor entry – acquire lock WHILE   = (cond.read[b:Bool] ->   // while (!cond) wait();     if !b then WAIT;WHILE else CONTINUE     ), CONTINUE   = (                       // modify monitor data     notifyAll               // notifyAll()     -> release              // monitor exit – release lock     -> END   ) + {SyncOps, LockOps, cond.BoolAlpha}.

Note that with the above constructions, while we can now model monitors in some detail, we are still ignoring the effect of InterruptException occurrence and handling. In the book, we have only used this mechanism to terminate all the threads that constitute the concurrent Java program. At the end of this chapter we discuss the problems that can arise if only a subset of threads is terminated in this way.




Concurrency(c) State Models & Java Programs
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net