3 #include "threads-model.h"
4 #include "clockvector.h"
6 #include "cyclegraph.h"
11 #include "inference.h"
13 #include "sc_annotation.h"
18 scfence_priv *SCFence::priv;
21 scgen(new SCGenerator),
22 stats((struct sc_statistics *)model_calloc(1, sizeof(struct sc_statistics))),
25 priv = new scfence_priv();
33 void SCFence::setExecution(ModelExecution * execution) {
34 this->execution=execution;
37 const char * SCFence::name() {
38 const char * name = "SCFENCE";
42 void SCFence::finish() {
43 model_print("SCFence finishes!\n");
47 /******************** SCFence-related Functions (Beginning) ********************/
49 void SCFence::inspectModelAction(ModelAction *act) {
50 if (act == NULL) // Get pass cases like data race detector
52 if (act->get_mo() >= memory_order_relaxed && act->get_mo() <=
53 memory_order_seq_cst) {
55 } else if (act->get_mo() == memory_order_normal) {
56 // For the purpose of eliminating data races
57 act->set_mo(memory_order_relaxed);
58 } else { // For wildcards
59 Inference *curInfer = getCurInference();
60 int wildcardID = get_wildcard_id(act->get_mo());
61 memory_order order = (*curInfer)[wildcardID];
62 if (order == WILDCARD_NONEXIST) {
63 (*curInfer)[wildcardID] = memory_order_relaxed;
64 act->set_mo(memory_order_relaxed);
66 act->set_mo((*curInfer)[wildcardID]);
72 void SCFence::actionAtInstallation() {
73 // When this pluggin gets installed, it become the inspect_plugin
74 model->set_inspect_plugin(this);
77 void SCFence::analyze(action_list_t *actions) {
78 scgen->setActions(actions);
79 scgen->setExecution(execution);
80 dup_threadlists = scgen->getDupThreadLists();
81 if (getTimeout() > 0 && isTimeout()) {
82 model_print("Backtrack because we reached the timeout bound.\n");
83 routineBacktrack(false);
87 /* Build up the thread lists for general purpose */
88 mo_graph = execution->get_mo_graph();
90 // First of all check if there's any uninitialzed read bugs
91 if (execution->have_bug_reports()) {
95 action_list_t *list = scgen->getSCList();
96 bool cyclic = scgen->getCyclic();
98 struct sc_statistics *s = scgen->getStats();
99 stats->nonsccount += s->nonsccount;
100 stats->sccount += s->sccount;
101 stats->elapsedtime += s->elapsedtime;
102 stats->actions += s->actions;
104 if (!cyclic && execution->have_bug_reports()) {
105 model_print("Be careful. This execution has bugs and still SC\n");
108 if (!cyclic && scgen->getPrintAlways()) {
109 scgen->print_list(list);
112 // Now we find a non-SC execution
114 /******** The Non-SC case (beginning) ********/
115 // Only print those that should be fixed
116 if (getCurInference()->getShouldFix())
117 scgen->print_list(list);
118 bool added = addFixes(list, NON_SC);
120 routineAfterAddFixes();
122 } else { // Couldn't imply anymore, backtrack
123 routineBacktrack(false);
126 /******** The Non-SC case (end) ********/
128 /******** The implicit MO case (beginning) ********/
129 if (getInferImplicitMO() && execution->too_many_steps() &&
130 !execution->is_complete_execution()) {
131 // Only print those that should be fixed
132 if (getCurInference()->getShouldFix())
133 scgen->print_list(list);
134 bool added = addFixes(list, IMPLICIT_MO);
136 FENCE_PRINT("Found an implicit mo pattern to fix!\n");
137 routineAfterAddFixes();
140 // This can be a good execution, so we can't do anything,
144 /******** The implicit MO case (end) ********/
146 /******** The checking data races case (beginning) ********/
147 bool added = addFixes(list, DATA_RACE);
149 FENCE_PRINT("Found an data race pattern to fix!\n");
150 routineAfterAddFixes();
156 void SCFence::exitModelChecker() {
157 model->exit_model_checker();
160 void SCFence::restartModelChecker() {
162 if (!getHasRestarted())
163 setHasRestarted(true);
166 bool SCFence::modelCheckerAtExitState() {
167 return model->get_exit_flag();
170 void SCFence::actionAtModelCheckingFinish() {
171 // Just bail if the model checker is at the exit state
172 if (modelCheckerAtExitState())
175 /** Backtrack with a successful inference */
176 routineBacktrack(true);
179 void SCFence::initializeByFile() {
180 char *name = getCandidateFile();
181 FILE *fp = fopen(name, "r");
183 fprintf(stderr, "Cannot open the input parameter assignment file: %s!\n", name);
187 Inference *infer = NULL;
189 memory_order mo = memory_order_relaxed;
190 char *str = (char *) malloc(sizeof(char) * (30 + 1));
191 bool isProcessing = false;
196 ret = fscanf(fp, "%s", str);
198 if (strcmp(str, "Result") == 0 || isProcessing) { // In an inference
199 ret = fscanf(fp, "%s", str);
201 infer = new Inference();
202 isProcessing = false;
203 while (!feof(fp)) { // Processing a specific inference
204 // wildcard # -> memory_order
205 ret = fscanf(fp, "%s", str);
207 if (strcmp(str, "Result") == 0) {
211 ret = fscanf(fp, "%d", &curNum);
212 ret = fscanf(fp, "%s", str);
213 if (ret <= 0 && ret != -1) {
214 fprintf(stderr, "The input parameter assignment file has wrong format\n");
218 ret = fscanf(fp, "%s", str);
220 if (strcmp(str, "memory_order_relaxed") == 0)
221 mo = memory_order_relaxed;
222 else if (strcmp(str, "memory_order_acquire") == 0)
223 mo = memory_order_acquire;
224 else if (strcmp(str, "memory_order_release") == 0)
225 mo = memory_order_release;
226 else if (strcmp(str, "memory_order_acq_rel") == 0)
227 mo = memory_order_acq_rel;
228 else if (strcmp(str, "memory_order_seq_cst") == 0)
229 mo = memory_order_seq_cst;
230 (*infer)[curNum] = mo;
233 /******** addInference ********/
234 if (!addInference(infer))
240 FENCE_PRINT("candidate size from file: %d\n", setSize());
241 Inference *next = getNextInference();
243 model_print("Wrong with the candidate file\n");
245 setCurInference(next);
249 char* SCFence::parseOptionHelper(char *opt, int *optIdx) {
250 char *res = (char*) model_malloc(1024 * sizeof(char));
252 while (opt[*optIdx] != '\0' && opt[*optIdx] != '|') {
253 res[resIdx++] = opt[(*optIdx)++];
259 bool SCFence::parseOption(char *opt) {
263 char option = opt[optIdx++];
264 val = parseOptionHelper(opt, &optIdx);
266 case 'f': // Read initial inference from file
267 setCandidateFile(val);
268 if (strcmp(val, "") == 0) {
269 model_print("Need to specify a file that contains initial inference!\n");
273 case 'b': // The bound above
274 setImplicitMOReadBound(atoi(val));
275 if (getImplicitMOReadBound() <= 0) {
276 model_print("Enter valid bound value!\n");
280 case 'm': // Infer the modification order from repetitive reads from
282 setInferImplicitMO(true);
283 if (strcmp(val, "") != 0) {
284 model_print("option m doesn't take any arguments!\n");
288 case 'a': // Turn on the annotation mode
289 scgen->setAnnotationMode(true);
290 if (strcmp(val, "") != 0) {
291 model_print("option a doesn't take any arguments!\n");
295 case 't': // The timeout set to force the analysis to backtrack
296 model_print("Parsing t option!\n");
297 model_print("t value: %s\n", val);
298 setTimeout(atoi(val));
301 model_print("Unknown SCFence option: %c!\n", option);
305 if (opt[optIdx] == '|') {
315 char* SCFence::getInputFileName(char *opt) {
323 res = (char*) model_malloc(1024 * sizeof(char));
325 while (opt[j] != '\0') {
333 int SCFence::getImplicitMOBound(char *opt) {
342 num = (char*) model_malloc(1024 * sizeof(char));
344 while (opt[j] != '\0') {
356 bool SCFence::option(char * opt) {
357 char *inputFileName = NULL;
358 unsigned implicitMOBoundNum = 0;
360 if (strcmp(opt, "verbose")==0) {
361 scgen->setPrintAlways(true);
363 } else if (strcmp(opt, "buggy")==0) {
365 } else if (strcmp(opt, "quiet")==0) {
366 scgen->setPrintBuggy(false);
368 } else if (strcmp(opt, "nonsc")==0) {
369 scgen->setPrintNonSC(true);
371 } else if (strcmp(opt, "time")==0) {
374 } else if (strcmp(opt, "no-weaken")==0) {
377 } else if (strcmp(opt, "anno")==0) {
378 scgen->setAnnotationMode(true);
380 } else if (strcmp(opt, "implicit-mo")==0) {
381 setInferImplicitMO(true);
383 } else if ((inputFileName = getInputFileName(opt)) != NULL) {
384 if (strcmp(inputFileName, "") == 0) {
385 model_print("Need to specify a file that contains initial inference!\n");
388 setCandidateFile(inputFileName);
391 } else if ((implicitMOBoundNum = getImplicitMOBound(opt)) > 0) {
392 setImplicitMOReadBound(implicitMOBoundNum);
395 model_print("file-InputFile -- takes candidate file as argument right after the symbol '-' \n");
396 model_print("no-weaken -- turn off the weakening mode (by default ON)\n");
397 model_print("anno -- turn on the annotation mode (by default OFF)\n");
398 model_print("implicit-mo -- imply implicit modification order, takes no arguments (by default OFF, default bound is %d\n", DEFAULT_REPETITIVE_READ_BOUND);
399 model_print("bound-NUM -- specify the bound for the implicit mo implication, takes a number as argument right after the symbol '-'\n");
405 /** Check whether a chosen reads-from path is a release sequence */
406 bool SCFence::isReleaseSequence(path_t *path) {
408 path_t::reverse_iterator rit = path->rbegin(),
410 const ModelAction *read,
413 for (; rit != path->rend(); rit++) {
417 write = read->get_reads_from();
418 if (rit_next != path->rend()) {
419 next_read = *rit_next;
420 if (write != next_read) {
428 /** Only return those applicable patches in a vector */
429 SnapVector<Patch*>* SCFence::getAcqRel(const ModelAction *read, const
430 ModelAction *readBound,const ModelAction *write, const ModelAction *writeBound) {
432 SnapVector<Patch*> *patches = new SnapVector<Patch*>;
433 /* Also support rel/acq fences synchronization here */
434 // Look for the acq fence after the read action
435 int readThrdID = read->get_tid(),
436 writeThrdID = write->get_tid();
437 action_list_t *readThrd = &(*dup_threadlists)[readThrdID],
438 *writeThrd = &(*dup_threadlists)[writeThrdID];
439 action_list_t::iterator readIter = std::find(readThrd->begin(),
440 readThrd->end(), read);
441 action_list_t::reverse_iterator writeIter = std::find(writeThrd->rbegin(),
442 writeThrd->rend(), write);
444 action_list_t *acqFences = new action_list_t,
445 *relFences = new action_list_t;
446 ModelAction *act = *readIter;
447 while (readIter++ != readThrd->end() && act != readBound) {
448 if (act->is_fence()) {
449 acqFences->push_back(act);
454 while (writeIter++ != writeThrd->rend() && act != writeBound) {
455 if (act->is_fence()) {
456 relFences->push_back(act);
460 // Now we have a list of rel/acq fences at hand
461 int acqFenceSize = acqFences->size(),
462 relFenceSize = relFences->size();
465 if (acqFenceSize == 0 && relFenceSize == 0) {
467 } else if (acqFenceSize > 0 && relFenceSize == 0) {
468 for (action_list_t::iterator it = acqFences->begin(); it !=
469 acqFences->end(); it++) {
470 ModelAction *fence = *it;
471 p = new Patch(fence, memory_order_acquire, write, memory_order_release);
472 if (p->isApplicable())
473 patches->push_back(p);
475 } else if (acqFenceSize == 0 && relFenceSize > 0) {
476 for (action_list_t::iterator it = relFences->begin(); it !=
477 relFences->end(); it++) {
478 ModelAction *fence = *it;
479 p = new Patch(fence, memory_order_release, read, memory_order_acquire);
480 if (p->isApplicable())
481 patches->push_back(p);
484 /* Impose on both relFences and acqFences */
485 bool twoFences = false;
486 for (action_list_t::iterator it1 = relFences->begin(); it1 !=
487 relFences->end(); it1++) {
488 ModelAction *relFence = *it1;
489 for (action_list_t::iterator it2 = acqFences->begin(); it2 !=
490 acqFences->end(); it2++) {
491 ModelAction *acqFence = *it2;
492 p = new Patch(relFence, memory_order_release, acqFence, memory_order_acquire);
493 if (p->isApplicable()) {
494 patches->push_back(p);
500 /* Only impose on the acqFences */
501 for (action_list_t::iterator it = acqFences->begin(); it !=
502 acqFences->end(); it++) {
503 ModelAction *fence = *it;
504 p = new Patch(fence, memory_order_acquire, write, memory_order_release);
505 if (p->isApplicable())
506 patches->push_back(p);
508 /* Only impose on the relFences */
509 for (action_list_t::iterator it = relFences->begin(); it !=
510 relFences->end(); it++) {
511 ModelAction *fence = *it;
512 p = new Patch(fence, memory_order_release, read, memory_order_acquire);
513 if (p->isApplicable())
514 patches->push_back(p);
519 // If we can find a fix with fences, we don't fix on the operation
520 if (patches->size() > 0)
522 p = new Patch(read, memory_order_acquire, write,
523 memory_order_release);
524 if (p->isApplicable())
525 patches->push_back(p);
529 /** Impose the synchronization between the begin and end action, and the paths
530 * are a list of paths that each represent the union of rfUsb. We then
531 * strengthen the current inference by necessity.
533 bool SCFence::imposeSync(InferenceList *inferList,
534 paths_t *paths, const ModelAction *begin, const ModelAction *end) {
538 for (paths_t::iterator i_paths = paths->begin(); i_paths != paths->end(); i_paths++) {
539 // Iterator over all the possible paths
540 path_t *path = *i_paths;
541 InferenceList *cands = new InferenceList;
542 // Impose synchronization by path
543 if (imposeSync(cands, path, begin, end))
545 inferList->append(cands);
550 /** Impose the synchronization between the begin and end action, and the path
551 * is the union of rfUsb. We then strengthen the current inference by
554 bool SCFence::imposeSync(InferenceList *inferList,
555 path_t *path, const ModelAction *begin, const ModelAction *end) {
557 bool release_seq = isReleaseSequence(path);
558 SnapVector<Patch*> *patches;
560 const ModelAction *relHead = path->front()->get_reads_from(),
561 *lastRead = path->back();
562 patches = getAcqRel(lastRead, end, relHead, begin);
563 if (patches->size() == 0)
565 inferList->applyPatch(getCurInference(), patches);
567 // Bail now for the release sequence because
571 for (path_t::iterator it = path->begin(); it != path->end(); it++) {
572 const ModelAction *read = *it,
573 *write = read->get_reads_from(),
574 *prevRead = NULL, *nextRead;
576 const ModelAction *readBound = NULL,
579 if (it == path->end()) {
584 readBound = prevRead->get_reads_from();
589 writeBound = nextRead;
594 /* Extend to support rel/acq fences synchronization here */
595 patches = getAcqRel(read, readBound, write, writeBound);
597 if (patches->size() == 0) {
598 // We cannot strengthen the inference
602 inferList->applyPatch(getCurInference(), patches);
608 /** Impose SC orderings to related actions (including fences) such that we
609 * either want to establish mo between act1 & act2 (act1 -mo-> act2) when they
610 * can't establish hb; or that act2 can't read from any actions that are
611 * modification ordered before act1. All these requirements are consistent with
612 * the following strengthening strategy:
613 * 1. make both act1 and act2 SC
614 * 2. if there are fences in between act1 & act2, and the fences are either in
615 * the threads of either act1 or act2, we can impose SC on the fences or
616 * corresponding actions.
618 bool SCFence::imposeSC(action_list_t * actions, InferenceList *inferList, const ModelAction *act1, const ModelAction *act2) {
622 action_list_t::iterator act1Iter = std::find(actions->begin(),
623 actions->end(), act1);
624 action_list_t::iterator act2Iter = std::find(act1Iter,
625 actions->end(), act2);
627 action_list_t::iterator it = act1Iter;
629 action_list_t *fences = new action_list_t;
631 while (it != act2Iter) {
632 ModelAction *fence = *it;
634 if (!fence->is_fence())
636 if (!is_wildcard(fence->get_original_mo()))
638 fences->push_back(fence);
643 SnapVector<Patch*> *patches = new SnapVector<Patch*>;
645 bool twoFences = false;
646 // Impose SC on two fences
647 for (action_list_t::iterator fit1 = fences->begin(); fit1 != fences->end();
649 ModelAction *fence1 = *fit1;
650 action_list_t::iterator fit2 = fit1;
652 for (; fit2 != fences->end(); fit2++) {
653 ModelAction *fence2 = *fit2;
654 p = new Patch(fence1, memory_order_seq_cst, fence2, memory_order_seq_cst);
655 if (p->isApplicable()) {
656 Inference *curInfer = getCurInference();
657 memory_order mo1 = (*curInfer)[get_wildcard_id(fence1->get_original_mo())];
658 memory_order mo2 = (*curInfer)[get_wildcard_id(fence2->get_original_mo())];
659 // We can avoid this by adding two fences
660 if (mo1 != memory_order_seq_cst || mo2 != memory_order_seq_cst)
662 patches->push_back(p);
667 // Just impose SC on one fence
669 for (action_list_t::iterator fit = fences->begin(); fit != fences->end();
671 ModelAction *fence = *fit;
672 model_print("one fence\n");
674 p = new Patch(act1, memory_order_seq_cst, fence, memory_order_seq_cst);
675 if (p->isApplicable()) {
676 // We can avoid this by adding two fences
677 patches->push_back(p);
679 p = new Patch(act2, memory_order_seq_cst, fence, memory_order_seq_cst);
680 if (p->isApplicable()) {
681 // We can avoid this by adding two fences
682 patches->push_back(p);
686 p = new Patch(act1, memory_order_seq_cst, act2, memory_order_seq_cst);
687 if (p->isApplicable()) {
688 patches->push_back(p);
692 if (patches->size() > 0) {
693 inferList->applyPatch(getCurInference(), patches);
699 /** A subroutine that calculates the potential fixes for the non-sc pattern (a),
700 * a.k.a old value reading. The whole idea is as follows.
701 * write -isc-> write2 && write2 -isc->read && write -rf-> read!!!
702 * The fix can be two-step:
703 * a. make write -mo-> write2, and we can accomplish this by imposing hb
704 * between write and write2, and if not possible, make write -sc-> write2
705 * b. make write2 -hb-> read, and if not possible, make write2 -sc-> read.
707 InferenceList* SCFence::getFixesFromPatternA(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter) {
708 ModelAction *read = *readIter,
711 InferenceList *candidates = new InferenceList;
712 paths_t *paths1, *paths2;
714 // Find all writes between the write1 and the read
715 action_list_t *write2s = new action_list_t();
717 action_list_t::iterator findIt = writeIter;
721 if (write2->is_write() && write2->get_location() ==
722 write->get_location()) {
723 write2s->push_back(write2);
726 } while (findIt != readIter);
728 // Found all the possible write2s
729 FENCE_PRINT("write2s set size: %ld\n", write2s->size());
730 for (action_list_t::iterator itWrite2 = write2s->begin();
731 itWrite2 != write2s->end(); itWrite2++) {
732 InferenceList *tmpCandidates = new InferenceList;
734 // Whether the write and the write2 originally have modification order
735 bool isWritesMO = false;
736 FENCE_PRINT("write2:\n");
738 // write1->write2 (write->write2)
739 // Whether write -mo-> write2
740 if (!mo_graph->checkReachable(write, write2)) {
741 paths1 = get_rf_sb_paths(write, write2);
742 if (paths1->size() > 0) {
743 FENCE_PRINT("From write1 to write2: \n");
744 print_rf_sb_paths(paths1, write, write2);
745 // FIXME: Need to make sure at least one path is feasible; what
746 // if we got empty candidates here, maybe should then impose SC,
747 // same in the write2->read
748 imposeSync(tmpCandidates, paths1, write, write2);
750 FENCE_PRINT("Have to impose sc on write1 & write2: \n");
753 imposeSC(list, tmpCandidates, write, write2);
756 if (!write->happens_before(write2)) {
759 FENCE_PRINT("write1 mo before write2. \n");
762 // write2->read (write2->read)
763 // now we only need to make write2 -hb-> read
764 if (!write2->happens_before(read)) {
765 paths2 = get_rf_sb_paths(write2, read);
766 if (paths2->size() > 0) {
767 FENCE_PRINT("From write2 to read: \n");
768 print_rf_sb_paths(paths2, write2, read);
769 imposeSync(tmpCandidates, paths2, write2, read);
771 FENCE_PRINT("Have to impose sc on write2 & read: \n");
774 imposeSC(list, tmpCandidates, write2, read);
776 // Also need to make sure write -sc/hb-> write2
777 FENCE_PRINT("Also have to impose hb/sc on write & write2: \n");
780 paths1 = get_rf_sb_paths(write, write2);
781 if (paths1->size() > 0) {
782 FENCE_PRINT("Impose hb, from write1 to write2: \n");
783 print_rf_sb_paths(paths1, write, write2);
784 imposeSync(tmpCandidates, paths1, write, write2);
786 FENCE_PRINT("Also have to impose sc on write1 & write2: \n");
789 imposeSC(list, tmpCandidates, write, write2);
794 FENCE_PRINT("write2 hb before read. \n");
796 candidates->append(tmpCandidates);
798 // Return the complete list of candidates
802 /** To fix this pattern, we have two options:
803 * 1. impose futureWrite -hb-> read so that the SC analysis will order
804 * in a way that the the write is ordered before the read;
805 * 2. impose read -hb->futureWrite so that the reads-from edge from futureWrite
806 * to the read is not allowed.
808 InferenceList* SCFence::getFixesFromPatternB(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter) {
809 InferenceList *res = new InferenceList,
810 *candidates = new InferenceList;
812 ModelAction *read = *readIter,
814 // Fixing one direction (read -> futureWrite)
815 paths_t *paths1 = get_rf_sb_paths(read, write);
816 if (paths1->size() > 0) {
817 FENCE_PRINT("From read to future write: \n");
818 print_rf_sb_paths(paths1, read, write);
819 imposeSync(res, paths1, read, write);
822 // Fixing the other direction (futureWrite -> read) for one edge case
823 paths_t *paths2 = get_rf_sb_paths(write, read);
824 FENCE_PRINT("From future write to read (edge case): \n");
825 print_rf_sb_paths(paths2, write, read);
826 imposeSync(candidates, paths2, write, read);
828 // Append the candidates to the res list
829 res->append(candidates);
833 bool SCFence::addFixesNonSC(action_list_t *list) {
835 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
836 InferenceList *candidates = NULL;
837 ModelAction *act = *it;
839 // Save the iterator of the read and the write
840 action_list_t::iterator readIter = it, writeIter;
841 if (act->get_seq_number() > 0) {
842 // Annotated reads will be ignored
843 if (scgen->getBadrfset()->contains(act) &&
844 !scgen->getAnnotatedReadSet()->contains(act)) {
845 const ModelAction *write = act->get_reads_from();
846 // Check reading old or future value
847 writeIter = std::find(list->begin(),
849 action_list_t::iterator findIt = std::find(list->begin(),
851 bool readOldVal = findIt != readIter ? true : false;
853 if (readOldVal) { // Pattern (a) read old value
854 FENCE_PRINT("Running through pattern (a)!\n");
855 candidates = getFixesFromPatternA(list, readIter, writeIter);
856 // Add candidates pattern (a)
858 added = addCandidates(candidates);
859 } else { // Pattern (b) read future value
860 // act->read, write->futureWrite
861 FENCE_PRINT("Running through pattern (b)!\n");
862 candidates = getFixesFromPatternB(list, readIter, writeIter);
863 // Add candidates pattern (b)
864 added = addCandidates(candidates);
866 // Just eliminate the first cycle we see in the execution
875 /** Return false to indicate there's no fixes for this execution. This can
876 * happen for specific reason such as it's a user-specified assertion failure */
877 bool SCFence::addFixesBuggyExecution(action_list_t *list) {
878 InferenceList *candidates = new InferenceList;
879 bool foundFix = false;
881 for (action_list_t::reverse_iterator rit = list->rbegin(); rit !=
882 list->rend(); rit++) {
883 ModelAction *uninitRead = *rit;
884 if (uninitRead->get_seq_number() > 0) {
885 if (!uninitRead->is_read() ||
886 !uninitRead->get_reads_from()->is_uninitialized())
888 for (action_list_t::iterator it = list->begin(); it !=
890 ModelAction *write = *it;
891 if (write->same_var(uninitRead)) {
892 // Now we can try to impose sync write hb-> uninitRead
893 paths_t *paths1 = get_rf_sb_paths(write, uninitRead);
894 if (paths1->size() > 0) {
895 FENCE_PRINT("Running through pattern (b') (unint read)!\n");
896 print_rf_sb_paths(paths1, write, uninitRead);
897 imposeSync(candidates, paths1, write, uninitRead);
898 added = addCandidates(candidates);
914 /** Return false to indicate there's no implied mo for this execution. The idea
915 * is that it counts the number of reads in the middle of write1 and write2, if
916 * that number exceeds a specific number, then the analysis thinks that the
917 * program is stuck in an infinite loop because write1 does not establish proper
918 * synchronization with write2 such that the reads can read from write1 for
920 bool SCFence::addFixesImplicitMO(action_list_t *list) {
922 InferenceList *candidates = new InferenceList;
923 for (action_list_t::reverse_iterator rit2 = list->rbegin(); rit2 !=
924 list->rend(); rit2++) {
925 ModelAction *write2 = *rit2;
926 if (!write2->is_write())
928 action_list_t::reverse_iterator rit1 = rit2;
930 for (; rit1 != list->rend(); rit1++) {
931 ModelAction *write1 = *rit1;
932 if (!write1->is_write() || write1->get_location() !=
933 write2->get_location())
936 action_list_t::reverse_iterator ritRead = rit2;
938 for (; ritRead != rit1; ritRead++) {
939 ModelAction *read = *ritRead;
940 if (!read->is_read() || read->get_location() !=
941 write1->get_location())
945 if (readCnt > getImplicitMOReadBound()) {
946 // Found it, make write1 --hb-> write2
947 bool isMO = execution->get_mo_graph()->checkReachable(write1, write2);
948 if (isMO) // Only impose mo when it doesn't have mo impsed
950 FENCE_PRINT("Running through pattern (c) -- implicit mo!\n");
951 FENCE_PRINT("Read count between the two writes: %d\n", readCnt);
952 FENCE_PRINT("implicitMOReadBound: %d\n",
953 getImplicitMOReadBound());
956 paths_t *paths1 = get_rf_sb_paths(write1, write2);
957 if (paths1->size() > 0) {
958 FENCE_PRINT("From write1 to write2: \n");
959 print_rf_sb_paths(paths1, write1, write2);
960 imposeSync(candidates, paths1, write1, write2);
961 // Add the candidates as potential results
962 added = addCandidates(candidates);
966 FENCE_PRINT("Cannot establish hb between write1 & write2: \n");
977 bool SCFence::checkDataRace(action_list_t *list, ModelAction **act1,
978 ModelAction **act2) {
980 SnapList<action_list_t*> *opList = new SnapList<action_list_t*>;
981 /** Collect the operations per location */
982 for (action_list_t::iterator iter = list->begin(); iter != list->end();
984 ModelAction *act = *iter;
985 if (act->get_original_mo() != memory_order_normal)
987 bool foundIt = false;
988 for (SnapList<action_list_t*>::iterator listIter = opList->begin();
989 listIter != opList->end(); listIter++) {
990 action_list_t *list = *listIter;
991 ModelAction *listAct = *(list->begin());
992 if (listAct->get_location() != act->get_location())
995 list->push_back(act);
998 action_list_t *newList = new action_list_t;
999 newList->push_back(act);
1000 opList->push_back(newList);
1004 if (opList->size() == 0)
1006 /** Now check if any two operations (same loc) establish hb */
1007 for (SnapList<action_list_t*>::iterator listIter = opList->begin();
1008 listIter != opList->end(); listIter++) {
1009 action_list_t *list = *listIter;
1010 action_list_t::iterator it1, it2;
1011 for (it1 = list->begin(); it1 != list->end(); it1++) {
1012 ModelAction *raceAct1 = *it1;
1015 for (; it2 != list->end(); it2++) {
1016 ModelAction *raceAct2 = *it2;
1017 if (!raceAct1->happens_before(raceAct2) &&
1018 !raceAct2->happens_before(raceAct1)) {
1029 ModelAction* SCFence::sbPrevAction(ModelAction *act) {
1030 int idx = id_to_int(act->get_tid());
1031 // Retrieves the thread list of the action
1032 action_list_t *list = &(*scgen->getDupThreadLists())[idx];
1033 action_list_t::iterator iter = std::find(list->begin(),
1038 ModelAction* SCFence::sbNextAction(ModelAction *act) {
1039 int idx = id_to_int(act->get_tid());
1040 // Retrieves the thread list of the action
1041 action_list_t *list = &(*scgen->getDupThreadLists())[idx];
1042 action_list_t::iterator iter = std::find(list->begin(),
1047 bool SCFence::addFixesDataRace(action_list_t *list) {
1048 ModelAction *act1, *act2;
1049 bool hasRace = checkDataRace(list, &act1, &act2);
1051 InferenceList *candidates1 = new InferenceList,
1052 *candidates2 = new InferenceList;
1053 paths_t *paths1, *paths2;
1054 model_print("Fixing data race: \n");
1055 paths1 = get_rf_sb_paths(sbNextAction(act1), sbPrevAction(act2));
1056 paths2 = get_rf_sb_paths(sbNextAction(act2), sbPrevAction(act1));
1058 if (paths1->size() > 0) {
1059 model_print("paths1: \n");
1060 print_rf_sb_paths(paths1, act1, act2);
1061 imposeSync(candidates1, paths1, act1, act2);
1062 bool added = addCandidates(candidates1);
1063 if (paths2->size() > 0) {
1064 model_print("paths2: \n");
1065 print_rf_sb_paths(paths2, act2, act1);
1066 imposeSync(candidates2, paths2, act2, act1);
1067 added |= addCandidates(candidates2);
1075 bool SCFence::addFixes(action_list_t *list, fix_type_t type) {
1076 // First check whether this is a later weakened inference
1077 if (!getCurInference()->getShouldFix())
1081 case BUGGY_EXECUTION:
1082 added = addFixesBuggyExecution(list);
1085 added = addFixesImplicitMO(list);
1088 added = addFixesNonSC(list);
1091 added = addFixesDataRace(list);
1096 if (added && isBuggy()) {
1097 // If this is a buggy inference and we have got fixes for it, set the
1105 bool SCFence::routineBacktrack(bool feasible) {
1106 model_print("Backtrack routine:\n");
1108 /******** commitCurInference ********/
1109 Inference *curInfer = getCurInference();
1110 commitInference(curInfer, feasible);
1113 model_print("Found one result!\n");
1114 } else if (!hasFixes()) { // Buggy and have no fixes
1115 model_print("Found one buggy candidate!\n");
1118 // Try to weaken this inference
1119 if (weaken && !isBuggy()) {
1120 getSet()->addWeakerInference(curInfer);
1124 if (curInfer->getShouldFix()) {
1125 model_print("Reach an infeasible inference!\n");
1127 model_print("Get an unweakenable inference!\n");
1128 curInfer->print(true);
1132 /******** getNextInference ********/
1133 Inference *next = getNextInference();
1136 /******** setCurInference ********/
1137 setCurInference(next);
1138 /******** restartModelChecker ********/
1139 restartModelChecker();
1142 // Finish exploring the whole process
1143 model_print("We are done with the whole process!\n");
1144 model_print("The results are as the following:\n");
1148 /******** exitModelChecker ********/
1155 void SCFence::routineAfterAddFixes() {
1156 model_print("Add fixes routine begin:\n");
1158 /******** getNextInference ********/
1159 Inference *next = getNextInference();
1163 /******** setCurInference ********/
1164 setCurInference(next);
1165 /******** restartModelChecker ********/
1166 restartModelChecker();
1168 model_print("Add fixes routine end:\n");
1169 model_print("Restart checking with the follwing inference:\n");
1170 getCurInference()->print();
1171 model_print("Checking...\n");
1173 routineBacktrack(false);
1179 /** This function finds all the paths that is a union of reads-from &
1180 * sequence-before relationship between act1 & act2. */
1181 paths_t * SCFence::get_rf_sb_paths(const ModelAction *act1, const ModelAction *act2) {
1182 int idx1 = id_to_int(act1->get_tid()),
1183 idx2 = id_to_int(act2->get_tid());
1184 // Retrieves the two lists of actions of thread1 & thread2
1185 action_list_t *list1 = &(*dup_threadlists)[idx1],
1186 *list2 = &(*dup_threadlists)[idx2];
1187 if (list1->size() == 0 || list2->size() == 0) {
1188 return new paths_t();
1191 // The container for all possible results
1192 paths_t *paths = new paths_t();
1193 // A stack that records all current possible paths
1194 paths_t *stack = new paths_t();
1196 // Initialize the stack with loads sb-ordered before act2
1197 for (action_list_t::iterator it2 = list2->begin(); it2 != list2->end(); it2++) {
1198 ModelAction *act = *it2;
1199 // Add read action not sb after the act2 (including act2)
1200 if (act->get_seq_number() > act2->get_seq_number())
1202 if (!act->is_read())
1204 // Each start with a possible path
1205 path = new path_t();
1206 path->push_front(act);
1207 stack->push_back(path);
1209 while (stack->size() > 0) {
1210 path = stack->back();
1212 // The latest read in the temporary path
1213 ModelAction *read = path->front();
1214 const ModelAction *write = read->get_reads_from();
1215 // If the read is uninitialized, don't do it
1216 if (write->get_seq_number() == 0) {
1220 /** In case of cyclic sbUrf, make sure the write appears in a new thread
1221 * or in an existing thread that is sequence-before the added read
1225 for (path_t::iterator p_it = path->begin(); p_it != path->end();
1227 ModelAction *addedRead = *p_it;
1228 if (id_to_int(write->get_tid()) == id_to_int(addedRead->get_tid())) {
1229 // In the same thread
1230 if (write->get_seq_number() >= addedRead->get_seq_number()) {
1238 // Not a useful rfUsb path (loop)
1243 unsigned write_seqnum = write->get_seq_number();
1244 // We then check if we got a valid path
1245 if (id_to_int(write->get_tid()) == idx1 &&
1246 write_seqnum >= act1->get_seq_number()) {
1248 paths->push_back(path);
1251 // Extend the path with the latest read
1252 int idx = id_to_int(write->get_tid());
1253 action_list_t *list = &(*dup_threadlists)[idx];
1254 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
1255 ModelAction *act = *it;
1256 if (act->get_seq_number() > write_seqnum) // Could be RMW
1258 if (!act->is_read())
1260 path_t *new_path = new path_t(*path);
1261 new_path->push_front(act);
1262 stack->push_back(new_path);
1269 void SCFence::print_rf_sb_paths(paths_t *paths, const ModelAction *start, const ModelAction *end) {
1270 FENCE_PRINT("Starting from:\n");
1273 for (paths_t::iterator paths_i = paths->begin(); paths_i !=
1274 paths->end(); paths_i++) {
1275 path_t *path = *paths_i;
1276 FENCE_PRINT("Path %ld, size (%ld):\n", distance(paths->begin(), paths_i),
1278 path_t::iterator it = path->begin(), i_next;
1279 for (; it != path->end(); it++) {
1282 const ModelAction *read = *it,
1283 *write = read->get_reads_from(),
1284 *next_read = (i_next != path->end()) ? *i_next : NULL;
1286 if (next_read == NULL || next_read->get_reads_from() != read) {
1287 // Not the same RMW, also print the read operation
1291 // Output a linebreak at the end of the path
1294 FENCE_PRINT("Ending with:\n");
1298 /******************** SCFence-related Functions (End) ********************/