scfence/scfence.cc

   1 #include "scfence.h"
   2 #include "action.h"
   3 #include "threads-model.h"
   4 #include "clockvector.h"
   5 #include "execution.h"
   6 #include "cyclegraph.h"
   7 #include <sys/time.h>
   8
   9 #include "model.h"
  10 #include "wildcard.h"
  11 #include "inference.h"
  12 #include "inferset.h"
  13 #include "sc_annotation.h"
  14 #include "errno.h"
  15 #include <stdio.h>
  16 #include <algorithm>
  17
  18 scfence_priv *SCFence::priv;
  19
  20 SCFence::SCFence() :
  21         scgen(new SCGenerator),
  22         stats((struct sc_statistics *)model_calloc(1, sizeof(struct sc_statistics))),
  23         execution(NULL)
  24 {
  25         priv = new scfence_priv();
  26         weaken = true;
  27 }
  28
  29 SCFence::~SCFence() {
  30         delete(stats);
  31 }
  32
  33 void SCFence::setExecution(ModelExecution * execution) {
  34         this->execution=execution;
  35 }
  36
  37 const char * SCFence::name() {
  38         const char * name = "AUTOMO";
  39         return name;
  40 }
  41
  42 void SCFence::finish() {
  43         model_print("SCFence finishes!\n");
  44 }
  45
  46
  47 /******************** SCFence-related Functions (Beginning) ********************/
  48
  49 void SCFence::inspectModelAction(ModelAction *act) {
  50         if (act == NULL) // Get pass cases like data race detector
  51                 return;
  52         if (act->get_mo() >= memory_order_relaxed && act->get_mo() <=
  53                 memory_order_seq_cst) {
  54                 return;
  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);
  65                 } else {
  66                         act->set_mo((*curInfer)[wildcardID]);
  67                 }
  68         }
  69 }
  70
  71
  72 void SCFence::actionAtInstallation() {
  73         // When this pluggin gets installed, it become the inspect_plugin
  74         model->set_inspect_plugin(this);
  75 }
  76
  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);
  84                 return;
  85         }
  86
  87         /* Build up the thread lists for general purpose */
  88         mo_graph = execution->get_mo_graph();
  89
  90         // First of all check if there's any uninitialzed read bugs
  91         if (execution->have_bug_reports()) {
  92                 setBuggy(true);
  93         }
  94
  95         action_list_t *list = scgen->getSCList();
  96         bool cyclic = scgen->getCyclic();
  97
  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;
 103
 104         if (!cyclic && execution->have_bug_reports()) {
 105                 model_print("Be careful. This execution has bugs and still SC\n");
 106         }
 107
 108         if (!cyclic && scgen->getPrintAlways()) {
 109                 scgen->print_list(list);
 110         }
 111
 112         // Now we find a non-SC execution
 113         if (cyclic) {
 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);
 119                 if (added) {
 120                         routineAfterAddFixes();
 121                         return;
 122                 } else { // Couldn't imply anymore, backtrack
 123                         routineBacktrack(false);
 124                         return;
 125                 }
 126                 /******** The Non-SC case (end) ********/
 127         } else {
 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);
 135                         if (added) {
 136                                 FENCE_PRINT("Found an implicit mo pattern to fix!\n");
 137                                 routineAfterAddFixes();
 138                                 return;
 139                         } else {
 140                                 // This can be a good execution, so we can't do anything,
 141                                 return;
 142                         }
 143                 }
 144                 /******** The implicit MO case (end) ********/
 145
 146                 /******** The checking data races case (beginning) ********/
 147                 bool added = addFixes(list, DATA_RACE);
 148                 if (added) {
 149                         FENCE_PRINT("Found an data race pattern to fix!\n");
 150                         routineAfterAddFixes();
 151                         return;
 152                 }
 153         }
 154 }
 155
 156 void SCFence::exitModelChecker() {
 157         model->exit_model_checker();
 158 }
 159
 160 void SCFence::restartModelChecker() {
 161         model->restart();
 162         if (!getHasRestarted())
 163                 setHasRestarted(true);
 164 }
 165
 166 bool SCFence::modelCheckerAtExitState() {
 167         return model->get_exit_flag();
 168 }
 169
 170 void SCFence::actionAtModelCheckingFinish() {
 171         // Just bail if the model checker is at the exit state
 172         if (modelCheckerAtExitState())
 173                 return;
 174
 175         /** Backtrack with a successful inference */
 176         routineBacktrack(true);
 177 }
 178
 179 void SCFence::initializeByFile() {
 180         char *name = getCandidateFile();
 181         FILE *fp = fopen(name, "r");
 182         if (fp == NULL) {
 183                 fprintf(stderr, "Cannot open the input parameter assignment file: %s!\n", name);
 184                 perror(name);
 185                 exit(EXIT_FAILURE);
 186         }
 187         Inference *infer = NULL;
 188         int curNum = 0;
 189         memory_order mo = memory_order_relaxed;
 190         char *str = (char *) malloc(sizeof(char) * (30 + 1));
 191         bool isProcessing = false;
 192         int ret = 0;
 193         while (!feof(fp)) {
 194                 // Result #:
 195                 if (!isProcessing) {
 196                         ret = fscanf(fp, "%s", str);
 197                 }
 198                 if (strcmp(str, "Result") == 0 || isProcessing) { // In an inference
 199                         ret = fscanf(fp, "%s", str);
 200
 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);
 206
 207                                 if (strcmp(str, "Result") == 0) {
 208                                         isProcessing = true;
 209                                         break;
 210                                 }
 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");
 215                                         perror(name);
 216                                         exit(EXIT_FAILURE);
 217                                 }
 218                                 ret = fscanf(fp, "%s", str);
 219
 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;
 231                         }
 232
 233                         /******** addInference ********/
 234                         if (!addInference(infer))
 235                                 delete infer;
 236                 }
 237         }
 238         fclose(fp);
 239
 240         FENCE_PRINT("candidate size from file: %d\n", setSize());
 241         Inference *next = getNextInference();
 242         if (!next) {
 243                 model_print("Wrong with the candidate file\n");
 244         } else {
 245                 setCurInference(next);
 246         }
 247 }
 248
 249 char* SCFence::parseOptionHelper(char *opt, int *optIdx) {
 250         char *res = (char*) model_malloc(1024 * sizeof(char));
 251         int resIdx = 0;
 252         while (opt[*optIdx] != '\0' && opt[*optIdx] != '|') {
 253                 res[resIdx++] = opt[(*optIdx)++];
 254         }
 255         res[resIdx] = '\0';
 256         return res;
 257 }
 258
 259 bool SCFence::parseOption(char *opt) {
 260         int optIdx = 0;
 261         char *val = NULL;
 262         while (true) {
 263                 char option = opt[optIdx++];
 264                 val = parseOptionHelper(opt, &optIdx);
 265                 switch (option) {
 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");
 270                                         return true;
 271                                 }
 272                                 break;
 273                         case 'b': // The bound above
 274                                 setImplicitMOReadBound(atoi(val));
 275                                 if (getImplicitMOReadBound() <= 0) {
 276                                         model_print("Enter valid bound value!\n");
 277                                         return true;
 278                                 }
 279                                 break;
 280                         case 'm': // Infer the modification order from repetitive reads from
 281                                           // the same write
 282                                 setInferImplicitMO(true);
 283                                 if (strcmp(val, "") != 0) {
 284                                         model_print("option m doesn't take any arguments!\n");
 285                                         return true;
 286                                 }
 287                                 break;
 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");
 292                                         return true;
 293                                 }
 294                                 break;
 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));
 299                                 break;
 300                         default:
 301                                 model_print("Unknown SCFence option: %c!\n", option);
 302                                 return true;
 303                                 break;
 304                 }
 305                 if (opt[optIdx] == '|') {
 306                         optIdx++;
 307                 } else {
 308                         break;
 309                 }
 310         }
 311         return false;
 312
 313 }
 314
 315 char* SCFence::getInputFileName(char *opt) {
 316         char *res = NULL;
 317         if (opt[0] == 'f' &&
 318                 opt[1] == 'i' &&
 319                 opt[2] == 'l' &&
 320                 opt[3] == 'e' &&
 321                 opt[4] == '-') {
 322
 323                 res = (char*) model_malloc(1024 * sizeof(char));
 324                 int i = 0, j = 5;
 325                 while (opt[j] != '\0') {
 326                         res[i++] = opt[j++];
 327                 }
 328                 res[i] = '\0';
 329         }
 330         return res;
 331 }
 332
 333 int SCFence::getImplicitMOBound(char *opt) {
 334         char *num = NULL;
 335         if (opt[0] == 'b' &&
 336                 opt[1] == 'o' &&
 337                 opt[2] == 'u' &&
 338                 opt[3] == 'n' &&
 339                 opt[4] == 'd' &&
 340                 opt[5] == '-') {
 341
 342                 num = (char*) model_malloc(1024 * sizeof(char));
 343                 int i = 0, j = 6;
 344                 while (opt[j] != '\0') {
 345                         num[i++] = opt[j++];
 346                 }
 347                 num[i] = '\0';
 348         }
 349         if (num) {
 350                 return atoi(num);
 351         } else {
 352                 return 0;
 353         }
 354 }
 355
 356 bool SCFence::option(char * opt) {
 357         char *inputFileName = NULL;
 358         unsigned implicitMOBoundNum = 0;
 359
 360         if (strcmp(opt, "verbose")==0) {
 361                 scgen->setPrintAlways(true);
 362                 return false;
 363         } else if (strcmp(opt, "buggy")==0) {
 364                 return false;
 365         } else if (strcmp(opt, "quiet")==0) {
 366                 scgen->setPrintBuggy(false);
 367                 return false;
 368         } else if (strcmp(opt, "nonsc")==0) {
 369                 scgen->setPrintNonSC(true);
 370                 return false;
 371         } else if (strcmp(opt, "time")==0) {
 372                 time=true;
 373                 return false;
 374         } else if (strcmp(opt, "no-weaken")==0) {
 375                 weaken=false;
 376                 return false;
 377         } else if (strcmp(opt, "anno")==0) {
 378                 scgen->setAnnotationMode(true);
 379                 return false;
 380         } else if (strcmp(opt, "implicit-mo")==0) {
 381                 setInferImplicitMO(true);
 382                 return false;
 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");
 386                         return true;
 387                 }
 388                 setCandidateFile(inputFileName);
 389                 initializeByFile();
 390                 return false;
 391         } else if ((implicitMOBoundNum = getImplicitMOBound(opt)) > 0) {
 392                 setImplicitMOReadBound(implicitMOBoundNum);
 393                 return false;
 394         } else {
 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");
 400                 model_print("\n");
 401                 return true;
 402         }
 403 }
 404
 405 /** Check whether a chosen reads-from path is a release sequence */
 406 bool SCFence::isReleaseSequence(path_t *path) {
 407         ASSERT (path);
 408         path_t::reverse_iterator rit = path->rbegin(),
 409                 rit_next;
 410         const ModelAction *read,
 411                 *write,
 412                 *next_read;
 413         for (; rit != path->rend(); rit++) {
 414                 read = *rit;
 415                 rit_next = rit;
 416                 rit_next++;
 417                 write = read->get_reads_from();
 418                 if (rit_next != path->rend()) {
 419                         next_read = *rit_next;
 420                         if (write != next_read) {
 421                                 return false;
 422                         }
 423                 }
 424         }
 425         return true;
 426 }
 427
 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) {
 431
 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);
 443
 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);
 450                 }
 451                 act = *readIter;
 452         }
 453         act = *writeIter;
 454         while (writeIter++ != writeThrd->rend() && act != writeBound) {
 455                 if (act->is_fence()) {
 456                         relFences->push_back(act);
 457                 }
 458                 act = *writeIter;
 459         }
 460         // Now we have a list of rel/acq fences at hand
 461         int acqFenceSize = acqFences->size(),
 462                 relFenceSize = relFences->size();
 463
 464         Patch *p;
 465         if (acqFenceSize == 0 && relFenceSize == 0) {
 466                 //return patches;
 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);
 474                 }
 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);
 482                 }
 483         } else {
 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);
 495                                         twoFences = true;
 496                                 }
 497                         }
 498                 }
 499                 if (!twoFences) {
 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);
 507                         }
 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);
 515                         }
 516                 }
 517         }
 518
 519         // If we can find a fix with fences, we don't fix on the operation
 520         if (patches->size() > 0)
 521                 return patches;
 522         p = new Patch(read, memory_order_acquire, write,
 523                 memory_order_release);
 524         if (p->isApplicable())
 525                 patches->push_back(p);
 526         return patches;
 527 }
 528
 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.
 532  */
 533 bool SCFence::imposeSync(InferenceList *inferList,
 534         paths_t *paths, const ModelAction *begin, const ModelAction *end) {
 535         if (!inferList)
 536                 return false;
 537         bool res = false;
 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))
 544                         res = true;
 545                 inferList->append(cands);
 546         }
 547         return res;
 548 }
 549
 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
 552  *  necessity.
 553  */
 554 bool SCFence::imposeSync(InferenceList *inferList,
 555         path_t *path, const ModelAction *begin, const ModelAction *end) {
 556
 557         bool release_seq = isReleaseSequence(path);
 558         SnapVector<Patch*> *patches;
 559         if (release_seq) {
 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)
 564                         return false;
 565                 inferList->applyPatch(getCurInference(), patches);
 566                 delete patches;
 567                 // Bail now for the release sequence because
 568                 return true;
 569         }
 570
 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;
 575
 576                 const ModelAction *readBound = NULL,
 577                         *writeBound = NULL;
 578                 nextRead = *++it;
 579                 if (it == path->end()) {
 580                         nextRead = NULL;
 581                 }
 582                 it--;
 583                 if (prevRead) {
 584                         readBound = prevRead->get_reads_from();
 585                 } else {
 586                         readBound = end;
 587                 }
 588                 if (nextRead) {
 589                         writeBound = nextRead;
 590                 } else {
 591                         writeBound = begin;
 592                 }
 593
 594                 /* Extend to support rel/acq fences synchronization here */
 595                 patches = getAcqRel(read, readBound, write, writeBound);
 596
 597                 if (patches->size() == 0) {
 598                         // We cannot strengthen the inference
 599                         return false;
 600                 }
 601
 602                 inferList->applyPatch(getCurInference(), patches);
 603                 delete patches;
 604         }
 605         return true;
 606 }
 607
 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.
 617  */
 618 bool SCFence::imposeSC(action_list_t * actions, InferenceList *inferList, const ModelAction *act1, const ModelAction *act2) {
 619         if (!inferList) {
 620                 return false;
 621         }
 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);
 626
 627         action_list_t::iterator it = act1Iter;
 628         it++;
 629         action_list_t *fences = new action_list_t;
 630         int size = 0;
 631         while (it != act2Iter) {
 632                 ModelAction *fence = *it;
 633                 it++;
 634                 if (!fence->is_fence())
 635                         continue;
 636                 if (!is_wildcard(fence->get_original_mo()))
 637                         continue;
 638                 fences->push_back(fence);
 639                 size++;
 640         }
 641
 642         Patch *p;
 643         SnapVector<Patch*> *patches = new SnapVector<Patch*>;
 644
 645         bool twoFences = false;
 646         // Impose SC on two fences
 647         for (action_list_t::iterator fit1 = fences->begin(); fit1 != fences->end();
 648                 fit1++) {
 649                 ModelAction *fence1 = *fit1;
 650                 action_list_t::iterator fit2 = fit1;
 651                 fit2++;
 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)
 661                                         twoFences = true;
 662                                 patches->push_back(p);
 663                         }
 664                 }
 665         }
 666
 667         // Just impose SC on one fence
 668         if (!twoFences) {
 669                 for (action_list_t::iterator fit = fences->begin(); fit != fences->end();
 670                         fit++) {
 671                         ModelAction *fence = *fit;
 672                         model_print("one fence\n");
 673                         fence->print();
 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);
 678                         }
 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);
 683                         }
 684                 }
 685
 686                 p = new Patch(act1, memory_order_seq_cst, act2, memory_order_seq_cst);
 687                 if (p->isApplicable()) {
 688                         patches->push_back(p);
 689                 }
 690         }
 691
 692         if (patches->size() > 0) {
 693                 inferList->applyPatch(getCurInference(), patches);
 694                 return true;
 695         }
 696         return false;
 697 }
 698
 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.
 706  */
 707 InferenceList* SCFence::getFixesFromPatternA(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter) {
 708         ModelAction *read = *readIter,
 709                 *write = *writeIter;
 710
 711         InferenceList *candidates = new InferenceList;
 712         paths_t *paths1, *paths2;
 713
 714         // Find all writes between the write1 and the read
 715         action_list_t *write2s = new action_list_t();
 716         ModelAction *write2;
 717         action_list_t::iterator findIt = writeIter;
 718         findIt++;
 719         do {
 720                 write2 = *findIt;
 721                 if (write2->is_write() && write2->get_location() ==
 722                         write->get_location()) {
 723                         write2s->push_back(write2);
 724                 }
 725                 findIt++;
 726         } while (findIt != readIter);
 727
 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;
 733                 write2 = *itWrite2;
 734                 // Whether the write and the write2 originally have modification order
 735                 bool isWritesMO = false;
 736                 FENCE_PRINT("write2:\n");
 737                 ACT_PRINT(write2);
 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);
 749                         } else {
 750                                 FENCE_PRINT("Have to impose sc on write1 & write2: \n");
 751                                 ACT_PRINT(write);
 752                                 ACT_PRINT(write2);
 753                                 imposeSC(list, tmpCandidates, write, write2);
 754                         }
 755                 } else {
 756                         if (!write->happens_before(write2)) {
 757                                 isWritesMO = true;
 758                         }
 759                         FENCE_PRINT("write1 mo before write2. \n");
 760                 }
 761
 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);
 770                         } else {
 771                                 FENCE_PRINT("Have to impose sc on write2 & read: \n");
 772                                 ACT_PRINT(write2);
 773                                 ACT_PRINT(read);
 774                                 imposeSC(list, tmpCandidates, write2, read);
 775                                 if (isWritesMO) {
 776                                         // Also need to make sure write -sc/hb-> write2
 777                                         FENCE_PRINT("Also have to impose hb/sc on write & write2: \n");
 778                                         ACT_PRINT(write);
 779                                         ACT_PRINT(write2);
 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);
 785                                         } else {
 786                                                 FENCE_PRINT("Also have to impose sc on write1 & write2: \n");
 787                                                 ACT_PRINT(write);
 788                                                 ACT_PRINT(write2);
 789                                                 imposeSC(list, tmpCandidates, write, write2);
 790                                         }
 791                                 }
 792                         }
 793                 } else {
 794                         FENCE_PRINT("write2 hb before read. \n");
 795                 }
 796                 candidates->append(tmpCandidates);
 797         }
 798         // Return the complete list of candidates
 799         return candidates;
 800 }
 801
 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.
 807 */
 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;
 811
 812         ModelAction *read = *readIter,
 813                 *write = *writeIter;
 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);
 820         }
 821
 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);
 827
 828         // Append the candidates to the res list
 829         res->append(candidates);
 830         return res;
 831 }
 832
 833 bool SCFence::addFixesNonSC(action_list_t *list) {
 834         bool added = false;
 835         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 836                 InferenceList *candidates = NULL;
 837                 ModelAction     *act = *it;
 838
 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(),
 848                                         list->end(), write);
 849                                 action_list_t::iterator findIt = std::find(list->begin(),
 850                                         readIter, write);
 851                                 bool readOldVal = findIt != readIter ? true : false;
 852
 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)
 857
 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);
 865                                 }
 866                                 // Just eliminate the first cycle we see in the execution
 867                                 break;
 868                         }
 869                 }
 870         }
 871         return added;
 872 }
 873
 874
 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;
 880         bool added = 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())
 887                                 continue;
 888                         for (action_list_t::iterator it = list->begin(); it !=
 889                                 list->end(); 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);
 899                                                 if (added) {
 900                                                         foundFix = true;
 901                                                         break;
 902                                                 }
 903                                         }
 904                                 }
 905                         }
 906                 }
 907                 if (foundFix)
 908                         break;
 909         }
 910
 911         return added;
 912 }
 913
 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
 919  * ever. */
 920 bool SCFence::addFixesImplicitMO(action_list_t *list) {
 921         bool added = false;
 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())
 927                         continue;
 928                 action_list_t::reverse_iterator rit1 = rit2;
 929                 rit1++;
 930                 for (; rit1 != list->rend(); rit1++) {
 931                         ModelAction *write1 = *rit1;
 932                         if (!write1->is_write() || write1->get_location() !=
 933                                 write2->get_location())
 934                                 continue;
 935                         int readCnt = 0;
 936                         action_list_t::reverse_iterator ritRead = rit2;
 937                         ritRead++;
 938                         for (; ritRead != rit1; ritRead++) {
 939                                 ModelAction *read = *ritRead;
 940                                 if (!read->is_read() || read->get_location() !=
 941                                         write1->get_location())
 942                                         continue;
 943                                 readCnt++;
 944                         }
 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
 949                                         break;
 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());
 954                                 ACT_PRINT(write1);
 955                                 ACT_PRINT(write2);
 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);
 963                                         if (added)
 964                                                 return true;
 965                                 } else {
 966                                         FENCE_PRINT("Cannot establish hb between write1 & write2: \n");
 967                                         ACT_PRINT(write1);
 968                                         ACT_PRINT(write2);
 969                                 }
 970                         }
 971                         break;
 972                 }
 973         }
 974         return false;
 975 }
 976
 977 bool SCFence::checkDataRace(action_list_t *list, ModelAction **act1,
 978         ModelAction **act2) {
 979
 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();
 983                 iter++) {
 984                 ModelAction *act = *iter;
 985                 if (act->get_original_mo() != memory_order_normal)
 986                         continue;
 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())
 993                                 continue;
 994                         foundIt = true;
 995                         list->push_back(act);
 996                 }
 997                 if (!foundIt) {
 998                         action_list_t *newList = new action_list_t;
 999                         newList->push_back(act);
1000                         opList->push_back(newList);
1001                 }
1002         }
1003
1004         if (opList->size() == 0)
1005                 return false;
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;
1013                         it2 = it1;
1014                         it2++;
1015                         for (; it2 != list->end(); it2++) {
1016                                 ModelAction *raceAct2 = *it2;
1017                                 if (!raceAct1->happens_before(raceAct2) &&
1018                                         !raceAct2->happens_before(raceAct1)) {
1019                                         *act1 = raceAct1;
1020                                         *act2 = raceAct2;
1021                                         return true;
1022                                 }
1023                         }
1024                 }
1025         }
1026         return false;
1027 }
1028
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(),
1034                 list->end(), act);
1035         return *--iter;
1036 }
1037
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(),
1043                 list->end(), act);
1044         return *++iter;
1045 }
1046
1047 bool SCFence::addFixesDataRace(action_list_t *list) {
1048         ModelAction *act1, *act2;
1049         bool hasRace = checkDataRace(list, &act1, &act2);
1050         if (hasRace) {
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));
1057                 bool added = false;
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);
1068                         }
1069                 }
1070                 return added;
1071         }
1072         return false;
1073 }
1074
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())
1078                 return false;
1079         bool added = false;
1080         switch(type) {
1081                 case BUGGY_EXECUTION:
1082                         added = addFixesBuggyExecution(list);
1083                         break;
1084                 case IMPLICIT_MO:
1085                         added = addFixesImplicitMO(list);
1086                         break;
1087                 case NON_SC:
1088                         added = addFixesNonSC(list);
1089                         break;
1090                 case DATA_RACE:
1091                         added = addFixesDataRace(list);
1092                         break;
1093                 default:
1094                         break;
1095         }
1096         if (added && isBuggy()) {
1097                 // If this is a buggy inference and we have got fixes for it, set the
1098                 // falg
1099                 setHasFixes(true);
1100         }
1101         return added;
1102 }
1103
1104
1105 bool SCFence::routineBacktrack(bool feasible) {
1106         model_print("Backtrack routine:\n");
1107
1108         /******** commitCurInference ********/
1109         Inference *curInfer = getCurInference();
1110         commitInference(curInfer, feasible);
1111         if (feasible) {
1112                 if (!isBuggy()) {
1113                         model_print("Found one result!\n");
1114                 } else if (!hasFixes()) { // Buggy and have no fixes
1115                         model_print("Found one buggy candidate!\n");
1116                 }
1117                 curInfer->print();
1118                 // Try to weaken this inference
1119                 if (weaken && !isBuggy()) {
1120                         getSet()->addWeakerInference(curInfer);
1121                 }
1122
1123         } else {
1124                 if (curInfer->getShouldFix()) {
1125                         model_print("Reach an infeasible inference!\n");
1126                 } else {
1127                         model_print("Get an unweakenable inference!\n");
1128                         curInfer->print(true);
1129                 }
1130         }
1131
1132         /******** getNextInference ********/
1133         Inference *next = getNextInference();
1134
1135         if (next) {
1136                 /******** setCurInference ********/
1137                 setCurInference(next);
1138                 /******** restartModelChecker ********/
1139                 restartModelChecker();
1140                 return true;
1141         } else {
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");
1145                 printResults();
1146                 printCandidates();
1147
1148                 /******** exitModelChecker ********/
1149                 exitModelChecker();
1150
1151                 return false;
1152         }
1153 }
1154
1155 void SCFence::routineAfterAddFixes() {
1156         model_print("Add fixes routine begin:\n");
1157
1158         /******** getNextInference ********/
1159         Inference *next = getNextInference();
1160         //ASSERT (next);
1161
1162         if (next) {
1163                 /******** setCurInference ********/
1164                 setCurInference(next);
1165                 /******** restartModelChecker ********/
1166                 restartModelChecker();
1167
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");
1172         } else {
1173                 routineBacktrack(false);
1174         }
1175 }
1176
1177
1178
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();
1189         }
1190
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();
1195         path_t *path;
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())
1201                         break;
1202                 if (!act->is_read())
1203                         continue;
1204                 // Each start with a possible path
1205                 path = new path_t();
1206                 path->push_front(act);
1207                 stack->push_back(path);
1208         }
1209         while (stack->size() > 0) {
1210                 path = stack->back();
1211                 stack->pop_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) {
1217                         delete path;
1218                         continue;
1219                 }
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
1222                  * actions
1223                  */
1224                 bool loop = false;
1225                 for (path_t::iterator p_it = path->begin(); p_it != path->end();
1226                         p_it++) {
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()) {
1231                                         // Have a loop
1232                                         delete path;
1233                                         loop = true;
1234                                         break;
1235                                 }
1236                         }
1237                 }
1238                 // Not a useful rfUsb path (loop)
1239                 if (loop) {
1240                         continue;
1241                 }
1242
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()) {
1247                         // Find a path
1248                         paths->push_back(path);
1249                         continue;
1250                 }
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
1257                                 break;
1258                         if (!act->is_read())
1259                                 continue;
1260                         path_t *new_path = new path_t(*path);
1261                         new_path->push_front(act);
1262                         stack->push_back(new_path);
1263                 }
1264                 delete path;
1265         }
1266         return paths;
1267 }
1268
1269 void SCFence::print_rf_sb_paths(paths_t *paths, const ModelAction *start, const ModelAction *end) {
1270         FENCE_PRINT("Starting from:\n");
1271         ACT_PRINT(start);
1272         FENCE_PRINT("\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),
1277                         path->size());
1278                 path_t::iterator it = path->begin(), i_next;
1279                 for (; it != path->end(); it++) {
1280                         i_next = it;
1281                         i_next++;
1282                         const ModelAction *read = *it,
1283                                 *write = read->get_reads_from(),
1284                                 *next_read = (i_next != path->end()) ? *i_next : NULL;
1285                         ACT_PRINT(write);
1286                         if (next_read == NULL || next_read->get_reads_from() != read) {
1287                                 // Not the same RMW, also print the read operation
1288                                 ACT_PRINT(read);
1289                         }
1290                 }
1291                 // Output a linebreak at the end of the path
1292                 FENCE_PRINT("\n");
1293         }
1294         FENCE_PRINT("Ending with:\n");
1295         ACT_PRINT(end);
1296 }
1297
1298 /******************** SCFence-related Functions (End) ********************/