Difference between revisions of "RunMode"

From BP Wiki
Jump to: navigation, search
Line 10: Line 10:
 
* Backtracking: none.
 
* Backtracking: none.
 
* Stops: When all b-threads end, or when there are no enabled events.
 
* Stops: When all b-threads end, or when there are no enabled events.
 +
 +
== -DrunMode=MCSafety ==
 +
* Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties.
 +
* Use: Model checking: explore safety properties (including deadlocks), discover desired paths, etc.
 +
* Nondeterminism specification: Allowed (actually required by definition).
 +
* Event selection: Systematically makes all possible combinations of event selections
 +
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
 +
* Stops:  When counterexample is found, or when verification of all transitions / states is complete.
 +
* Additional related parameters: -Dsearch=BFS/DFS,  -Drecursive=true/false
 +
 +
== -DrunMode=MCLiveness ==
 +
* Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions.
 +
* Use: Model checking for liveness properties - (with fairness assumptions),.
 +
* Non-determinism specification: Allowed (actually required by definition).
 +
* Event selection: Systematically makes all possible combinations of event selections.
 +
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
 +
Stops:  When counterexample is found, or when verification of all transitions / states is complete.
 +
* Additional related parameters:  Conditional, strong and weak fairness assumptions provided as sets of events
  
 
== -DrunMode=Random ==
 
== -DrunMode=Random ==
Line 28: Line 46:
 
* Stops: When the last run of all possible runs  ends (all possible combinations of event selections exhausted).
 
* Stops: When the last run of all possible runs  ends (all possible combinations of event selections exhausted).
  
== -DrunMode=MCSafety ==
+
== -DrunMode=MCDet ==
* Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties.
+
Description: A deterministic run, with model-checking instrumentation. No non-determinism. Always pick 1st event that is requested and not blocked. See [[MCInstrumentation | Application Assistance and Instrumentation for BPmc]]
* Use: Model checking: explore safety properties (including deadlocks), discover desired paths, etc.
+
* Nondeterminism specification: Allowed (actually required by definition).
+
* Event selection: Systematically makes all possible combinations of event selections
+
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
+
* Stops:  When counterexample is found, or when verification of all transitions / states is complete.
+
* Additional related parameters: -Dsearch=BFS/DFS,  -Drecursive=true/false
+
 
+
 
+
== -DrunMode=MCLiveness ==
+
* Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions.
+
* Use: Model checking for liveness properties - (with fairness assumptions),.
+
* Non-determinism specification: Allowed (actually required by definition).
+
* Event selection: Systematically makes all possible combinations of event selections.
+
* Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]].
+
Stops:  When counterexample is found, or when verification of all transitions / states is complete.
+
* Additional related parameters:  Conditional, strong and weak fairness assumptions provided as sets of events
+
 
+
== -DrunMode=MCDet ==  
+
Description: A deterministic run, with model-checking instrumentation. No non-determinism. Always pick 1st event that is requested and not blocked. See [[MCInstrumentation | Application Assistance and Instrumentation for BPmc]]  
+
  
== -DrunMode=Learning/Training ==  
+
== -DrunMode=Learning/Training ==
 
(In development)
 
(In development)

Revision as of 14:19, 4 August 2013

Specifying Run Modes

BPmc is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows:

-DrunMode=Det

  • Description: “Normal” / standard / deterministic run.
  • Use: when you want the program to “do something”.
  • Nondeterminism specification: Ignored. All priorities are considered distinct.
  • Event Selection: Always the first requested event that is not blocked.
  • Backtracking: none.
  • Stops: When all b-threads end, or when there are no enabled events.

-DrunMode=MCSafety

  • Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties.
  • Use: Model checking: explore safety properties (including deadlocks), discover desired paths, etc.
  • Nondeterminism specification: Allowed (actually required by definition).
  • Event selection: Systematically makes all possible combinations of event selections
  • Backtracking: systematic as part of exploring the state-graph - as described in section on nondetermism.
  • Stops: When counterexample is found, or when verification of all transitions / states is complete.
  • Additional related parameters: -Dsearch=BFS/DFS, -Drecursive=true/false

-DrunMode=MCLiveness

  • Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions.
  • Use: Model checking for liveness properties - (with fairness assumptions),.
  • Non-determinism specification: Allowed (actually required by definition).
  • Event selection: Systematically makes all possible combinations of event selections.
  • Backtracking: systematic as part of exploring the state-graph - as described in section on nondetermism.

Stops: When counterexample is found, or when verification of all transitions / states is complete.

  • Additional related parameters: Conditional, strong and weak fairness assumptions provided as sets of events

-DrunMode=Random

  • Description: One possible run out of many.
  • Use: Demonstration or manual exploration of different possible runs.
  • Non-determinism specification: Allowed.
  • Event selection: Random among all non-deterministic choices.
  • Backtracking: none.
  • Stops: When all b-threads end, or when there are no enabled events.
  • Additional related parameters: -DrandomSeed= nnnn.

-DrunMode=Iter

  • Description: An iterative run – explore all possible executions.
  • Use: to assess traces and results of all possible runs resulting from non-deterministic choices.
  • Non-determinism specification: Allowed.
  • Event selection: Systematically makes all possible combinations of event selections - in different runs.
  • Backtracking: When a run ends , it is restarted , and a new combination of event selections is used - from the beginning - not at the next higher nondeterminstic choice.
  • Stops: When the last run of all possible runs ends (all possible combinations of event selections exhausted).

-DrunMode=MCDet

Description: A deterministic run, with model-checking instrumentation. No non-determinism. Always pick 1st event that is requested and not blocked. See Application Assistance and Instrumentation for BPmc

-DrunMode=Learning/Training

(In development)