5 InferenceSet::InferenceSet() {
6 discoveredSet = new InferenceList;
7 results = new InferenceList;
8 candidates = new InferenceList;
11 /** Print the result of inferences */
12 void InferenceSet::printResults() {
13 results->print("Result");
17 /** Print candidates of inferences */
18 void InferenceSet::printCandidates() {
19 candidates->print("Candidate");
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) {
28 infer->setExplored(true);
29 FENCE_PRINT("Explored %lu\n", infer->getHash());
35 int InferenceSet::getCandidatesSize() {
36 return candidates->getSize();
39 int InferenceSet::getResultsSize() {
40 return results->getSize();
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) {
49 // First prune the list of inference
50 inferList->pruneCandidates(curInfer);
52 ModelList<Inference*> *cands = inferList->getList();
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());
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
63 addCurInference(curInfer);
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);
75 it = cands->erase(it);
77 addedCandidates->push_back(candidate);
81 // For debugging, print the list of candidates for this iteration
82 FENCE_PRINT("Current inference:\n");
85 FENCE_PRINT("The added inferences:\n");
86 addedCandidates->print("Candidates");
89 // Clean up the candidates
90 inferList->clearList();
91 FENCE_PRINT("potential results size: %d.\n", candidates->getSize());
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 !=
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();
109 it = list->erase(it);
113 list->push_back(infer);
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);
127 if (infer->getShouldFix() && hasBeenExplored(infer)) {
128 // Finish exploring this node
129 // Remove the node from the set
130 FENCE_PRINT("Explored inference:\n");
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
144 void InferenceSet::addCurInference(Inference *infer) {
145 infer->setLeaf(false);
146 candidates->push_back(infer);
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).
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();
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);
170 if (compVal == 0) // Same
172 model_print("wildcard %d -> %s (%s)\n", i, get_mo_str(mo1),
174 strengthened->push_back(i);
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;
190 (*weakerInfer1)[w] = memory_order_acquire;
191 weakerInfer2 = new Inference(curInfer);
192 (*weakerInfer2)[w] = memory_order_release;
196 (*weakerInfer1)[w] = weakerMO;
199 weakerInfer1->setShouldFix(false);
200 weakerInfer1->setLeaf(true);
202 weakerInfer2->setShouldFix(false);
203 weakerInfer2->setLeaf(true);
206 bool foundIt = false;
207 for (ModelList<Inference*>::iterator it = list->begin(); 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()) {
218 addInference(weakerInfer1);
223 for (ModelList<Inference*>::iterator it = list->begin(); 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()) {
234 addInference(weakerInfer2);
238 model_print("After adding weaker inferece, candidates size=%d\n",
239 candidates->getSize());
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
245 bool InferenceSet::addInference(Inference *infer) {
246 if (!hasBeenDiscovered(infer)) {
247 // We haven't discovered this inference yet
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());
256 stat.notAddedAtFirstPlace++;
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 !=
267 Inference *discoveredInfer = *it;
268 // When we already have an equal inferences in the candidates list
269 int compVal = discoveredInfer->compareTo(infer);
271 FENCE_PRINT("%lu has beend discovered.\n",
275 // Or the discoveredInfer is explored and infer is strong than it is
276 if (compVal == -1 && discoveredInfer->isLeaf() &&
277 discoveredInfer->isExplored()) {
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 !=
290 Inference *discoveredInfer = *it;
291 if (!discoveredInfer->isExplored())
293 // When we already have an equal inferences in the candidates list
294 int compVal = discoveredInfer->compareTo(infer);
295 if (compVal == 0 || compVal == -1) {