Finding Feasible Abstract Counter-examples : Case Studies

Corina S. Pasareanu - Matthew B. Dwyer - Willem Visser

Experience with Defective Java Applications

To illustrate the potential benefits of the techniques described in the previous section, we applied them to several small to medium-size multi-threaded Java applications. These applications used both lock synchronization and condition-based synchronization (i.e., wait/notify). The systems are: RAX (Remote Agent experiment), a Java version of a component extracted from an embedded spacecraft-control application, Pipeline, a generic framework for implementing multi-threaded staged calculations, RWVSN, Lea's generic readers-writers synchronization framework, DEOS, the scheduler from a real-time executive for avionics systems that was translated from C++, BoundedBuffer, a bounded buffer implementation in Java that is amenable to simultaneous use by multiple threads, NestedMonitor, a version of the bounded buffer implementation that uses semaphores instead of Java condition-based synchronization, and ReplicatedWorkers, a parameterizable parallel job scheduler.

Most of these programs use a rich set of Java features and concurrency constructs, including abstract classes, inheritance, and java.util.Vector. The RAX, DEOS, BoundedBuffer and NestedMonitor examples had known errors that we checked for. For the Pipeline, RWVSN and ReplicatedWorkers examples we seeded faults in the program. For example, we dropped a negation (!) in two programs and changed <= into < (simulating an off-by-one error) in the other. It is interesting to note that not all seeded faults could be detected given the properties we checked for, so we altered the faults until we generated a property violation. In our experiments, we encoded the properties to be checked as assertions (rather than temporal logic formulae), in order to use JPF's new heuristic-search capabilities.

Description of experiments

We now describe several model checks for the abstracted systems and the automated analysis of the resulting counter-examples. The data for each of the model checking runs, using JPF to perform choose-free search, depth-first search, breadth-first search and choose-free heuristic search is described here. For each run, we report the abstraction that was used, the size of the counter-example, the total of user and system time to execute the checking and the memory used in verification. All model checks were performed on a SUN ULTRA5 with a 270Mhz UltraSparc IIi and 512Meg of RAM. The results are slightly different from the original paper, due to the use of the updated (and improved) version of the JPF tool. Full details for the examples and model checks are available are linked below.

RAX

We model checked the RAX example to detect deadlocks using two different abstractions. The abstraction of the program was driven by our selection that the Event.count field should be abstracted with signs. Bandera's abstraction type inference determined that the local count variables in the FirstTask.run() method should also be abstracted, since there are two event objects allocated this amounts to four abstracted variables in the system. Running JPF (using depth-first search) on this abstracted system detects a deadlock and produces a 103 step counter-example. Analysis of this counter-example reveals that it is spurious. After 35 steps in the counter-example the trace reaches the conditional at line 15. In the real system, the branch condition is false, but due to the nondeterminism of Signs.eq() for positive parameters the abstract system enters the conditional. JPF is able to find a 30 step choose-free counter-example. Running JPF using the heuristic searches (i.e., both breadth-first search and choose-free heuristic search) discover the same 30 step counter-example.We ran JPF in simulation mode guided by the 30 step counter-example and it was shown to be feasible. It is clear that the presence of spurious counter-examples is closely related to the property being checked, the program and the abstraction's selected. We reran our model checks changing the abstraction for Event.count field to record information about the evenness or oddness of its values. This produced a 72 step counter-example (using depth-first search) and a 30 step counter-example (using both heuristic searches), but JPF was unable to find a choose-free counter-example. At this point, we ran JPF in simulation mode guided by the 72 step and the 30 step counter-examples and while these counter-examples did contain nondeterministic choices, they were shown to be feasible.

Pipeline

The Pipeline example consists of an application that uses the methods of a Pipeline class to manage execution of a multi-threaded staged computation. The application constructs and starts execution of a pipeline, calls stop() to end execution of the pipeline, and calls add() to provide input to the computation. We model checked a precedence property for the Pipeline system stating that ``no pipeline stage (i.e., thread) will terminate until the stop method is called''. We encoded this using a boolean variable, stopCalled, set to true when the stop() method had been called and embedded assert(stopCalled) at the return point of the stage run methods. This example was abstracted by identifying a loop index variable that controlled the number of times the add() method was called and abstracting it to signs. Type inference determined that 5 additional fields and local variables also needed abstraction. JPF found a choose-free counter-example that occurred on the first iteration of an abstracted loop. We ran JPF in simulation mode to analyze the counter-examples produced during depth-first search and the heuristic searches, and they were shown to be feasible.

RWVSN

RWVSN consists of an application that extends Lea's RWVSN class to implement an object with a readers-writers synchronization policy. That object is then shared by several threads that read and write through the RWVSN interface. We checked that access by a reader excluded access by a writer by setting a boolean variable, in_writer, in the writer's critical section and resetting it upon exit, and embedding assert(!in_writer) in the reader's critical section. Abstraction was applied to 3 integer fields of the RWVSN class abstracting them to signs. JPF found a choose-free counter-example; the counter-example produced during depth-first search was analyzed and found not feasible, while the counter-examples produced during heuristic searches were shown to be feasible.

DEOS

The DEOS real-time scheduling kernel has been the subject of several recent case studies in model checking code. The property being checked is an assertion that encodes a test for time partitioning in the scheduler component of the system. We used JPF to detect a subtle implementation error related to the kernel's time partitioning requirement that was originally discovered and fixed during the standard formal review process. That requirement is that ``application processes are guaranteed to be scheduled for their budgeted time during a scheduling unit''. The requirement was encoded as a method that observes the state of the kernel and asserts that budgets are allocated in each scheduling unit. Calls to this method are inserted whenever the kernel schedules an application process; this guarantees the detection of property violations. To analyze the DEOS kernel, additional code was written to simulate the behavior of user applications and the hardware environment (e.g., a tick generator thread simulates a hardware clock for time related processing in the kernel). We modeled the environment using explicit external nondeterminism. We used dependence analysis driven by the location of the assert statement and the data values it referenced to identify a single field (out of 92) as influencing the property. We selected the signs AI for that field and type inference determined that 2 more fields should be abstracted. Checking the property on the abstracted system detected a choose-free counter-example (i.e. a counter-example that does not contain internal nondeterminism introduced by the abstraction). JPF ran out of memory during the heuristic searches.

BoundedBuffer

The BoundedBuffer program uses a synchronization object that monitors the access to a bounded buffer into which producer threads put items and consumer threads get items. The monitor class maintains an array of objects, two indices into that array representing the beginning and the end of the active segment of the array and a counter of the items stored into the buffer. A constant SIZE defines the maximum number of items that may be stored in the buffer. Calls to put() items into the buffer are guarded by a check for a full buffer using the Java conditional wait/notify idiom; calls to get() items into the buffer are guarded similarly by a check for an empty buffer. We ignored the details of what items are stored in the buffer and how these items are stored. We analyzed an instance of the problem with two producer and two consumer threads. The abstraction of the program was driven by our selection that the constant SIZE should be abstracted with signs. Bandera's abstraction type inference determined that variable count, that stores the number of items currently stored in the buffer, should also be abstracted. Running JPF (using depth-first search) on this abstracted system detects a deadlock and produces a counter-example; analysis of this counter-example reveals that it is spurious. No choose-free counter-example were found. Using the heuristic searches, JPF found counter-examples that were shown to be feasible. We reran our model checks changing the abstraction for SIZE with range(0..1) abstraction, which tracks concrete values 0 and 1, but abstracts the values less than 0 and greater than 1, by using the set of tokens { below0, zero, one, above1 }; this produced a choose-free counter-example. We ran JPF in simulation mode guided by the counter-example produced using depth-first search and it was shown to be not feasible; the counter-examples reported by the heuristic searches were found to be feasible.

NestedMonitor

The NestedMonitor program is an implementation of the bounded buffer that may deadlock because of nested monitor calls. We analyzed an instance of the program with one producer thread and one consumer thread. As with the previous example, we abstracted the constant SIZE (that records the number of items that are stored in the buffer) using signs. Checking the abstracted system yielded feasible counter-examples with each of the techniques.

ReplicatedWorkers

The ReplicatedWorker system a parameterizable job scheduler, where the user configures the computation to be performed in each job, the degree of parallelism and several pre-defined variations of scheduler behavior. An instance of this framework is a collection of similar computational elements, called workers. Each worker repeatedly accesses data from a shared work pool, processes the data, and produces new data elements which are returned to the pool. Users define the number of workers, the type of work data, and computations to be performed by a worker on a item. We checked for proper termination (i.e., that the computation can not terminate unless the work pool is empty or a worker signals termination). We encoded with an assertion that uses a variable, GLobalDone, set to true when a worker thread signals termination. To analyze the framework, additional code was written to simulate the behavior of a driver that invokes the framework's operations and of stubs that implement the work done by workers. Similar to DEOS, we modeled the environment using explicit external nondeterminism. The signs abstraction was applied to the variable that stores the number of work items in the pool. Checking the abstracted system yielded a choose-free counter-example; during heuristic searches, JPF ran out of memory.