Strategies #

When testing a program under JMC, the threads of the program are controlled by a custom runtime such that all but one thread is executing at any given point in time. The threads yield at specific points and the runtime refers to the strategy to decide the next thread to allow executing. JMC provides a range of inbuilt strategies.

Random strategy #

This is the default strategy used if none is specified.

A pure random strategy where JMC tests the program by choosing the next “available” thread at random. Availability ensures that only threads that do not block are allowed to be executed. For example, a thread A waiting to join on another thread B will not be allowed to execute until thread B is finished.

The seed parameter of JmcCheckConfiguration defines the seed that is used by the random strategy.

Trust strategy #

JMC uses an optimized version of the model checking procedure from the paper “Truly stateless, optimal dynamic partial order reduction”

The strategy iteratively explores the optimal number of executions required to explore all possible behaviors. Specify trust as the strategy type in JmcCheckConfiguration to use the strategy with default parameters.

Alternatively, use the JmcTrustStrategy annotation to specify the scheduling strategy used within Trust. Turning on the debug flag within JmcTrustStrategy records the execution graphs to the report path.

Measure Graph coverage strategy #

Trust explores different executions by mapping each execution to a graph (execution graphs). JMC provides a no-op strategy that measures the number of execution graphs covered. Use JmcMeasureGraphCoverage annotation to enable coverage measurement.

The coverage can be measured, either per-iteration or polled with a fixed frequency.

Custom strategies #

Apart from the standard strategies, users are free to define custom exploration strategies to test Java programs. Refer here for detailed documentation.