Package org.mpi_sws.jmc.strategies.trust

Class ExecutionGraph

java.lang.Object
org.mpi_sws.jmc.strategies.trust.ExecutionGraph
public class ExecutionGraph extends Object
Represents an execution graph.

Contains the exploration and all the relations defined according to the Trust algorithm. For now this class implements the sequential consistency model. Which, in theory, could be extended to other models.

Some terminology to understand the code

  • TO: Total order of events observed in this execution graph, in the order they were added
  • PO: Program order. A union of reads from partial order and the total order of events per task
  • RF: Reads from relation between reads and writes
  • CO: A coherency order between writes

  • Constructor Details

    • ExecutionGraph

      public ExecutionGraph()
      Initializes a new execution graph.

  • Method Details

    • getTaskSchedule

      public static List<SchedulingChoiceWrapper> getTaskSchedule(List<ExecutionGraphNode> taskEvents)
      Generate a task Schedule from a given sorted list of event nodes.

      Note that the generated Schedule involves tasks that are 1-indexed and The trust ExecutionGraph has tasks that are 0-indexed.

      Parameters:
      taskEvents - A sorted list of event nodes
      Returns:
      A list of SchedulingChoiceWrappers.

    • getUnblockedTasks

      public ArrayList<Integer> getUnblockedTasks()
      Returns the list of task identifiers in the execution graph where a new event can be added.
      Returns:
      The list of task identifiers in the execution graph.

    • getTOIndex

      protected int getTOIndex(ExecutionGraphNode node)
      Returns the index of the given node in the TO order.
      Parameters:
      node - The node to get the index of.
      Returns:
      The index of the given node in the TO order (-1 if not found).

    • getTOIndex

      protected int getTOIndex(Event.Key key)
      Returns the index of the given key in the TO order.
      Parameters:
      key - The key to get the index of.
      Returns:
      The index of the given key in the TO order (-1 if not found).

    • clone

      public ExecutionGraph clone()
      Creates a clone of the execution graph.
      Overrides:
      clone in class Object
      Returns:
      A clone of the execution graph.

    • hasEventNode

      public boolean hasEventNode(Event.Key key)
      Returns true if the execution graph has an event node with the given key.
      Parameters:
      key - The key of the event to check.
      Returns:
      True if the execution graph has an event node with the given key.

    • getEventNode

      public ExecutionGraphNode getEventNode(Event.Key key) throws NoSuchEventException
      Returns the event node with the given key.
      Parameters:
      key - The key of the event to get.
      Returns:
      The event node with the given key.
      Throws:
      NoSuchEventException - If the event with the given key is not found.

    • contains

      public boolean contains(Event.Key key)
      Returns true if the execution graph contains the event with the given key.
      Parameters:
      key - The key of the event to check.
      Returns:
      True if the execution graph contains the event with the given key.

    • addEvent

      public ExecutionGraphNode addEvent(Event event)
      Adds an event to the execution graph.
      Parameters:
      event - The event to add.
      Returns:
      The node representing the added event.

    • trackThreadJoins

      public void trackThreadJoins(ExecutionGraphNode node)
      Tracks thread join events in the execution graph. Adds a thread join edge from the last event of the joined task to the thread join event.
      Parameters:
      node - The node representing the thread join event.

    • trackThreadCreates

      public void trackThreadCreates(ExecutionGraphNode node)
      Tracks the thread starts in the execution graph as a total order

      Internally, it uses a special location in the coherency Order to maintain the total order. Additionally, the relation is part of _porf_ and is reflected in the happens before.

      Parameters:
      node - The node representing the thread start event.

    • trackThreadStarts

      public void trackThreadStarts(ExecutionGraphNode node)

    • addBlockingLabel

      public void addBlockingLabel(Long taskId)
      Adds a blocking label to the execution graph.
      Parameters:
      taskId - The task ID to add the blocking label for.

    • isTaskBlocked

      public boolean isTaskBlocked(Long taskId)
      Checks if the task with the given ID is blocked.
      Parameters:
      taskId - The task ID to check.
      Returns:
      True if the task with the given ID is blocked.

    • unBlockTask

      public void unBlockTask(Long taskId) throws HaltCheckerException
      Unblocks the task with the given ID.
      Parameters:
      taskId - The task ID to block.
      Throws:
      HaltCheckerException - If the task ID is invalid.

    • getCoMax

      public ExecutionGraphNode getCoMax(Integer location)
      Returns the last write event to the given location.
      Parameters:
      location - The location to get the last write event for.
      Returns:
      The last write event to the given location.

    • getAlternativeWrites

      public List<ExecutionGraphNode> getAlternativeWrites(ExecutionGraphNode read)
      Returns the alternative writes (in reverse CO order) to the given read event.

      All writes that are not _porf_-before the given read. (Tied to Sequential consistency model) ecluding the CO max write.

      Parameters:
      read - The read event node.
      Returns:
      The alternative writes to the given read event.

    • getAlternativeLockReads

      public List<ExecutionGraphNode> getAlternativeLockReads(ExecutionGraphNode write)
      Returns the alternative reads to the given write event.

      All reads that are not _porf_-before the given write. Specifically looking for lock acquire reads. In the search, the concurrent writes do not include lock acquire exclusive writes.

      Parameters:
      write - The write event node.
      Returns:
      The alternative reads to the given write event.

    • getAlternativeLockWrites

      public List<ExecutionGraphNode> getAlternativeLockWrites(ExecutionGraphNode read)
      Returns the potential alternative writes to the given lock read.

      Writes that other lock reads are reading from.

      Parameters:
      read - The write event node.
      Returns:
      The potential writes to the given read event.

    • getPotentialReads

      public List<ExecutionGraphNode> getPotentialReads(ExecutionGraphNode write)
      Returns the potential alternative reads to the given write event.

      All reads that are not _porf_-before the given write.

      Parameters:
      write - The write event node.
      Returns:
      The potential reads to the given write event.

    • revisitView

      public BackwardRevisitView revisitView(ExecutionGraphNode write, ExecutionGraphNode read)
      Constructs a backward revisit view of the ExecutionGraph.
      Parameters:
      write - The write event
      read - The read event that the write needs to backward revisit
      Returns:
      The backward revisit view of the ExecutionGraph

    • getWrites

      public List<ExecutionGraphNode> getWrites(Integer location)
      Returns the writes to the given location.
      Parameters:
      location - The location to get the writes for.
      Returns:
      The writes to the given location.

    • getAllWrites

      public List<ExecutionGraphNode> getAllWrites()
      Returns all the writes in the execution graph.
      Returns:
      All the writes in the execution graph.

    • swapCoherency

      public void swapCoherency(ExecutionGraphNode write1, ExecutionGraphNode write2)
      Resets the coherency order between the given write events. The later write is added just before the earlier write.

      Invalidates the total order of events in the graph. The concern of fixing the total order is passed to the calling function.

      Parameters:
      write1 - The first write event.
      write2 - The second write event.

    • getCoherentPlacings

      public List<ExecutionGraphNode> getCoherentPlacings(ExecutionGraphNode write)
      Returns the coherency placings of the given write event under sequential consistency.

      Writes that are not _porf_-before the given write event. (Tied to Sequential consistency model)

      Parameters:
      write - The write event.
      Returns:
      The coherency placings of the given write event.

    • changeReadsFrom

      public void changeReadsFrom(ExecutionGraphNode read, ExecutionGraphNode write)
      Updates the reads from relation between the given read and write events.

      Invalidates the total order and the vector clocks of events in the graph. The concern of fixing the total order and the vector clocks is passed to the calling function.

      Parameters:
      read - The read event.
      write - The write event.

    • setReadsFrom

      public void setReadsFrom(ExecutionGraphNode read, ExecutionGraphNode write)
      Sets the reads from relation between the given read and write events.

      Does not validate if there is an existing reads-from edge to the corresponding read

      Parameters:
      read - The read event.
      write - The write event.

    • trackCoherency

      public void trackCoherency(ExecutionGraphNode write)
      Tracks the coherency order between the given write event and the previous write event to the same location.
      Parameters:
      write - The write event.

    • restrictBySet

      public void restrictBySet(Set<Event.Key> set)

    • recomputeVectorClocks

      public void recomputeVectorClocks()
      Recomputes the vector clocks of all nodes in the execution graph.

    • restrict

      public void restrict(ExecutionGraphNode restrictingNode)

    • iterator

      public List<ExecutionGraphNode> iterator() throws ExecutionGraph.TopologicalSorter.GraphCycleException
      Returns an iterator walking through the nodes in a topological sort order.
      Throws:
      ExecutionGraph.TopologicalSorter.GraphCycleException

    • unsafeIterator

      public List<ExecutionGraphNode> unsafeIterator()
      Returns List of nodes while silently ignoring any errors with cycles *

    • checkExtensiveConsistency

      public boolean checkExtensiveConsistency()

    • checkReadsFromEdges

      public boolean checkReadsFromEdges()

    • checkConsistency

      public List<ExecutionGraphNode> checkConsistency()

    • checkDanglingEdges

      public void checkDanglingEdges()

    • checkConsistencyAndTopologicallySort

      public List<ExecutionGraphNode> checkConsistencyAndTopologicallySort()

    • isEmpty

      public boolean isEmpty()
      Returns true if the graph contains only the initial event.

    • clear

      public void clear()
      Clears the execution graph.

    • toJsonString

      public String toJsonString()

    • toJsonStringIgnoreLocation

      public String toJsonStringIgnoreLocation()

    • printCO

      public void printCO()

    • equals

      public boolean equals(Object o)
      Overrides:
      equals in class Object

    • checkCoherencyEdges

      public boolean checkCoherencyEdges()

    • trackThreadJoinCompletion

      public void trackThreadJoinCompletion(ExecutionGraphNode eventNode)

    • blockTaskForLock

      public void blockTaskForLock(Event event)

    • unblockAllTasksForLock

      public void unblockAllTasksForLock(Integer location)

    • acquireLock

      public void acquireLock(Integer location, Long taskId)

    • waitingForLock

      public boolean waitingForLock(Integer location, Long taskId)

    • printGraph

      public void printGraph()

    • isRfConsistent

      public boolean isRfConsistent()