Package org.mpi_sws.jmc.runtime.scheduling

Class Scheduler

java.lang.Object
org.mpi_sws.jmc.runtime.scheduling.Scheduler
public class Scheduler extends Object
The scheduler is responsible for managing the execution of threads.

The scheduler uses the strategy to decide which thread to Schedule. To do so, it instantiates a separate SchedulerThread that is blocked whenever other threads are running and unblocked only when it needs to pick the next thread to schedule.

To interact with the scheduler, invoke the yield() which will defer control the scheduler thread.

  • Constructor Details

    • Scheduler

      public Scheduler(SchedulingStrategy strategy, int schedulerTries, long schedulerTrySleepTimeNanos)
      Constructs a new Scheduler object.
      Parameters:
      strategy - the scheduling strategy

  • Method Details

    • start

      public void start()
      Starts the scheduler thread.

    • init

      public void init(TaskManager taskManager, Long mainTaskId)
      Initializes the scheduler with the task manager and the main thread.
      Parameters:
      taskManager - the task manager
      mainTaskId - the ID of the main thread

    • initIteration

      public void initIteration(int iteration, JmcModelCheckerReport report) throws HaltCheckerException
      Initializes the strategy for a new iteration.
      Parameters:
      iteration - the number of the iteration
      Throws:
      HaltCheckerException

    • currentTask

      public Long currentTask()
      Returns the ID of the current task.
      Returns:
      the ID of the current task

    • setCurrentTask

      protected void setCurrentTask(Long taskId)
      Sets the ID of the current task.
      Parameters:
      taskId - the ID of the current task

    • scheduleTask

      protected <T extends SchedulingChoiceValue> void scheduleTask(SchedulingChoice<T> choice)
      Performs the scheduling choice (instance of SchedulingChoice) indicated. Either resuming the task, stopping the task or stopping all tasks.
      Parameters:
      choice - The scheduling choice to make.

    • updateEvent

      public void updateEvent(JmcRuntimeEvent event) throws HaltTaskException
      Updates the event in the scheduling strategy.
      Parameters:
      event - the event to be updated
      Throws:
      HaltTaskException

    • yield

      public CompletableFuture<?> yield() throws TaskAlreadyPaused
      Pauses the current task and yields the control to the scheduler.

      The call is non-blocking and returns immediately.

      Returns:
      a future that completes when the task is resumed
      Throws:
      TaskAlreadyPaused - if the current task is already paused

    • yield

      public CompletableFuture<?> yield(Long taskId) throws TaskAlreadyPaused
      Pauses the task with the given ID and yields the control to the scheduler.

      The call is non-blocking and returns immediately.

      Parameters:
      taskId - the ID of the task to be paused
      Returns:
      a future that completes when the task is resumed
      Throws:
      TaskAlreadyPaused - if the task is already paused

    • resetIteration

      public void resetIteration(int iteration)
      Resets the TaskManager and the scheduling strategy for a new iteration.

    • recordTrace

      public void recordTrace()

    • shutdown

      public void shutdown()
      Shuts down the scheduler.