scfence/inferset.cc

   1 #include "patch.h"
   2 #include "inference.h"
   3 #include "inferset.h"
   4
   5 InferenceSet::InferenceSet() {
   6         discoveredSet = new InferenceList;
   7         results = new InferenceList;
   8         candidates = new InferenceList;
   9 }
  10
  11 /** Print the result of inferences  */
  12 void InferenceSet::printResults() {
  13         results->print("Result");
  14         stat.print();
  15 }
  16
  17 /** Print candidates of inferences */
  18 void InferenceSet::printCandidates() {
  19         candidates->print("Candidate");
  20 }
  21
  22 /** When we finish model checking or cannot further strenghen with the
  23  * inference, we commit the inference to be explored; if it is feasible, we
  24  * put it in the result list */
  25 void InferenceSet::commitInference(Inference *infer, bool feasible) {
  26         ASSERT (infer);
  27
  28         infer->setExplored(true);
  29         FENCE_PRINT("Explored %lu\n", infer->getHash());
  30         if (feasible) {
  31                 addResult(infer);
  32         }
  33 }
  34
  35 int InferenceSet::getCandidatesSize() {
  36         return candidates->getSize();
  37 }
  38
  39 int InferenceSet::getResultsSize() {
  40         return results->getSize();
  41 }
  42
  43 /** Be careful that if the candidate is not added, it will be deleted in this
  44  *  function. Therefore, caller of this function should just delete the list when
  45  *  finishing calling this function. */
  46 bool InferenceSet::addCandidates(Inference *curInfer, InferenceList *inferList) {
  47         if (!inferList)
  48                 return false;
  49         // First prune the list of inference
  50         inferList->pruneCandidates(curInfer);
  51
  52         ModelList<Inference*> *cands = inferList->getList();
  53
  54         // For the purpose of debugging, record all those inferences added here
  55         InferenceList *addedCandidates = new InferenceList;
  56         FENCE_PRINT("List size: %ld.\n", cands->size());
  57         bool added = false;
  58
  59         /******** addCurInference ********/
  60         // Add the current inference to the set, but specifially it marks it as
  61         // non-leaf node so that when it gets popped, we just need to commit it as
  62         // explored
  63         addCurInference(curInfer);
  64
  65         ModelList<Inference*>::iterator it;
  66         for (it = cands->begin(); it != cands->end(); it++) {
  67                 Inference *candidate = *it;
  68                 // Before adding those fixes, set its initial inference
  69                 candidate->setInitialInfer(curInfer->getInitialInfer());
  70                 bool tmpAdded = false;
  71                 /******** addInference ********/
  72                 tmpAdded = addInference(candidate);
  73                 if (tmpAdded) {
  74                         added = true;
  75                         it = cands->erase(it);
  76                         it--;
  77                         addedCandidates->push_back(candidate);
  78                 }
  79         }
  80
  81         // For debugging, print the list of candidates for this iteration
  82         FENCE_PRINT("Current inference:\n");
  83         curInfer->print();
  84         FENCE_PRINT("\n");
  85         FENCE_PRINT("The added inferences:\n");
  86         addedCandidates->print("Candidates");
  87         FENCE_PRINT("\n");
  88
  89         // Clean up the candidates
  90         inferList->clearList();
  91         FENCE_PRINT("potential results size: %d.\n", candidates->getSize());
  92         return added;
  93 }
  94
  95
  96 /** Check if we have stronger or equal inferences in the current result
  97  * list; if we do, we remove them and add the passed-in parameter infer */
  98  void InferenceSet::addResult(Inference *infer) {
  99         ModelList<Inference*> *list = results->getList();
 100         for (ModelList<Inference*>::iterator it = list->begin(); it !=
 101                 list->end(); it++) {
 102                 Inference *existResult = *it;
 103                 int compVal = existResult->compareTo(infer);
 104                 if (compVal == 0 || compVal == 1) {
 105                         // The existing result is equal or stronger, remove it
 106                         FENCE_PRINT("We are dumping the follwing inference because it's either too weak or the same:\n");
 107                         existResult->print();
 108                         FENCE_PRINT("\n");
 109                         it = list->erase(it);
 110                         it--;
 111                 }
 112         }
 113         list->push_back(infer);
 114  }
 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* InferenceSet::getNextInference() {
 119         Inference *infer = NULL;
 120         while (candidates->getSize() > 0) {
 121                 infer = candidates->back();
 122                 candidates->pop_back();
 123                 if (!infer->isLeaf()) {
 124                         commitInference(infer, false);
 125                         continue;
 126                 }
 127                 if (infer->getShouldFix() && hasBeenExplored(infer)) {
 128                         // Finish exploring this node
 129                         // Remove the node from the set
 130                         FENCE_PRINT("Explored inference:\n");
 131                         infer->print();
 132                         FENCE_PRINT("\n");
 133                         continue;
 134                 } else {
 135                         return infer;
 136                 }
 137         }
 138         return NULL;
 139 }
 140
 141 /** Add the current inference to the set before adding fixes to it; in
 142  * this case, fixes will be added afterwards, and infer should've been
 143  * discovered */
 144 void InferenceSet::addCurInference(Inference *infer) {
 145         infer->setLeaf(false);
 146         candidates->push_back(infer);
 147 }
 148
 149 /** Add one weaker node (the stronger one has been explored and known to be SC,
 150  *  we just want to know if a weaker one might also be SC).
 151  */
 152 void InferenceSet::addWeakerInference(Inference *curInfer) {
 153         Inference *initialInfer = curInfer->getInitialInfer();
 154         model_print("Before adding weaker inferece, candidates size=%d\n",
 155                 candidates->getSize());
 156         ModelList<Inference*> *list = discoveredSet->getList();
 157
 158         // An array of strengthened wildcards
 159         SnapVector<int> *strengthened = new SnapVector<int>;
 160         model_print("Strengthened wildcards\n");
 161         for (int i = 1; i <= curInfer->getSize(); i++) {
 162                 memory_order mo1 = (*curInfer)[i],
 163                         mo2 = (*initialInfer)[i];
 164                 int compVal = Inference::compareMemoryOrder(mo1, mo2);
 165                 if (!(compVal == 0 || compVal == 1)) {
 166                         model_print("assert failure\n");
 167                         model_print("compVal=%d\n", compVal);
 168                         ASSERT (false);
 169                 }
 170                 if (compVal == 0) // Same
 171                         continue;
 172                 model_print("wildcard %d -> %s (%s)\n", i, get_mo_str(mo1),
 173                         get_mo_str(mo2));
 174                 strengthened->push_back(i);
 175         }
 176
 177         for (unsigned i = 0; i < strengthened->size(); i++) {
 178                 int w = (*strengthened)[i]; // The wildcard
 179                 memory_order mo1 = (*curInfer)[w];
 180                 memory_order mo2 = (*initialInfer)[w];
 181                 memory_order weakerMO = Inference::nextWeakOrder(mo1, mo2);
 182                 Inference *weakerInfer1 = new Inference(curInfer);
 183                 Inference *weakerInfer2 = NULL;
 184                 if (mo1 == memory_order_acq_rel) {
 185                         if (mo2 == memory_order_acquire) {
 186                                 (*weakerInfer1)[w] = memory_order_acquire;
 187                         } else if (mo2 == memory_order_release) {
 188                                 (*weakerInfer1)[w] = memory_order_release;
 189                         } else { // relaxed
 190                                 (*weakerInfer1)[w] = memory_order_acquire;
 191                                 weakerInfer2 = new Inference(curInfer);
 192                                 (*weakerInfer2)[w] = memory_order_release;
 193                         }
 194                 } else {
 195                         if (mo2 != weakerMO)
 196                                 (*weakerInfer1)[w] = weakerMO;
 197                 }
 198
 199                 weakerInfer1->setShouldFix(false);
 200                 weakerInfer1->setLeaf(true);
 201                 if (weakerInfer2) {
 202                         weakerInfer2->setShouldFix(false);
 203                         weakerInfer2->setLeaf(true);
 204                 }
 205
 206                 bool foundIt = false;
 207                 for (ModelList<Inference*>::iterator it = list->begin(); it !=
 208                         list->end(); it++) {
 209                         Inference *discoveredInfer = *it;
 210                         // When we already have an equal inferences in the candidates list
 211                         int compVal = discoveredInfer->compareTo(weakerInfer1);
 212                         if (compVal == 0 && !discoveredInfer->isLeaf()) {
 213                                 foundIt = true;
 214                                 break;
 215                         }
 216                 }
 217                 if (!foundIt) {
 218                         addInference(weakerInfer1);
 219                 }
 220                 if (!weakerInfer2)
 221                         continue;
 222                 foundIt = false;
 223                 for (ModelList<Inference*>::iterator it = list->begin(); it !=
 224                         list->end(); it++) {
 225                         Inference *discoveredInfer = *it;
 226                         // When we already have an equal inferences in the candidates list
 227                         int compVal = discoveredInfer->compareTo(weakerInfer2);
 228                         if (compVal == 0 && !discoveredInfer->isLeaf()) {
 229                                 foundIt = true;
 230                                 break;
 231                         }
 232                 }
 233                 if (!foundIt) {
 234                         addInference(weakerInfer2);
 235                 }
 236         }
 237
 238         model_print("After adding weaker inferece, candidates size=%d\n",
 239                 candidates->getSize());
 240 }
 241
 242 /** Add one possible node that represents a fix for the current inference;
 243  * @Return true if the node to add has not been explored yet
 244  */
 245 bool InferenceSet::addInference(Inference *infer) {
 246         if (!hasBeenDiscovered(infer)) {
 247                 // We haven't discovered this inference yet
 248
 249                 // Newly added nodes are leaf by default
 250                 infer->setLeaf(true);
 251                 candidates->push_back(infer);
 252                 discoveredSet->push_back(infer);
 253                 FENCE_PRINT("Discovered a parameter assignment with hashcode %lu\n", infer->getHash());
 254                 return true;
 255         } else {
 256                 stat.notAddedAtFirstPlace++;
 257                 return false;
 258         }
 259 }
 260
 261 /** Return false if we haven't discovered that inference yet. Basically we
 262  * search the candidates list */
 263 bool InferenceSet::hasBeenDiscovered(Inference *infer) {
 264         ModelList<Inference*> *list = discoveredSet->getList();
 265         for (ModelList<Inference*>::iterator it = list->begin(); it !=
 266                 list->end(); it++) {
 267                 Inference *discoveredInfer = *it;
 268                 // When we already have an equal inferences in the candidates list
 269                 int compVal = discoveredInfer->compareTo(infer);
 270                 if (compVal == 0) {
 271                         FENCE_PRINT("%lu has beend discovered.\n",
 272                                 infer->getHash());
 273                         return true;
 274                 }
 275                 // Or the discoveredInfer is explored and infer is strong than it is
 276                 if (compVal == -1 && discoveredInfer->isLeaf() &&
 277                         discoveredInfer->isExplored()) {
 278                         return true;
 279                 }
 280         }
 281         return false;
 282 }
 283
 284 /** Return true if we have explored this inference yet. Basically we
 285  * search the candidates list */
 286 bool InferenceSet::hasBeenExplored(Inference *infer) {
 287         ModelList<Inference*> *list = discoveredSet->getList();
 288         for (ModelList<Inference*>::iterator it = list->begin(); it !=
 289                 list->end(); it++) {
 290                 Inference *discoveredInfer = *it;
 291                 if (!discoveredInfer->isExplored())
 292                         continue;
 293                 // When we already have an equal inferences in the candidates list
 294                 int compVal = discoveredInfer->compareTo(infer);
 295                 if (compVal == 0 || compVal == -1) {
 296                         return true;
 297                 }
 298         }
 299         return false;
 300 }