Difference between revisions of "JavaFlow"
From BP Wiki
| Line 1: | Line 1: | ||
| − | =BPmc Internals: BPmc and the Javaflow package= | + | =BPmc Internals: BPmc and the Javaflow package, and related programming constraints= |
* 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). | ||
| Line 7: | Line 7: | ||
** Answer 1: BPJ serializes the Continuation. 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. | ** Answer 1: BPJ serializes the Continuation. 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. | ||
* Problem 2: 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. | * Problem 2: 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 “==“ | + | ** 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. |
Revision as of 11:52, 16 January 2014
- 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.
- Problem 1: The stack does not contain objects. What happens when a stack variable is a pointer to an object that is not on the stack? - how does BPmc keep the two synchronized, or, in other words, what happens if the state of a b-thread also depends on an object?
- Answer 1: BPJ serializes the Continuation. 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.
- Problem 2: 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.
