JavaFlow
Contents
Enabling your application for model checking
In addition to the controls described in earlier sections, there are certain constraints on how the application should be coded to enable processing by BPmc. BPJ uses the package Javaflow to perform backtracking as needed for model checking. Depending on the run mode, BPJ instruments the application for Javaflow. As part of traversing all possible execution paths, BPmc uses Javaflow for backtracking and saves and restores the thread’s stack using an object called "continuation". The stack contains the non-static fields/variables from the b-thread class and the variables defined in-line in the runBThread method. Objects (which are not on the stack) are saved and restored by BPmc using serialization and deserialization of the continuation object. Serialization translates each field and each object pointed to from the continuation into a bit stream. Deserialization turns such bit streams into program objects and fully restores the state.
Programming Requirement 1
When two pointers on the stack point to the same object, Javaflow deserialization creates two copies of the object, and the application that relied on the two being one object no longer works. Therefore, do not use the operator "==" to compare objects that are part of the b-thread's state. Instead, use the equals() method. A default equals() method based on object ids already exists for events.
Programming Requirement 2
Serialization and desrialization may significantly slow the application. Therefore, if you have objects that do not change from one bt-state to another, mark them as transient static (for the class or for the instance, as needed). Objects marked as transient are not processed by serialization and deserialization resets them to their initial value.
Programming Tip
If all the objects pointed to from the stack can be transient as defined above, you do not have to specify them as transient, and instead you can just specify static, and specify the run time parameter "–Dshallow=true" (the default is "-Dshallow=false"). Then, the when BPJ uses Javaflow to save and restore the stack(s) it does not perform serialization and deserialization.
