JavaFlow
BPmc and JavaFlow
BPJ uses the package javaflow to perform backtracking as needed for model checking Depending on the run mode, BPJ instrument the application for javaflow�(user may observe that some objects are instantiated twice – this should OK). Backtracking uses javaflow to (save and) restore 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 runBThread. The stack does not contain objects. Problem 1: what if a stack variable was a pointer to an object that is not on the stack? - how do we keep them synchronized, or (in other words), what 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 bitstream. Deserialization turns such bit streams into program objects. Problem 2: When two pointers on the stack point to the same object, after deserialization we have two copies of the object. Answer 2: Do not use “==“ between objects that are part of the state. Instead – use equals() method. A default equals() method based on object ids already exists for events.
