JavaFlow - Revision history

BpAdmin: /* Enabling your application for model checking */

2014-03-19T09:49:01Z

‎Enabling your application for model checking

Assaf: /* Programming Tip */

2014-02-11T13:15:48Z

‎Programming Tip

Assaf at 13:15, 11 February 2014

2014-02-11T13:15:23Z

Assaf at 14:42, 16 January 2014

2014-01-16T14:42:43Z

Assaf at 14:42, 16 January 2014

2014-01-16T14:42:24Z

Assaf at 14:42, 16 January 2014

2014-01-16T14:42:07Z

Assaf at 14:39, 16 January 2014

2014-01-16T14:39:35Z

Assaf at 14:37, 16 January 2014

2014-01-16T14:37:41Z

Assaf: /* Programming requirements for model checking */

2014-01-16T14:33:42Z

‎Programming requirements for model checking

Assaf at 13:14, 16 January 2014

2014-01-16T13:14:58Z

@@ Line 1: / Line 1: @@
 =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 processing by BPmc.
+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, BPmc 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 BPmc 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.
+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=

@@ Line 17: / Line 17: @@
 Example:
 Examine the code snippet below:
     Integer x = new Integer(5);
@@ Line 25: / Line 25: @@
     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
+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.

← Older revision		Revision as of 13:15, 11 February 2014
Line 15:		Line 15:

	[[Image:Dshallow.png \| 600px \| <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>]]		[[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.

← Older revision		Revision as of 14:42, 16 January 2014
Line 14:		Line 14:


−	[[Image:Dshallow.png \| ~~800px~~ \| <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>]]	+	[[Image:Dshallow.png \| 600px \| <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>]]

← Older revision		Revision as of 14:42, 16 January 2014
Line 14:		Line 14:


−	[[Image:Dshallow.png \| ~~400px~~ \| <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>]]	+	[[Image:Dshallow.png \| 800px \| <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>]]

← Older revision		Revision as of 14:39, 16 January 2014
Line 14:		Line 14:


−	[[Image:Dshallow.png \| frame \| <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>~~]]\| Dshallow.png~~]]	+	[[Image:Dshallow.png \| frame \| <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>]]

← Older revision		Revision as of 14:37, 16 January 2014
Line 14:		Line 14:


−	[[~~image~~ \| Dshallow.png]]	+	[[Image:Dshallow.png \| frame \| <span style="color: rgb(0, 128, 128);"><span style="font-family: Tahoma;"> Object serialization</span> </span>]]\| Dshallow.png]]

@@ Line 1: / Line 1: @@
 =Programming requirements 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 processing by BPmc.
 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, BPmc 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 BPmc 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.
@@ Line 12: / Line 12: @@
 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.