Patrick Lam

Associate Professor, Department of Electrical and Computer Engineering
Director, Software Engineering Programme
University of Waterloo
email: patrick.lam@uwaterloo.ca (no unsolicited commercial email)
phone: use email instead!

Picture of Patrick Lam

Example Applications

We implemented our system and, to obtain experience using it, coded up several benchmark programs, using our system during the development of the programs.

Our system verifies 1) the consistency of individual data structures encapsulated in instantiable modules, 2) that the rest of the program uses each module correctly, and 3) important properties that involve data structures encapsulated in different modules. The following examples illustrate how our approach enables the verification of properties that span multiple modules.

Water

We have ported the Water program from the Perfect Club benchmark, which uses a predictor/corrector method to evaluate forces and potentials in a system of water molecules in the liquid state. The central loop of the computation performs a time step simulation. Each step predicts the state of the simulation, uses the predicted state to compute the forces acting on each molecule, uses the computed forces to correct the prediction and obtain a new simulation state, and uses the new simulation state to compute the potential and kinetic energy of the system.

We use abstract sets to model the conceptual typestates of the data structures as the computation processes them. The predictor computation requires the object storing the simulation state to start in the corrected set. It then moves this object from the corrected set to the predicted set. The force computation moves the force object from the invalid set to the valid set; the corrector computation requires the object storing the simulation state to start in the predicted set, then moves it to the corrected set. It requires the object representing the forces to start in the valid set, then moves it into the invalid set (conceptually, the correction invalidates the computed forces). The energy computations require the object storing the simulation state to be in the corrected state. We include a typical specification, that of the inter-molecule forces computation:

  proc INTERF(m:MoleculeData; f:ForceData) returns cf : ForceData
    requires (m in Predicted) & (f in InterfUncomputed) &
    modifies InterfUncomputed, InterfComputed
    ensures (cf' = f) &
            (InterfUncomputed' = InterfUncomputed - cf') &
            (InterfComputed' = InterfComputed + cf');

We found that our system enabled us to easily express the conceptual state that each object in the data structure needed to be in for the computation to operate correctly. The flag analysis was able to verify that the program staged the computation correctly.

Minesweeper

Our minesweeper implementation has several modules, as shown below: a game board module (which represents the game state), a controller module (which responds to user input), a view module (which produces the game's output), an exposed cell module (which stores the exposed cells in an array), and an unexposed cell module (which stores the unexposed cells in an instantiated linked list). There are 750 non-blank lines of implementation code in the 6 implementation sections of minesweeper, and 236 non-blank lines in its specification and abstraction sections.

Modules in Minesweeper

Our minesweeper implementation uses the standard model-view-controller (MVC) design pattern. The board module (which stores an array of Cell objects) implements the model part of the MVC pattern. Each Cell object may be mined, exposed or marked. The board module represents this state information by contributing isMined, isExposed and isMarked flags to Cell objects. At an abstract level, the sets MarkedCells, MinedCells, ExposedCells, UnexposedCells, and U (for Universe) represent sets of cells with various properties; the U set contains all cells known to the board. The board also uses a flag gameOver, which it sets to true when the game ends.

Minesweeper Screenshot

Minesweeper Inter-Module Properties

Our system verifies that our implementation has the following properties (among others):

Stack Data Structure

For our stack example, we maintain an abstract set S representing the content of the stack, and verify that stack insertions actually insert the given object into the stack (S' = S + e), and that removal actually removes an object from the stack, if possible: card(S) = 0 | (exists e:Entry. (S' = S - e) & card(e) =1)).

Our PALE plugin checks that objects that belong to a set have consistent values for navigational fields (e.g. next, prev), and that objects that do not belong to the set have those fields set to null. Initially, our implementation for removeFirst was:

     proc removeFirst() returns e:Entry {
         Entry res = root;
         if (root != null) root = root.next;
         pragma "removed res";
         return res;
     }

where the pragma statement indicates to the analysis that it is verifying a set removal. However, the analysis reports an error while verifying this implementation. Careful inspection of this code, however, reveals that the removed object, res, will still have a reference to an object in the stack after removal; this is potentially problematic, as it may lead to non-list structures being present in the heap. Our plugin therefore requires us to add res.next = null to this procedure, so that all objects subsequently passed to this module will have next set to null.

Process Scheduler

Our process scheduler benchmark maintains a list of running processes and a priority queue of suspended processes. There are three modules in our process scheduler implementation: the {\tt RunningList} module (which maintains the list of running processes), the {\tt SuspendedQueue} module (which maintains the queue of suspended processes), and the {\tt Scheduler} module (which implements the specification for the scheduler). The running list and suspended queue are verified using the PALE plugin, whereas the scheduler itself is verified with the flag plugin. Both the data structures and the core scheduler know whether a process is running or suspended: the core scheduler uses flags to indicate set membership, whereas the data structures use heap reachability to track membership. One of the global invariants ensures that the sets in the scheduler and in the data structures coincide. Our analysis also verifies that the set of running processes is always disjoint from the set of suspended processes:

    invariant (Running = RunningList.InList) &
              (Suspended = SuspendedQueue.InQueue) &
              disjoint (Running, Suspended);

Valid HTML 5!