Latest revision as of 08:41, 29 April 2014

BPJ Model Checking Parameters

Specifying Run Modes

BPJ model checking 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),.
• 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: 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.
• Nondeterminism specification: Allowed.
• Event selection: Random among all nondeterministic 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 nondeterministic choices.
• Nondeterminism 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 nondeterminism. The event selection mechanism always picks the first event that is requested and not blocked. It is the same as defining the priority delta for equal priority b-threads as zero.

-DrunMode=Learning/Training

(In development)

Run-control Parameters

-Dsearch=BFS or -Dsearch=DFS

Breadth-first or depth-first search.

-Drecursive=true

Depth first search by recursive calls instead of by a application-maintained stack

-DdisableStateHashing

BPJ will not recognize previously visited states.

-DestimatedStates

Control initial space allocation for state hashing

-DsuppressDeadlock=true

deadlocks will not cause a verification failure.

-DlogBacktracking=true

Issues a message with every visited BProgram state

-ea

Enable assertions. This standard Java JUnit parameter causes assertions in the code to be enabled and evaluated at run time, causing AssertionErrors when not true.

-noverify

Resolving Java7 compatibility issues with the bytecode instrumentation.

Memory Management Parameters

-DShallow=true/false

This parameter controls the serialization of objects not on the stack for backtracking during execution. See details in "Enabling your application for Model Checking".

-Xmn=,-Xms=,-Xmx=

These parameters are standard Java memory allocation parameters, and are used to define sufficient memory for large model-checking run. E.g.:

-Xmn200M
-Xms700M
-Xmx700M

Explanation:

• As Java starts, it creates within the systems memory a Java Virtual Machine (JVM). JVM is where the complete processing of any Java program takes place. All Java applications (including IQv6) by default allocate & reserve up to 64 MB of memory resource pool from the system on which it is running.
• The Xms is the initial / minimum Java memory (heap) size within the JVM. Setting the initial memory (heap) size higher can help in a couple of ways. First, it will allow garbage collection (GC) to work less which is more efficient. The higher initial memory value will cause the size of the memory (heap) not to have to grow as fast as a lower initial memory (heap) size, thereby saving the overhead of the Java VM asking the OS for more memory.
• The Xmx is the maximum Java memory (heap) size within the Java Virtual Memory (JVM). As the JVM gets closer to fully utilizing the initial memory, it checks the Xmx settings to find out if it can draw more memory from the system resources. If it can, it does so. For the JVM to allocate contiguous memory to itself is a very expensive operation. So as the JVM gets closer to the initial memory, the JVM will use aggressive garbage collection (to clean the memory and if possible avoid memory allocation), increasing the load on the system.
• If JVM is in need of memory beyond the value set in Xmx, the JVM will not be able to draw more memory from system resource (even if available) and run out of memory. Hence, the -Xms and -Xmx memory parameters should be increased depending upon the demand estimation of the system. Ideally both should be the same value (set at maximum possible as per demand estimation). This ensure that the maximum memory is allocated right at the start-up eliminating the need for extra memory allocation during program execution. It is sometimes recommended to use aggressive maximum memory (heap) size of between 1/2 and 3/4 of physical memory.
• -Xmn: the size of the heap for the young generation.

See more details in general Java reference information.

Application-specific parameters

You can pass parameters to your own application, and process them in standard Java techniques. E.g.,

• - nPhils=5 number of philosophers.
• leftyPhil=false is any of the philosophers left handed.

static int nPhils; // number of philosophers
static boolean leftyPhil = false; // Last Philosopher is left handed.
static {
nPhils = Integer.parseInt(System.getProperty("nPhils", "3"));
parmString += "nPhils=" + nPhils;
leftyPhil = (System.getProperty("leftyPhil","false").equals("true"));
parmString += ", leftyPhil=" + leftyPhil;
System.out.println(parmString);
}

Run Configuration Examples:

  -DrunMode=MCSafety
  -Drecursive=true
  -Dshallow=true
  -noverify

  -DrunMode=MCSafety
  -Dsearch=DFS
  -Xms300M
  -Xmx1000M
  -DestimatedStates=10000
  -DlogBacktracking=false
  -ea
  -noverify