Newsletter sign-up
View all newsletters

Enterprise Java Newsletter
Stay up to date on the latest tutorials and Java community news posted on JavaWorld

Sponsored Links

Optimize with a SATA RAID Storage Solution
Range of capacities as low as $1250 per TB. Ideal if you currently rely on servers/disks/JBODs

Better monitors for Java

A Hoare-style monitor package for multithreaded programming in Java

  • Print
  • Feedback

Page 3 of 4

Conditions and 'design by contract'

If we follow the convention that the assertion Pc is true whenever c.signal() is called, then Pc must be true when c.await() returns. This is a sort of contract that the person implementing the monitor makes with himself. Indeed, signal() and await() are best understood in terms of "design by contract" based on preconditions and postconditions.

A contract for await()

The precondition of c.await(), as you've seen, is the monitor's invariant, which I'll call I. The thread only returns from c.await() when another thread calls c.signal(). From the precondition of c.signal(), as you will see, Pc must be true at that time. The contract for c.await() is shown below.

 
c.await()
Require:
I && this thread alone occupies the monitor
Ensure:
Pc && this tread alone occupies the monitor
 

A contract for signal()

What about signal()? If a thread is waiting on the condition's queue, then Pc must be true as a precondition. On return, as the monitor was just empty, the monitor invariant will be true as a postcondition. But what if no thread is waiting? In that case, signal() does nothing and so, to ensure the invariant is true as a postcondition, it should be a precondition as well. You can express the contract using c.isEmpty(), which indicates whether any threads are waiting on the condition.

 
c.signal()
Require:
( !c.isEmpty() && Pc  || c.isEmpty() && I )
&& this thread alone occupies the monitor
Ensure:
I && this thread alone occupies the monitor
 

The precondition of the above contract is a bit complicated. In practice you can almost always use one of two simpler preconditions instead; each implies the contract's precondition, as so, is a safe substitute. One precondition is

Pc && I && this thread alone occupies the monitor

and the other is

!c.isEmpty()&& Pc && this thread alone occupies the monitor

signalAndLeave()

Often, there is no need for a signaling thread to wait and later reoccupy the monitor. In this case you can call signalAndLeave(). Upon awakening an awaiting thread, if there is one, this method returns without re-occupying the monitor. The contract for signalAndLeave() is shown here.

 
c.signalAndLeave()
Require:
( !c.isEmpty() && Pc  || c.isEmpty() && I )
&& this thread alone occupies the monitor
Ensure:
this thread does not occupy the monitor
 

More detailed contracts

There's one more wrinkle to these contracts: they only work if neither the invariant I nor the assertion Pc depend on the number of threads waiting on c. That's because the acts of starting to wait and ceasing to wait change this quantity. John H. Howard and Ole-Johan Dahl give correct contracts for the rare cases when I and Pc are dependent on the number of waiting threads.

Assertion objects

Looking back at Listing 2, you can see that each assertion appears four times, counting comments, assert statements and if statements. For good reason, software engineers abhor such duplication. Of course, you could encapsulate each duplicated assertion in a method, but then you would have to duplicate the call to the method. In my Java-based monitor package I've provided a better solution, wherein each assertion may be represented by an object.

Classes representing assertions are created by subclassing Assertion and overriding the abstract method isTrue(). Each condition object knows one Assertion object and checks the assertion upon any call to signal(), throwing an exception if the assertion is false. Based on this approach, you could change the FIFO queue in Listing 2 by rewriting the declarations of the condition objects as follows:

Listing 3. The FIFO queue with assertions

private final Condition notFull = makeCondition(
        new Assertion() {
            public boolean isTrue() {return count < capacity ; } } ) ;


    private final Condition notEmpty = makeCondition(
        new Assertion() {
            public boolean isTrue() {return count > 0 ; } } ) ;



You can also use assertion objects to replace if statements, such as those in fetch and deposit, with calls to conditionalAwait(). The rewritten deposit method is shown in Listing 4; the fetch method can be rewritten similarly. The classes for the revised FIFO queue are shown in Figure 2. Similarly, there is a conditionalSignal() method.

Listing 4. The deposit method rewritten

public void deposit( Object value ) {
        enter() ;
            notFull.conditionalAwait() ;
            queue[ (front + count) % capacity ] = value ;
            count++ ;
        notEmpty.signalAndLeave() ; }
Classes for the revised FIFO queue

Figure 2. Classes for the revised FIFO queue (click for larger image)

In summary, the following checks are made automatically:

  • The invariant is checked on the return from enter(), the call to leave(), on the call to await(), on the return from signal(), and, when there is no waiting thread, on the call to signalAndLeave().
  • Assertion objects are checked on calls to signal() or signalAndLeave(), if there is a waiting thread, and on the return from await().

  • Print
  • Feedback

Resources