Difference between revisions of "JavaFlow"

From BP Wiki
Jump to: navigation, search
(New page: =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 ob...)
 
(→‎Enabling your application for model checking)
 
(16 intermediate revisions by one user not shown)
Line 1: Line 1:
−
=BPmc and JavaFlow=
+
=Enabling your application for model checking=
−
BPJ uses the package javaflow to perform backtracking as needed 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.
−
Depending on the run mode, BPJ instrument the application for javaflow�(user may observe that some objects are instantiated twice – this should OK).  
+
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.
−
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.  
+
= Programming Requirement 1=
−
The stack does not contain objects.
+
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.
−
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.  
+
=Programming Requirement 2=
−
Serialization translates each field and each object pointed to from the Continuation into a bitstream.  
+
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.
−
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.
+
=Programming Tip=
−
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.
+
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.
 +
 
 +
 
 +
[[Image:Dshallow.png | 600px | <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>]]
 +
 
 +
 
 +
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.

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.


Object serialization


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.

Retrieved from "https://wiki.weizmann.ac.il/bp/index.php?title=JavaFlow&oldid=224"