Expressing Checkable Properties of Dynamic Systems: The Bandera Specification Language
Case Studies

James C. Corbett - Matthew B. Dwyer - John Hatcliff - Robby

Note: The Java and property specification files will be linked in here

Applications of BSL

BSL support has been implemented in the latest version of the Bandera toolset. The user interface provides a significant advance over the previous interface for specifying program properties by extracting assertions and predicates and presenting the latter as building blocks for instantiating temporal pattern specifications.

The intended methodology for constructing BSL specifications can be summarized as follows.

Given an informal software requirement R,

Identify source code features/properties mentioned in R that should correspond to propositions in temporal reasoning. Typically, these propositions correspond to specific events or execution of a particular control point (e.g., a call to a particular method), or a constraint on the program's data state.

Formalize these propositions by defining BSL predicates or assertions in source Java-doc comments.

Select a temporal pattern and scope that matches the temporal structure of R, and parameterize the pattern with the predicates defined in the previous step. Alternatively, selectively enable the assertions from the source code that implement R.

If a temporal pattern is used in the previous step, add appropriate object quantification if instance predicates are used as parameters in the temporal pattern above.

Figure 1: Bounded Buffer Implementation with Predicate Definitions

Figure 2: Bounded Buffer Properties in BSL

BSL can used be used to write both white-box and black-box specifications. The IndexRangeInvariant and the FullToNonFull properties of the BoundedBuffer class (Figure 1) in Figure 2 are examples of white-box specifications, because the definition of the Full and TailRange predicates and the AddToEnd assertion depend on the actual implementation of the bounded buffer in terms of an array. The NoTakeWhileEmpty property is an example of a black-box specification; one can change the implementation of the bounded buffer from a circular queue to any other data structures without changing the definition of the predicates and the temporal specification.

The following subsections illustrate the capabilities of BSL by defining and checking properties of several software components that are difficult to express and check in other model checking tools due to the presence of dynamic object creation.

For each sample application, we present annotated source code and both black and white-box specifications. In order to check those properties we defined an environment for the software component. Environments consist of a main program which allocates a number of instances of the component's objects. In cases where the components are interfaces or abstract classes, the environment code includes appropriate class definitions to implement or extend those components; those classes are then instantiated by the main program

The main program also instantiates and starts a number of threads that repeatedly and non-deterministically choose a component class instance, choose a method of the component class, choose parameters for that method and then perform the chosen method invocation. The intent is to create a multi-threaded environment that is capable of all possible sequences of calls on the component under analysis; in some cases, e.g., the BoundedBuffer, we were able restrict the sequence of calls based on the property being checked. The number of component instances and threads in these environments can be easily adjusted and we kept them rather small in the applications described below.

Figure 3: Readers Writers Implementation with Predicate Definitions

Figure 4: Readers Writers Properties in BSL

Bounded Buffer

To exercise the methods of the BoundedBuffer class, we built a simple environment (not shown here) consisting of four threads: a main thread that instantiates two BoundedBuffers, loads one of the buffers until it is full, then passes the pair of buffers to threads that read from one buffer and write to the other such that a ring topology is established. An additional thread repeatedly polls the state of the two BoundedBuffers to determine if they are empty. Under this environment, each buffer will be forced through all its internal states limited by its bound and Bandera determines that all of the properties in Figure 2 hold.

Readers Writers Synchronization

Java's concurrency facilities have been used to implement several reusable customizable implementations that embody common patterns of synchronization. We analyzed correctness properties of Doug Lea's Readers Writers Synchronization Class RW. Figure 3 shows source code for the RW class annotated with BSL observables and assertions. This class provides readers/writers synchronization but provides no guarantees about the order in which requested read or write operations will occur. This functionality is provided to users by way of two abstract methods, read_() and write_(), that users extend to perform application specific processing. Those methods are wrapped by calls to, for example, beforeRead() and afterRead() that implement the synchronization policy; note that overriding these methods can change the policy, but we analyzed the policies implemented in the RW class.

Figure 5: Observer Interface and Observable Implementation (excerpts)

We formalized two properties:

(1)

write operations operate exclusive of any other operation, and

(2)

read operations may execute concurrently.

White-box specification of these properties can be expressed by querying the state of the RW instance when read_() and write_() operations are invoked. We code these as pre-condition assertions in Figure 4. Black-box specifications of these properties are expressed by specifying that, for example for property (1), invocations of the read_() cannot occur after write_() has been invoked and before it returns for a given instance. These black-box specifications are coded as absence properties with after-until scopes in Figure 4.

The environment for these components consisted of two instances of sub-types of the RW that implement trivial read_() and write_() methods, and four threads that repeatedly choose to call the read() and write() methods of those instance. Under this environment, Bandera is able to show that all of the specifications in Figure 4 hold.

Observer Pattern Implementations

The intent of the Observer pattern, as described in, is to ``define a one-to-many dependency between objects so that when one object changes state, all its dependents are notified and updated automatically''. There are many variations of this pattern. We applied Bandera to analyze properties of an implementation that is available in the SUN's Java Development Kit in the form of the java.util.Observer interface and java.util.Observable class (the code we analyzed was version 1.10 of Observer and version 1.19 of Observable which were written by Chris Warth and which are both copyright by Sun Microsystems, Inc.). Excerpts of that code with BSL observable (in an unfortunate duplication of terms, the BSL keyword observable coincides with the name of one of the classes in this application) and assertion definitions is given in Figure 5.

Figure 6: Observer Properties in BSL

There are two kinds of actors in the observer pattern: observers and observables. An observer may monitor the state of several observables, and an observable may have several observers. The Observable.addObserver() registers a given observer's intent to monitor changes in the observable. The Observable.deleteObserver() method dissolves the association between an observer and an observable. Users extend class Observable to add application-specific data and methods and to indicate when changes have occurred that should cause observers to be notified. A change that prompts notification is indicated by calling the Observable.setChanged() and Observable.notifyObservers() methods in sequence; in our application, the method changeState() performs this sequence. Observable.notifyObservers() indicates to all registered observers that a change has been made by invoking the Observer.update() ``call-back'' method of each observer.

We formalized two properties for this system:

(1)

only registered observers are notified of updates, and

(2)

all registered observers are notified of updates.

We encoded both white and black-box specifications for these properties which are shown in Figure 6.

The white-box specification identifies the location, labeled window in the Observable.notifyObservers() method, after which the collection of registered Observers has been constructed but before the call-backs have been made. The code is implemented this way so that the Observable instances lock is not held while the call-back methods execute (since they may take an arbitrary amount of time). A mismatch in the sizes of the local array, arrLocal, and the Vector of observers at this point indicates that a change in registration has occurred since Observable.notifyObservers() was called. If that change was the deletion of an observer, then that observer will still be notified which violates property (1). If that change was the addition of an observer, then that observer will not be notified which violates property (2). The assertion obsCountsEqual checks observer collection sizes for equality, and, consequently, it can detect both of these violations. It is interesting to note that there are comments in the actual source code of the java.util.Observable.notifyObservers() method that indicate that the author of the method knowingly left race conditions in the implementation that lead to the two situations mentioned above; the author apparently felt that the consequences of these ``violations'' were not severe.

Black-box specifications are defined only in terms of the events and data at the component's interface (i.e, which methods are called and with what parameters). Since Observable instances do not make their registered observers public, a black box specification must ``record'' registration information by observing sequences of Observable.addObserver() and Observable.deleteObserver() calls. For property (1) there are two cases to consider: (a) an observer must not be updated for a change in an observable before it registers for that observable for the first time, and (b) an observer must not be updated for a change in an observable between the time it unregisters and the time it re-registers for notifications of changes in that observable. These sub-cases are coded as two specifications. The first, InitiallyNotNotified, states that calls to Observer.update() are absent an appropriate call to addObserver has completed. The second, NotRegisteredNotNotified, states that calls to Observer.update() are absent after a call to Observable.deleteObserver() until a call to Observable.addObserver() returns. Parameterization of predicates in these specifications insures that the sequence of calls must occur for the same Observer and Observable instances.

Property (2) is more complex to state as a black-box specification. Essentially we want to state that if an Observer registers for an Observable and does not unregister up to the point where a call to Observable.notifyObservers() is made, then Observer.update() will be called before Observable.notifyObservers() returns; this specification describes synchronous notification. This is coded as property RegisteredNotified in Figure 6 using a constrained-response chain pattern. This pattern was not originally in the BSL library, but was added for this application by adding the pattern definition in Figure 7.

Figure 7: BSL Chain Pattern Definition

The next section will give an alternate white-box formulation of this property.

As with the BoundedBuffer example, we constructed an environment with a class that extends Observable and one that implements Observer, and with threads that repeatedly make calls to changeState() and register and unregister observers with observables. For an environment with two observers, two observables, one state changing thread, and one registration thread we were able to check all of the above properties. All properties were violated (except InitiallyNotNotified which was verified) which is consistent with the documented behavior of the Observable.notifyObservers() method.

Discussion

Our goal in this section was to illustrate that BSL allows for interesting properties of realistic software to be expressed and checked.

Several differences were apparent in the use of white-box versus black-box specifications. Clearly there are situations in which white-box specification is not possible, for example, when the behavior of an interface or abstract method is to be defined. The white-box specifications described in this paper were generally assertions, but that need not be the case. Predicates can be defined that test the values of static and instance fields as in the FullToNonFull white-box buffer property.

White-box specifications can be viewed as a test case description for multi-threaded software. For example, the race conditions that are the subject of the obsCountEqual assertion in Figure 6 would be extremely difficult to test for using traditional methods.

White-box specifications are not reusable since they depend on the implementation details of a system. Conversely, the black-box readers/writers properties in Figure 4 were reused verbatim in checking both the RW and RWVSN implementations.

The black-box specifications for the Observable.notifyObservers() method did not capture the behavior of that method in a multi-threaded environment. In fact, it is difficult to capture the exact behavior of that method using any black-box specification since race conditions can cause interference both between the method call and the start of the synchronized statement and between the end of the synchronized statement and the call to Observer.update(). One way to address this is to weaken, for example, property (2) to state that ``all registered observers are notified of updates so long as no observers unregister during notification''. One could specify this by modifying the RegisteredNotified property to require that no invocations of Observable.deleteObserver() co-execute with the call to Observable.notifyObservers(). With only INVOKE and RETURN predicates available, this specification would be extremely complex, but by introducing predicates that hold for the duration of a Observable.deleteObserver() call would make the modification relatively simple. We are considering extending location predicates to regions of locations to handle this kind of situation; the extension is straightforward as the region predicate is simply a disjunction of location predicates.

While temporal specifications are necessary to describe the sequencing of actions for the same object instance, it is often significantly more efficient to use assertions. In the readers writers application above, checks of the assertions were two orders of magnitude faster than checks of the temporal properties.