Difference between revisions of "JavaFlow"
From BP Wiki
| Line 2: | Line 2: | ||
* BPJ uses the package Javaflow to perform backtracking as needed for 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 (the user may observe that some objects are instantiated twice – this should OK). | * Depending on the run mode, BPJ instruments the application for javaflow (the user may observe that some objects are instantiated twice – this should OK). | ||
| − | * As part of traversing all possible execution paths, BPmc uses Javaflow for backtracking. It saves and restores the thread’s stack using an object called “Continuation”. | + | * As part of traversing all possible execution paths, BPmc uses Javaflow for backtracking. It saves and restores the thread’s stack using an object called “Continuation”. |
* The stack of a b-thread contains all non-static fields/variables of the b-thread class and all variables defined in-line in the runBThread method. | * The stack of a b-thread contains all non-static fields/variables of the b-thread class and all variables defined in-line in the runBThread method. | ||
* BPJ saves and restores objects (which are not on the stack) using serialization and deserialization. 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. | * BPJ saves and restores objects (which are not on the stack) using serialization and deserialization. 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. | ||
| Line 11: | Line 11: | ||
=Programming Tip 2= | =Programming Tip 2= | ||
| − | If you have objects that do not change from bt-state to bt-state, mark them as transient static (for the class or for the instance, as needed). Objects marked as transient are not processed by serialization. Deserialization resets them to initial value. | + | If you have objects that do not change from bt-state to bt-state, mark them as transient static (for the class or for the instance, as needed). Objects marked as transient are not processed by serialization. Deserialization resets them to initial value. |
=Programming Tip 3= | =Programming Tip 3= | ||
| − | If all the objects pointed to from the stack can be transient as defined above, you do not have to specify transient, and instead you can just specify static, and specify the run time parameter | + | If all the objects pointed to from the stack can be transient as defined above, you do not have to specify transient, and instead you can just specify static, and specify the run time parameter "–Dshallow=true" (the default is false). Then the when BPJ uses Javaflow to save and restore the stack(s) serialization and deserialization do not take place. |
Revision as of 12:55, 16 January 2014
Contents
- BPJ uses the package Javaflow to perform backtracking as needed for model checking
- Depending on the run mode, BPJ instruments the application for javaflow (the user may observe that some objects are instantiated twice – this should OK).
- As part of traversing all possible execution paths, BPmc uses Javaflow for backtracking. It saves and restores the thread’s stack using an object called “Continuation”.
- The stack of a b-thread contains all non-static fields/variables of the b-thread class and all variables defined in-line in the runBThread method.
- BPJ saves and restores objects (which are not on the stack) using serialization and deserialization. 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 Tip 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.
- Answer 2: 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 Tip 2
If you have objects that do not change from bt-state to bt-state, mark them as transient static (for the class or for the instance, as needed). Objects marked as transient are not processed by serialization. Deserialization resets them to initial value.
Programming Tip 3
If all the objects pointed to from the stack can be transient as defined above, you do not have to specify transient, and instead you can just specify static, and specify the run time parameter "–Dshallow=true" (the default is false). Then the when BPJ uses Javaflow to save and restore the stack(s) serialization and deserialization do not take place.
