BpAdmin: /* Nondeterministic execution in BPJ model checking */

2014-03-19T09:47:52Z

‎Nondeterministic execution in BPJ model checking

Assaf: New page: = Nondeterministic execution in BPmc = In common processing event selection in BP is deterministic. However, in some cases it is desired to specify nondetermistic choices - e.g., when simu...

2013-08-04T14:13:40Z

New page: = Nondeterministic execution in BPmc = In common processing event selection in BP is deterministic. However, in some cases it is desired to specify nondetermistic choices - e.g., when simu...

New page

= Nondeterministic execution in BPmc =
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 ==
* 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

. . .

== Nondeterministic execution ==

* 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.

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).
* When the first event that is requested and not blocked is found it is remembered as one alternative.
* 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.
* 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.
* 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 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. Model checking explores all possible execution paths defined by this nondeterminism.
 == Specifiying nondeterminism ==
@@ 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.
+* 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.
 * Example

Nondeterminism - Revision history

BpAdmin: /* Nondeterministic execution in BPJ model checking */

Assaf: New page: = Nondeterministic execution in BPmc = In common processing event selection in BP is deterministic. However, in some cases it is desired to specify nondetermistic choices - e.g., when simu...