JMC internals #

Testing/verifying a program with JMC involves two steps. First, Instrumentation of the compiled bytecode and second, running the instrumented bytecode using JMC’s custom runtime.

Instrumentation #

JMC defines a custom Java Agent that instruments classes as they are loaded. The instrumentation inserts calls to JMC runtime at strategic points to capture the relevant event and pause the thread. For example, the agent instruments every GETFIELD and PUTFIELD instruction to present the read and write events to JMC runtime respectively.

Refer here for detailed documentation on the instrumentation process.

Runtime and model checking #

Once instrumented, the model checker runs the instrumented code using the specified strategy. The runtime accepts events from threads and maintains state of all paused threads. The events are passed to the strategy and threads are released as specified by the strategy.

Refer here for more detailed documentation of the JMC runtime.