Latest revision as of 09:49, 19 March 2014

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 model checking. 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, BPJ model checking 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 the BPJ model checking 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.

Example: Examine the code snippet below:

  Integer x = new Integer(5);
  bSync(...)
  x++;
  bSync(...)

If -Dshallow=true is specified, in the second visit to the second bSync (after backtracking to try an execution with a different choice of event in the first bSync) the value of X will be 7, because X was not restored. Solution: Use int and not Integer - and then the variable is on the stack, and is always restored with backtracking, or use -Dshallow=false, to force full serialization.