X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=scfence%2Finferset.cc;fp=scfence%2Finferset.cc;h=7eeb003a42fbfce38cb31bd213b314aca8c63953;hp=0000000000000000000000000000000000000000;hb=a65e234b607444355eb6e34097ee55ba93d4c01b;hpb=7c510878f9679da10de79c289df402356b092396 diff --git a/scfence/inferset.cc b/scfence/inferset.cc new file mode 100644 index 0000000..7eeb003 --- /dev/null +++ b/scfence/inferset.cc @@ -0,0 +1,300 @@ +#include "patch.h" +#include "inference.h" +#include "inferset.h" + +InferenceSet::InferenceSet() { + discoveredSet = new InferenceList; + results = new InferenceList; + candidates = new InferenceList; +} + +/** Print the result of inferences */ +void InferenceSet::printResults() { + results->print("Result"); + stat.print(); +} + +/** Print candidates of inferences */ +void InferenceSet::printCandidates() { + candidates->print("Candidate"); +} + +/** When we finish model checking or cannot further strenghen with the + * inference, we commit the inference to be explored; if it is feasible, we + * put it in the result list */ +void InferenceSet::commitInference(Inference *infer, bool feasible) { + ASSERT (infer); + + infer->setExplored(true); + FENCE_PRINT("Explored %lu\n", infer->getHash()); + if (feasible) { + addResult(infer); + } +} + +int InferenceSet::getCandidatesSize() { + return candidates->getSize(); +} + +int InferenceSet::getResultsSize() { + return results->getSize(); +} + +/** Be careful that if the candidate is not added, it will be deleted in this + * function. Therefore, caller of this function should just delete the list when + * finishing calling this function. */ +bool InferenceSet::addCandidates(Inference *curInfer, InferenceList *inferList) { + if (!inferList) + return false; + // First prune the list of inference + inferList->pruneCandidates(curInfer); + + ModelList *cands = inferList->getList(); + + // For the purpose of debugging, record all those inferences added here + InferenceList *addedCandidates = new InferenceList; + FENCE_PRINT("List size: %ld.\n", cands->size()); + bool added = false; + + /******** addCurInference ********/ + // Add the current inference to the set, but specifially it marks it as + // non-leaf node so that when it gets popped, we just need to commit it as + // explored + addCurInference(curInfer); + + ModelList::iterator it; + for (it = cands->begin(); it != cands->end(); it++) { + Inference *candidate = *it; + // Before adding those fixes, set its initial inference + candidate->setInitialInfer(curInfer->getInitialInfer()); + bool tmpAdded = false; + /******** addInference ********/ + tmpAdded = addInference(candidate); + if (tmpAdded) { + added = true; + it = cands->erase(it); + it--; + addedCandidates->push_back(candidate); + } + } + + // For debugging, print the list of candidates for this iteration + FENCE_PRINT("Current inference:\n"); + curInfer->print(); + FENCE_PRINT("\n"); + FENCE_PRINT("The added inferences:\n"); + addedCandidates->print("Candidates"); + FENCE_PRINT("\n"); + + // Clean up the candidates + inferList->clearList(); + FENCE_PRINT("potential results size: %d.\n", candidates->getSize()); + return added; +} + + +/** Check if we have stronger or equal inferences in the current result + * list; if we do, we remove them and add the passed-in parameter infer */ + void InferenceSet::addResult(Inference *infer) { + ModelList *list = results->getList(); + for (ModelList::iterator it = list->begin(); it != + list->end(); it++) { + Inference *existResult = *it; + int compVal = existResult->compareTo(infer); + if (compVal == 0 || compVal == 1) { + // The existing result is equal or stronger, remove it + FENCE_PRINT("We are dumping the follwing inference because it's either too weak or the same:\n"); + existResult->print(); + FENCE_PRINT("\n"); + it = list->erase(it); + it--; + } + } + list->push_back(infer); + } + +/** Get the next available unexplored node; @Return NULL + * if we don't have next, meaning that we are done with exploring */ +Inference* InferenceSet::getNextInference() { + Inference *infer = NULL; + while (candidates->getSize() > 0) { + infer = candidates->back(); + candidates->pop_back(); + if (!infer->isLeaf()) { + commitInference(infer, false); + continue; + } + if (infer->getShouldFix() && hasBeenExplored(infer)) { + // Finish exploring this node + // Remove the node from the set + FENCE_PRINT("Explored inference:\n"); + infer->print(); + FENCE_PRINT("\n"); + continue; + } else { + return infer; + } + } + return NULL; +} + +/** Add the current inference to the set before adding fixes to it; in + * this case, fixes will be added afterwards, and infer should've been + * discovered */ +void InferenceSet::addCurInference(Inference *infer) { + infer->setLeaf(false); + candidates->push_back(infer); +} + +/** Add one weaker node (the stronger one has been explored and known to be SC, + * we just want to know if a weaker one might also be SC). + */ +void InferenceSet::addWeakerInference(Inference *curInfer) { + Inference *initialInfer = curInfer->getInitialInfer(); + model_print("Before adding weaker inferece, candidates size=%d\n", + candidates->getSize()); + ModelList *list = discoveredSet->getList(); + + // An array of strengthened wildcards + SnapVector *strengthened = new SnapVector; + model_print("Strengthened wildcards\n"); + for (int i = 1; i <= curInfer->getSize(); i++) { + memory_order mo1 = (*curInfer)[i], + mo2 = (*initialInfer)[i]; + int compVal = Inference::compareMemoryOrder(mo1, mo2); + if (!(compVal == 0 || compVal == 1)) { + model_print("assert failure\n"); + model_print("compVal=%d\n", compVal); + ASSERT (false); + } + if (compVal == 0) // Same + continue; + model_print("wildcard %d -> %s (%s)\n", i, get_mo_str(mo1), + get_mo_str(mo2)); + strengthened->push_back(i); + } + + for (unsigned i = 0; i < strengthened->size(); i++) { + int w = (*strengthened)[i]; // The wildcard + memory_order mo1 = (*curInfer)[w]; + memory_order mo2 = (*initialInfer)[w]; + memory_order weakerMO = Inference::nextWeakOrder(mo1, mo2); + Inference *weakerInfer1 = new Inference(curInfer); + Inference *weakerInfer2 = NULL; + if (mo1 == memory_order_acq_rel) { + if (mo2 == memory_order_acquire) { + (*weakerInfer1)[w] = memory_order_acquire; + } else if (mo2 == memory_order_release) { + (*weakerInfer1)[w] = memory_order_release; + } else { // relaxed + (*weakerInfer1)[w] = memory_order_acquire; + weakerInfer2 = new Inference(curInfer); + (*weakerInfer2)[w] = memory_order_release; + } + } else { + if (mo2 != weakerMO) + (*weakerInfer1)[w] = weakerMO; + } + + weakerInfer1->setShouldFix(false); + weakerInfer1->setLeaf(true); + if (weakerInfer2) { + weakerInfer2->setShouldFix(false); + weakerInfer2->setLeaf(true); + } + + bool foundIt = false; + for (ModelList::iterator it = list->begin(); it != + list->end(); it++) { + Inference *discoveredInfer = *it; + // When we already have an equal inferences in the candidates list + int compVal = discoveredInfer->compareTo(weakerInfer1); + if (compVal == 0 && !discoveredInfer->isLeaf()) { + foundIt = true; + break; + } + } + if (!foundIt) { + addInference(weakerInfer1); + } + if (!weakerInfer2) + continue; + foundIt = false; + for (ModelList::iterator it = list->begin(); it != + list->end(); it++) { + Inference *discoveredInfer = *it; + // When we already have an equal inferences in the candidates list + int compVal = discoveredInfer->compareTo(weakerInfer2); + if (compVal == 0 && !discoveredInfer->isLeaf()) { + foundIt = true; + break; + } + } + if (!foundIt) { + addInference(weakerInfer2); + } + } + + model_print("After adding weaker inferece, candidates size=%d\n", + candidates->getSize()); +} + +/** Add one possible node that represents a fix for the current inference; + * @Return true if the node to add has not been explored yet + */ +bool InferenceSet::addInference(Inference *infer) { + if (!hasBeenDiscovered(infer)) { + // We haven't discovered this inference yet + + // Newly added nodes are leaf by default + infer->setLeaf(true); + candidates->push_back(infer); + discoveredSet->push_back(infer); + FENCE_PRINT("Discovered a parameter assignment with hashcode %lu\n", infer->getHash()); + return true; + } else { + stat.notAddedAtFirstPlace++; + return false; + } +} + +/** Return false if we haven't discovered that inference yet. Basically we + * search the candidates list */ +bool InferenceSet::hasBeenDiscovered(Inference *infer) { + ModelList *list = discoveredSet->getList(); + for (ModelList::iterator it = list->begin(); it != + list->end(); it++) { + Inference *discoveredInfer = *it; + // When we already have an equal inferences in the candidates list + int compVal = discoveredInfer->compareTo(infer); + if (compVal == 0) { + FENCE_PRINT("%lu has beend discovered.\n", + infer->getHash()); + return true; + } + // Or the discoveredInfer is explored and infer is strong than it is + if (compVal == -1 && discoveredInfer->isLeaf() && + discoveredInfer->isExplored()) { + return true; + } + } + return false; +} + +/** Return true if we have explored this inference yet. Basically we + * search the candidates list */ +bool InferenceSet::hasBeenExplored(Inference *infer) { + ModelList *list = discoveredSet->getList(); + for (ModelList::iterator it = list->begin(); it != + list->end(); it++) { + Inference *discoveredInfer = *it; + if (!discoveredInfer->isExplored()) + continue; + // When we already have an equal inferences in the candidates list + int compVal = discoveredInfer->compareTo(infer); + if (compVal == 0 || compVal == -1) { + return true; + } + } + return false; +}