Module dev.civl.gmc

Class DporHbSet

java.lang.Object
dev.civl.gmc.dpor.DporHbSet

public class DporHbSet extends Object
Maintains a set of stack entries which are downward closed wrt to the happens-before relation. Meaning: if e is in our set and e' happens before e then e' is also in our set. This class is the foundation for building the full happens-before relation. Essentially, each entry on the stack has an HbSet which represents the set of entries that happen-before it.
  • Constructor Details

    • DporHbSet

      public DporHbSet()
  • Method Details

    • addEntry

      public void addEntry(DporStackEntry<?,?> entry)
    • contains

      public boolean contains(DporStackEntry<?,?> entry)
      Parameters:
      index - of stack entry
      Returns:
      whether the entry is in this set
    • lastEntryPos

      public int lastEntryPos(int pid)
      Parameters:
      process - id
      Returns:
      the last stack entry of pid that is in this set if it exists; -1 if it does not
    • procSet

      public Set<Integer> procSet()
      Returns:
      the set of process ids that have stack entries in this set