JMC runtime #

The JMC runtime imposes co-operative multi-threading semantics on the target program. It does so by capturing the creation and deletion of every concurrent computation (Threads, futures, etc…). We will refer to each concurrent computation as a task henceforth. Each task is paused by waiting on a temporary CompletableFuture.

Concurrently, the runtime initiates a separate scheduling thread that interacts with the SchedulingStrategy. Each time a task yields, the scheduler thread runs for a single iteration where it fetches the next task to resume from the strategy.

The implementation of the runtime and the auxiliary helper classes are defined in the org.mpi_sws.jmc.runtime package. Below we list a few key classes that capture the core behavior.

JmcRuntime #

The main runtime class that only contains static state and methods. Two primary calls of the runtime are invoked by concurrent computation to allow task switching.

1. JmcRuntime.updateEvent to inform the runtime of an event. Events are interesting points at which task switching can take place. (E.g. Thread creation, joins, synchronized method entry and exit.)
2. JmcRuntime.yield called to pause execution and yield control to the runtime scheduler.

Refer to the API docs

JmcRuntimeEvent #

Defines the structure of events that occur prior to yield calls. The attributes are,

1. type - Event type
2. taskId - the identifier of task invoking the event
3. params - All additional params of the event

Scheduler #

JmcRuntime initializes a scheduling thread that is responsible for interacting with the strategy to decide the task execution order. Each choice is represented by SchedulingChoice.