Difference between revisions of "MCInstrumentation"

From BP Wiki
Jump to: navigation, search
(New page: = Application Instrumentation and Assistance in BPmc The following API calls can be used inside Java b-thread to control the model checking process. Throughout, the term nextVerification...)
 
Line 1: Line 1:
 
= Application Instrumentation and Assistance in BPmc
 
= Application Instrumentation and Assistance in BPmc
  
The following API calls can be used inside Java b-thread to control the model checking process.  
+
The following API calls can be used inside Java b-thread to control the model checking process.
Throughout, the term nextVerificationState refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.  
+
Throughout, the term nextVerificationState refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.
  
== markNextVerificationStateAsBad() ==  
+
== markNextVerificationStateAsBad() ==
* Indicates safety property violation. MC stops and prints a counterexample.  
+
* Indicates safety property violation. MC stops and prints a counterexample.
  
== markNextVerificationStateAsHot() ==  
+
== markNextVerificationStateAsHot() ==
* Used for liveness property checking. BPmc looks for reachable cycles that contains only hot states (and no cold states). By default, states are considered cold.
+
* Used for liveness property checking. BPmc looks for reachable cycles that contains only hot states (and no cold states). By default, states are considered cold.
  
== pruneSearchNow()  
+
== pruneSearchNow()
  
- forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined
+
* Forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined.
pruneAtNextVerificationState()  - forces backtracking �after all b-threads reach the next state and after its badness is determined.
+
 
labelNextVerificationState(…): optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states).  
+
== pruneAtNextVerificationState()   
When BPmc reaches a state that was already fully checked – it backtracks.
+
* forces backtracking after all b-threads reach the next state and after its badness is determined.
If b-thread doesn’t label its states – it is considered to have one state – and it doesn’t increase the size of the Cartesian product.
+
 
While in regular runs a b-thread can terminate,  in a MC run A b-thread should not terminate. 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.
+
== labelNextVerificationState(…):  
 +
* Optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states - creating their Cartesian product).
 +
* When BPmc reaches a BP-state that was already fully checked – it backtracks.
 +
* If a b-thread does not label any of its states – it is considered to have one state – and it does not increase the size of the Cartesian product.

Revision as of 14:32, 4 August 2013

= Application Instrumentation and Assistance in BPmc

The following API calls can be used inside Java b-thread to control the model checking process. Throughout, the term nextVerificationState refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.

markNextVerificationStateAsBad()

  • Indicates safety property violation. MC stops and prints a counterexample.

markNextVerificationStateAsHot()

  • Used for liveness property checking. BPmc looks for reachable cycles that contains only hot states (and no cold states). By default, states are considered cold.

== pruneSearchNow()

  • Forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined.

== pruneAtNextVerificationState()

  • forces backtracking after all b-threads reach the next state and after its badness is determined.

== labelNextVerificationState(…):

  • Optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states - creating their Cartesian product).
  • When BPmc reaches a BP-state that was already fully checked – it backtracks.
  • If a b-thread does not label any of its states – it is considered to have one state – and it does not increase the size of the Cartesian product.