One of the more recent additions to Bogor is an internal publish-subscribe event notification system. Similar to the GTK+ windowing toolkit's signal/slot mechanism or the even more formal event source/event sink used in the CORBA Component Model, Bogor allows a custom module developer to register a listener object which takes notice of various events which occur during state space traversal.

Our experience indicates that using an event/callback framework allows customizations and optimizations to be implemented with much less code duplication. For example, a prior implementation of partial order reductions techniques for Bogor required duplication of almost the entire ISearcher implementation so that various bookkeeping tables could be updated as BIR objects are accessed. Every change to the default ISearcher had to be meticulously applied to the optimized version too. Using the event framework, the optimizations proceed independently of the searcher implementation, caring only to be notified when each of certain well defined events occurs.

Bogor's implementation of the signal-callback idiom focuses on two main classes of entities: notifiers and listeners. Listeners are the individual clients who wish to be messaged every time some particular event happens, and notifiers are the multiplexers which bridge the gap between producers of events and the individual consumers. Although some frameworks (for example, Java Swing) assign the task of managing event subscribers directly to the producers, we find that introducing the notifier as an intermediary allows better separation of concerns.

There are two flavors of events in Bogor: state events (global variable updated, activation record created, etc.) and value events (BIR object dereferenced, lock ownership tested, etc.). For both families there is a top-level notifier ( state notifier interface and value notifier) and a series of fine-grained interfaces (coarse aggregations of all events are given by the state listener and value listener interfaces).

The first step toward connecting a new client to the publish-subscribe framework is to implement the desired callbacks. Suppose that we want to know whenever a global variable is updated. Then we implement the IGlobalVarReadListener interface:

        
public class SimpleGlobalVarReadListener
    implements IGlobalVarReadListener
{
    // The callback
    public void globalVarRead(
        int threadId,
        int globalIndex,
        IValue readValue)
    {
        System.out.printf(
            "Thread %d accessed global offset %d\n",
            threadid,
            globalIndex);
    }
    
    // Key used to see whether notifications are
    // currently enabled on this listener.
    public Object getKey()
    {
        return this;
    }
}
        
      

Now armed with a listener class, we must find a way to programatically attach one of these listeners during Bogor initialization. The connect() phase of any IModule works well for this purpose. This is such a natural place from which to attach listeners, in fact, that Bogor recognizes a plug-point in its configuration which exists only to provide the names of IListener (a trivial sub-interface of IModule) classes which should be instantiated and allowed to attach callbacks.

But this is slightly ahead of our narrative. Returning to the issue of how to attach a new listener instance and enable event deliveries to it:

        
public class GlobalVariableReadListenerModule implements IListener
{
    private static final boolean NOTIFIER_DIRECTION_FORWARD = true;
    private static final boolean NOTIFIER_DIRECTION_BACKWARD = false;
    
    /**
     * Our custom listener instance
     */
    IGlobalVarReadListener listener;
    
    /**
     * The Bogor module from which the state-events notifier
     * is fetched.
     */
    IStateFactory sf;
    
    ...
    
    public IMessageStore connect(IBogorConfiguration bc)
    {
        sf = bc.getStateFactory();
        
        // allocate listener
        listener = new SimpleGlobalVarReadListener();
        
        // attach listener
        sf.getNotifier(NOTIFIER_DIRECTION_FORWARD)
          .addGlobalVarReadListener(listener);
          
        // enable delivery of events to listener
        sf.getNotifier(NOTIFIER_DIRECTION_FORWARD)
          .enableNotification(listener.getKey());
    }
    
    public void dispose()
    {
        if (sf != null)
        {
            // Disabling the listener isn't really necessary here, but
            // this example shows how it would be done...
            sf.getNotifier(NOTIFIER_DIRECTION_FORWARD)
              .removeEnableNotificationKey(listener.getKey());
              
            sf = null;
        }
    }
    
    ...
}
        
      

Finally, we must indicate to Bogor that the new module GlobalVarReadListenerModule should be instantiated and connected to the runtime, so that our listener is likewise connected. This is done by using the previously hinted-at configuration file key edu.ksu.cis.projects.bogor.module.IListener to give a comma-separated list of such modules which are to be instantiated. In our case:

edu.ksu.cis.projects.bogor.module.IListener=GlobalVariableReadListenerModule
      

Alternately, users of the Eclipse-based Bogor user interface can specify that a module should be loaded for a model checking run by adding a new node to the "Event Listeners" subtree on the configuration dialog.