scfence/inferset.h

   1 #ifndef _INFERSET_H
   2 #define _INFERSET_H
   3
   4 #include "fence_common.h"
   5 #include "patch.h"
   6 #include "inference.h"
   7 #include "inferlist.h"
   8
   9 typedef struct inference_stat {
  10         int notAddedAtFirstPlace;
  11
  12         inference_stat() :
  13                 notAddedAtFirstPlace(0) {}
  14
  15         void print() {
  16                 model_print("Inference process statistics output:...\n");
  17                 model_print("The number of inference not added at the first place: %d\n",
  18                         notAddedAtFirstPlace);
  19         }
  20 } inference_stat_t;
  21
  22
  23 /** Essentially, we have to explore a big lattice of inferences, the bottom of
  24  *  which is the inference that has all relaxed orderings, and the top of which
  25  *  is the one that has all SC orderings. We define the partial ordering between
  26  *  inferences as in compareTo() function in the Infereence class. In another
  27  *  word, we compare ordering parameters one by one as a vector. Theoretically,
  28  *  we need to explore up to the number of 5^N inferences, where N denotes the
  29  *  number of wildcards (since we have 5 possible options for each memory order).
  30
  31  *  We try to reduce the searching space by recording whether an inference has
  32  *  been discovered or not, and if so, we only need to explore from that
  33  *  inference for just once. We can use a set to record the inferences to be be
  34  *  explored, and insert new undiscovered fixes to that set iteratively until it
  35  *  gets empty.
  36
  37  *  In detail, we use the InferenceList to represent that set, and use a
  38  *  LIFO-like actions in pushing and popping inferences. When we add an
  39  *  inference to the stack, we will set it to leaf or non-leaf node. For the
  40  *  current inference to be added, it is non-leaf node because it generates
  41  *  stronger inferences. On the other hands, for those generated inferences, we
  42  *  set them to be leaf node. So when we pop a leaf node, we know that it is
  43  *  not just discovered but thoroughly explored. Therefore, when we dicide
  44  *  whether an inference is discovered, we can first try to look up the
  45  *  discovered set and also derive those inferences that are stronger the
  46  *  explored ones to be discovered.
  47
  48  ********** The main algorithm **********
  49  Initial:
  50         InferenceSet set; // Store the candiates to explore in a set
  51         Set discoveredSet; // Store the discovered candidates. For each discovered
  52                 // candidate, if it's explored (feasible or infeasible, meaning that
  53                 // they are already known to work or not work), we set it to be
  54                 // explored. With that, we can reduce the searching space by ignoring
  55                 // those candidates that are stronger than the explored ones.
  56         Inference curInfer = RELAX; // Initialize the current inference to be all relaxed (RELAX)
  57
  58  API Methods:
  59         bool addInference(infer, bool isLeaf) {
  60                 // Push back infer to the discovered when it's not discvoerd, and return
  61                 // whether it's added or not
  62         }
  63
  64         void commitInference(infer, isFeasible) {
  65                 // Set the infer to be explored and add it to the result set if feasible
  66         }
  67
  68         Inference* getNextInference() {
  69                 // Get the next unexplored inference so that we can contine searching
  70         }
  71 */
  72
  73 class InferenceSet {
  74         private:
  75
  76         /** The set of already discovered nodes in the tree */
  77         InferenceList *discoveredSet;
  78
  79         /** The list of feasible inferences */
  80         InferenceList *results;
  81
  82         /** The set of candidates */
  83         InferenceList *candidates;
  84
  85         /** The staticstics of inference process */
  86         inference_stat_t stat;
  87
  88         public:
  89         InferenceSet();
  90
  91         /** Print the result of inferences  */
  92         void printResults();
  93
  94         /** Print candidates of inferences */
  95         void printCandidates();
  96
  97         /** When we finish model checking or cannot further strenghen with the
  98          * inference, we commit the inference to be explored; if it is feasible, we
  99          * put it in the result list */
 100         void commitInference(Inference *infer, bool feasible);
 101
 102         int getCandidatesSize();
 103
 104         int getResultsSize();
 105
 106         /** Be careful that if the candidate is not added, it will be deleted in this
 107          *  function. Therefore, caller of this function should just delete the list when
 108          *  finishing calling this function. */
 109         bool addCandidates(Inference *curInfer, InferenceList *inferList);
 110
 111
 112         /** Check if we have stronger or equal inferences in the current result
 113          * list; if we do, we remove them and add the passed-in parameter infer */
 114          void addResult(Inference *infer);
 115
 116         /** Get the next available unexplored node; @Return NULL
 117          * if we don't have next, meaning that we are done with exploring */
 118         Inference* getNextInference();
 119
 120         /** Add the current inference to the set before adding fixes to it; in
 121          * this case, fixes will be added afterwards, and infer should've been
 122          * discovered */
 123         void addCurInference(Inference *infer);
 124
 125         /** Add one weaker node (the stronger one has been explored and known to be SC,
 126          *  we just want to know if a weaker one might also be SC).
 127          *  @Return true if the node to add has not been explored yet
 128          */
 129         void addWeakerInference(Inference *curInfer);
 130
 131         /** Add one possible node that represents a fix for the current inference;
 132          * @Return true if the node to add has not been explored yet
 133          */
 134         bool addInference(Inference *infer);
 135
 136         /** Return false if we haven't discovered that inference yet. Basically we
 137          * search the candidates list */
 138         bool hasBeenDiscovered(Inference *infer);
 139
 140         /** Return true if we have explored this inference yet. Basically we
 141          * search the candidates list */
 142         bool hasBeenExplored(Inference *infer);
 143
 144         MEMALLOC
 145 };
 146
 147 #endif