Difference between revisions of "Nondetermism"
From BP Wiki
(New page: 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-th...) |
|||
| Line 1: | Line 1: | ||
| − | 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. |
| − | Setting up nondeterminism: | + | 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). | + | * 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. |
| − | * 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 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). |
| + | * 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 : | How BPJ determines non-detereministic selection : | ||
| − | Scan b-threads in order of priority | + | Scan b-threads in order of priority |
| − | Scan the requested event set of each b-thread in event order (the set is enumerable. | + | 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 one alternative. | + | When the first event that is requested and not blocked is found it is one alternative. |
| − | 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. | + | 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 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). | 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). | ||
Example | Example | ||
Revision as of 13:40, 4 August 2013
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.
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).
- 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 : 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 one alternative. 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 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). Example
