Package org.mpi_sws.jmc.runtime

Class JmcRuntime

java.lang.Object
org.mpi_sws.jmc.runtime.JmcRuntime
public class JmcRuntime extends Object
The Runtime environment complete with a scheduler and configuration options used by the model checker.

Calls to the runtime are made by the instrumented byte code. These calls are used to record events occurring during the execution of tasks or allow for scheduling changes. For example, the runtime can be used to record Thread creation and deletion.

The runtime is a static class that stores minimal states and delegates calls to the Scheduler which retains all the state.

  • Constructor Details

    • JmcRuntime

      public JmcRuntime()

  • Method Details

    • setup

      public static void setup(JmcRuntimeConfiguration config)
      Sets up the runtime with the given configuration.
      Parameters:
      config - the configuration (instance of JmcRuntimeConfiguration)

    • setupReplay

      public static void setupReplay(JmcRuntimeConfiguration config) throws JmcCheckerException
      Throws:
      JmcCheckerException

    • tearDown

      public static void tearDown()
      Tears down the runtime by shutting down the scheduler adn clearing the task manager.

    • initIteration

      public static void initIteration(int iteration, JmcModelCheckerReport report)
      Initializes the runtime with the main thread for a given iteration.

      Initializes the scheduler with the main thread and marks it as ready.

      Parameters:
      iteration - the iteration number

    • resetIteration

      public static void resetIteration(int iteration)
      Resets the runtime for a new iteration.

    • recordTrace

      public static void recordTrace()

    • yield

      public static <T> T yield()
      Pauses the current task that invokes this method and yields the control to the scheduler. The call returns only when the task that invoked this method is resumed.

    • yield

      public static void yield(Long taskId) throws HaltTaskException, HaltExecutionException
      Pauses the task with the given ID and yields the control to the scheduler. The call returns only when the task with the given ID is resumed.

      Use with Caution! It is meant to be called when a new concurrent task starts and yields with the new task id. Should not be used otherwise.

      Parameters:
      taskId - the ID of the task to be paused
      Throws:
      HaltTaskException
      HaltExecutionException

    • pause

      public static void pause(Long taskId)
      Pauses the task.
      Parameters:
      taskId - the ID of the task to be paused

    • wait

      public static <T> T wait(Long taskId)

    • join

      public static void join(Long taskId)
      Updates the TaskManager to terminate the task with the given ID and yields control to the scheduler to schedule other tasks.
      Parameters:
      taskId - the ID of the task to be terminated

    • currentTask

      public static Long currentTask()
      Returns the current task id.
      Returns:
      the current task id

    • updateEvent

      public static void updateEvent(JmcRuntimeEvent event) throws HaltTaskException
      Adds a new event to the scheduler which is passed to the strategy.
      Parameters:
      event - to be added
      Throws:
      HaltTaskException

    • terminate

      public static void terminate(Long taskId)
      Terminates the task with the given ID.
      Parameters:
      taskId - the ID of the task to be terminated

    • updateEventAndYield

      public static <T> T updateEventAndYield(JmcRuntimeEvent event) throws HaltTaskException
      Adds a new event to the runtime and yields the control to the scheduler.
      Parameters:
      event - the new event
      Throws:
      HaltTaskException

    • addNewTask

      public static Long addNewTask()
      Adds a new task to the runtime and creates a future for that task.
      Returns:
      the ID of the new task