Nondetermism - Revision history

BpAdmin: /* Nondeterministic execution in BPmc */

2014-03-19T09:40:16Z

‎Nondeterministic execution in BPmc

Assaf: /* Nondeterministic execution in BPmc */

2014-02-11T13:37:30Z

‎Nondeterministic execution in BPmc

Assaf: /* Specifiying nondeterminism */

2014-02-11T13:01:28Z

‎Specifiying nondeterminism

Assaf: /* Specifiying nondeterminism */

2014-02-11T12:59:26Z

‎Specifiying nondeterminism

Assaf at 14:33, 4 August 2013

2013-08-04T14:33:46Z

Assaf at 14:02, 4 August 2013

2013-08-04T14:02:58Z

Assaf at 14:01, 4 August 2013

2013-08-04T14:01:40Z

Assaf at 13:47, 4 August 2013

2013-08-04T13:47:32Z

Assaf at 13:47, 4 August 2013

2013-08-04T13:47:14Z

Assaf at 13:41, 4 August 2013

2013-08-04T13:41:51Z

@@ Line 1: / Line 1: @@
-= Nondeterministic execution in BPmc =
+= Nondeterministic execution in BPJ model checking =
 In common processing event selection in BP is deterministic.
-However, in some cases it is desired to specify nondetermistic choices - e.g., when simulating environment behavior using b-threads as part of model checking. The BPmc model checker explores all possible execution paths defined by this nondeterminism.
+However, in some cases it is desired to specify nondetermistic choices - e.g., when simulating environment behavior using b-threads as part of model checking. The BPJ model checking capability explores all possible execution paths defined by this nondeterminism.
 In fact, often, the only non-determinism in execution is in b-threads that simulate the environment.
 == Specifiying nondeterminism ==
@@ Line 12: / Line 12: @@
 == Nondeterministic execution ==
-When executing in model-checking mode, nondetereministic event selection is performed according to the following algorithm :
+When executing in model-checking mode, nondeterministic event selection is performed according to the following algorithm :
 * Scan b-threads in order of priority
@@ Line 20: / Line 20: @@
 * If the event is in a first level of the requested event set, this event is the only one from this b-thread.
 * After exploring all execution subtrees anchored at the alternatives from one b-thread go to the next b-thread of “same” priority as defined with epsilon, and repeat the above . At most one second-level set will be selected from the requested events of that b-thread, but not necessarily the first one.
-* When all alternatives in a given execution path are explored the execution returns to the next higher level in the nondeterminstic execution path to select the next alternative at that level.
+* When all alternatives in a given execution path are explored the execution returns to the next higher level in the nondeterministic execution path to select the next alternative at that level.
-* BPmc uses the Java package javaflow to restore the stack of all b-threads in order to resume execution of another subtree at a previously visited synchronization point.
+* BPJ model checking uses the Java package javaflow to restore the stack of all b-threads in order to resume execution of another subtree at a previously visited synchronization point.
 == Programming Constraints ==
-* While in regular runs a b-thread can terminate,  in a MC run A b-thread should not terminate, to allow BPmc to bcaktrack. Precede/replace the return with bSync(none,none,none); In a regular run this will just terminate. In MC run it will allow the b-thread to backtrack from the end.
+* While in regular runs a b-thread can terminate,  in a MC run A b-thread should not terminate, to allow BPJ model checking to backtrack. Precede/replace the return with bSync(none,none,none); In a regular run this will just terminate. In MC run it will allow the b-thread to backtrack from the end.
 == Example ==

@@ Line 2: / Line 2: @@
 In common processing event selection in BP is deterministic.
 However, in some cases it is desired to specify nondetermistic choices - e.g., when simulating environment behavior using b-threads as part of model checking. The BPmc model checker explores all possible execution paths defined by this nondeterminism.
 == Specifiying nondeterminism ==
@@ Line 7: / Line 8: @@
 * When the difference in priority of two b-threads is less than a given "epsilon" (a real number provided by the user), the two b-threads  are considered of same priority.  For example, to create 48 bthreads of the same priority, choose epsilon of 1.00 and  create the set of these b-threads so that their priorities have the same whole part and differ only by fractional part.  (e.g. priority values of 7.001 – 7.048). The value of "epsilon" is determined by the method call setBthreadEpsilon().
 * Additionally, during model checking if an event in a requested event set of any b-thread is selected (requested and not blocked, and non-deterministic execution actually selected it), then if the event was in a nested second-level set, then all other events in the same nested second-level set are considered to be of the same priority. For example, if the requested even set is R={{e1,e2},e3,{e4,e5,e6,e7},e8} - then if e5 was selected (say, all preceding events were blocked), then e6 and e7, and only them are considered of the same priority and will be explored in non-deterministic execution. This priority processing is relevant only to the first event selection in b-thread. Once the selected second-level set is exhausted, (or if the event was a first level in the first place), non-deterministic execution continues with the next b-thread of the "same" priority as the previous b-thread.
 See execution below for more details.
 == Nondeterministic execution ==
@@ Line 22: / Line 23: @@
 * BPmc uses the Java package javaflow to restore the stack of all b-threads in order to resume execution of another subtree at a previously visited synchronization point.
 == Programming Constraints ==
 * While in regular runs a b-thread can terminate,  in a MC run A b-thread should not terminate, to allow BPmc to bcaktrack. Precede/replace the return with bSync(none,none,none); In a regular run this will just terminate. In MC run it will allow the b-thread to backtrack from the end.
 == Example ==

@@ Line 5: / Line 5: @@
 == Specifiying nondeterminism ==
 * In BP, event selection is deteremined by the unique priority of each b-thread, and by the order of events in the requested event set.
 * When the difference in priority of two b-threads is less than a given "epsilon" (a real number provided by the user), the two b-threads  are considered of same priority.  For example, to create 48 bthreads of the same priority, choose epsilon of 1.00 and  create the set of these b-threads so that their priorities have the same whole part and differ only by fractional part.  (e.g. priority values of 7.001 – 7.048). The value of "epsilon" is determined by the method call setBthreadEpsilon().
 * Additionally, during model checking if an event in a requested event set of any b-thread is selected (requested and not blocked, and non-deterministic execution actually selected it), then if the event was in a nested second-level set, then all other events in the same nested second-level set are considered to be of the same priority. For example, if the requested even set is R={{e1,e2},e3,{e4,e5,e6,e7},e8} - then if e5 was selected (say, all preceding events were blocked), then e6 and e7, and only them are considered of the same priority and will be explored in non-deterministic execution. This priority processing is relevant only to the first event selection in b-thread. Once the selected second-level set is exhausted, (or if the event was a first level in the first place), non-deterministic execution continues with the next b-thread of the "same" priority as the previous b-thread.
 == Nondeterministic execution ==
 When executing in model-checking mode, nondetereministic event selection is performed according to the following algorithm :

@@ Line 5: / Line 5: @@
 == Specifiying nondeterminism ==
 * In BP, event selection is deteremined by the unique priority of each b-thread, and by the order of events in the requested event set.
-* When the difference in priority of two b-threads is less than a given "epsilon" (a real number provided by the user), the two b-threads  are considered of same priority.  For example, to create 48 bthreads of the same priority, choose epsilon of 1.00 and  create the set of these b-threads so that their priorities have the same whole part and differ only by fractional part.  (e.g. priority values of 7.001 – 7.048). The value of "epsilon" is determined by
+* When the difference in priority of two b-threads is less than a given "epsilon" (a real number provided by the user), the two b-threads  are considered of same priority.  For example, to create 48 bthreads of the same priority, choose epsilon of 1.00 and  create the set of these b-threads so that their priorities have the same whole part and differ only by fractional part.  (e.g. priority values of 7.001 – 7.048). The value of "epsilon" is determined by the method call setBthreadEpsilon().
+* Additionally, during model checking if an event in a requested event set of any b-thread is selected (requested and not blocked, and non-deterministic execution actually selected it), then if the event was in a nested second-level set, then all other events in the same nested second-level set are considered to be of the same priority. For example, if the requested even set is R={{e1,e2},e3,{e4,e5,e6,e7},e8} - then if e5 was selected (say, all preceding events were blocked), then e6 and e7, and only them are considered of the same priority and will be explored in non-deterministic execution. This priority processing is relevant only to the first event selection in b-thread. Once the selected second-level set is exhausted, (or if the event was a first level in the first place), non-deterministic execution continues with the next b-thread of the "same" priority as the previous b-thread.
- . . .
 == Nondeterministic execution ==

@@ Line 23: / Line 23: @@
 * After exploring all execution subtrees anchored at the alternatives from one b-thread go to the next b-thread of “same” priority as defined with epsilon, and repeat the above . At most one second-level set will be selected from the requested events of that b-thread, but not necessarily the first one.
 * When all alternatives in a given execution path are explored the execution returns to the next higher level in the nondeterminstic execution path to select the next alternative at that level.
 * BPmc uses the Java package javaflow to restore the stack of all b-threads in order to resume execution of another subtree at a previously visited synchronization point.
 * Example

@@ Line 4: / Line 4: @@
 Setting up nondeterminism:
 * In BP, event selection is deteremined by the unique priority of each b-thread, and by the order of events in the requested event set.
 * When the difference in priority of two b-threads is less than a given "epsilon" (a real number provided by the user), the two b-threads  are considered of same priority.  For example, to create 48 bthreads of the same priority, choose epsilon of 1.00 and  create the set of these b-threads so that their priorities have the same whole part and differ only by fractional part.  (e.g. priority values of 7.001 – 7.048). The value of "epsilon" is determined by
   . . .
-−
+*
 * In a given requested-events set, events that are in the same second level event set are considered of same priority . E.g. in the requested event set R={a, {b,c,d},{e,f,g}}. b,c,d are considered of the same priority, and e,f,g are considered of the same priority.
-How BPJ determines non-detereministic selection :
+When executing in model-checking mode, nondetereministic event selection is performed according to the following algorithm :
 Scan b-threads in order of priority
-Scan the requested event set of each b-thread in event order (the set is enumerable.
+* Scan b-threads in order of priority
-When the first event that is requested and not blocked is found  it is one alternative.
+* Scan the requested event set of each b-thread in event order (the set is enumerable).
-If it  was in a  second level event set (a set within a set),  all its siblings in the same set are considered having the same priority, and are added as alternatives (if not blocked).   If it is in a first level of the requested event set, this event is the only one from this b-thread.
+* When the first event that is requested and not blocked is found  it is remembered as one alternative.
-When done with the alternatives from one b-thread (first requested and not blocked, and possibly its sibling in the second level set) –go to the next b-thread of “same” priority as defined with epsilon, and repeat the above . At most one second-level set will be selected from the requested events of that b-thread, but not necessarily the first one).
+* If the selected event was in a  second level event set (a set within a set),  all its siblings in the same second level set that are not blocked are considered having the same priority, and are added as alternatives.
-Example
+* If the event is in a first level of the requested event set, this event is the only one from this b-thread.