Package org.mpi_sws.jmc.strategies.trust

Class Algo

java.lang.Object
org.mpi_sws.jmc.strategies.trust.Algo
public class Algo extends Object
Contains the core Trust algorithm implementation. () We implement the recursive version described in the paper and in the thesis. ()

This class contains, in addition to the execution graph and the algorithm, the auxiliary state needed to enforce a specific task scheduling order.

Disclaimer!! This algorithm assumes that the programs are deterministic. Meaning, if you run a task, you will receive the same sequence of events in that task.

  • Constructor Details

    • Algo

      public Algo()
      Creates a new instance of the Trust algorithm.

  • Method Details

    • nextTask

      public SchedulingChoice<?> nextTask()
      Returns the next task to be scheduled according to the execution graph set in place.

    • recordTaskSchedule

      public void recordTaskSchedule(String filePath) throws JmcCheckerException
      Records the task schedule generated by the execution graph to the specified filePath.
      Parameters:
      filePath - to record the task schedule in.
      Throws:
      JmcCheckerException

    • updateEvent

      public void updateEvent(Event event) throws HaltTaskException, HaltExecutionException
      Handles the visit with this event. Equivalent of running a single loop iteration of the Visit method of the algorithm.

      We assume that the updateEvent call is followed immediately by a yield call. Therefore, we check the top of a guiding trace and raise exception if the scheduling choice is blocking.

      Parameters:
      event - A Event that is used to update the execution graph.
      Throws:
      HaltTaskException
      HaltExecutionException

    • checkCoherencyEdges

      public boolean checkCoherencyEdges()

    • handleNoop

      public void handleNoop(Event event)
      Handles the NOOP event. This is a special case where we do not need to update the execution graph.
      Parameters:
      event - The NOOP event.

    • initIteration

      public void initIteration(int iteration, JmcModelCheckerReport report)
      Initializes the iteration. This method is called at the beginning of each iteration of the algorithm.
      Parameters:
      iteration - The iteration number.

    • teardown

      public void teardown()
      Cleans up the execution graph and the task schedule. This method is called at the end of the exploration.

    • getSchedulableTasks

      public List<Long> getSchedulableTasks()

    • handleLockAcquired

      public void handleLockAcquired(Event event)

    • logStackState

      public void logStackState()

    • writeExecutionGraphToFile

      public void writeExecutionGraphToFile(String filePath)
      Writes the execution graph to a file.
      Parameters:
      filePath - The path to the file to write the execution graph to.

    • getExecutionGraph

      public ExecutionGraph getExecutionGraph()