Java Model Checker #

The Java Model Checker is a general purpose concurrent program correctness checker. It works by exploring different possible executions of the target program and checks the assertions at the end of each execution.

JMC is under active development, we are continuously adding support for concurrent primitives. If you encounter any errors, raise an issue here

Installation #

To use JMC, add the following maven dependency to the project.

testImplementation("org.mpi-sws.jmc:jmc:0.1.1")

Additionally, tests need to be configured to run with JMC. Use the JMC gradle plugin to ease the process.

plugins {
    id("org.mpi-sws.jmc.gradle") version "0.1.1"
}

The plugin is under review and awaiting publication. Refer to Complete Installation Guide for manual configuration.

Writing tests #

Once JMC is configured, you can start Writing Tests

How it works #

JMC works by first instrumenting the bytecode of the Java program and running it for many iterations under the JMC runtime. During each iteration, JMC imposes a co-operative multi-threading runtime on the threads created within the program. Specifically, each thread pauses at read, write, and other relevant events and yields control to the JMC runtime which decides the next thread to execute.

Refer here for a more detailed explanation and working of JMC’s internals.