JavaFlow
From BP Wiki
BPmc Internals: BPmc and the Javaflow package
- 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 “==“ between objects that are part of the state. Instead, use the equals() method. A default equals() method based on object ids already exists for events.
- 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?
