Difference between revisions of "Nondetermism"
From BP Wiki
(→Specifiying nondeterminism) |
(→Nondeterministic execution in BPmc) |
||
| Line 2: | Line 2: | ||
In common processing event selection in BP is deterministic. | 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 BPmc model checker 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 == | == 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(). | * 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. | * 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. | + | See execution below for more details. |
== Nondeterministic execution == | == 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. | * 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 == | + | == 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 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 == | == Example == | ||
Revision as of 13:37, 11 February 2014
Contents
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. In fact, often, the only non-determinism in execution is in b-threads that simulate the environment.
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.
See execution below for more details.
Nondeterministic execution
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.
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.
