scfence/scgen.cc

   1 #include "scgen.h"
   2
   3 SCGenerator::SCGenerator() :
   4         execution(NULL),
   5         actions(NULL),
   6         cvmap(),
   7         cyclic(false),
   8         badrfset(),
   9         lastwrmap(),
  10         threadlists(1),
  11         dup_threadlists(1),
  12         print_always(false),
  13         print_buggy(false),
  14         print_nonsc(false),
  15         stats(new struct sc_statistics),
  16         annotationMode(false) {
  17 }
  18
  19 SCGenerator::~SCGenerator() {
  20 }
  21
  22 bool SCGenerator::getCyclic() {
  23         return cyclic || hasBadRF;
  24 }
  25
  26 SnapVector<action_list_t>* SCGenerator::getDupThreadLists() {
  27         return &dup_threadlists;
  28 }
  29
  30 struct sc_statistics* SCGenerator::getStats() {
  31         return stats;
  32 }
  33
  34 void SCGenerator::setExecution(ModelExecution *execution) {
  35         this->execution = execution;
  36 }
  37
  38 void SCGenerator::setActions(action_list_t *actions) {
  39         this->actions = actions;
  40 }
  41
  42 void SCGenerator::setPrintAlways(bool val) {
  43         this->print_always = val;
  44 }
  45
  46 bool SCGenerator::getPrintAlways() {
  47         return this->print_always;
  48 }
  49
  50 bool SCGenerator::getHasBadRF() {
  51         return this->hasBadRF;
  52 }
  53
  54 void SCGenerator::setPrintBuggy(bool val) {
  55         this->print_buggy = val;
  56 }
  57
  58 void SCGenerator::setPrintNonSC(bool val) {
  59         this->print_nonsc = val;
  60 }
  61
  62 void SCGenerator::setAnnotationMode(bool val) {
  63         this->annotationMode = val;
  64 }
  65
  66 action_list_t * SCGenerator::getSCList() {
  67         struct timeval start;
  68         struct timeval finish;
  69         gettimeofday(&start, NULL);
  70
  71         /* Build up the thread lists for general purpose */
  72         int thrdNum;
  73         buildVectors(&dup_threadlists, &thrdNum, actions);
  74
  75         fastVersion = true;
  76         action_list_t *list = generateSC(actions);
  77         if (cyclic) {
  78                 reset(actions);
  79                 delete list;
  80                 fastVersion = false;
  81                 list = generateSC(actions);
  82         }
  83         check_rf(list);
  84         gettimeofday(&finish, NULL);
  85         stats->elapsedtime+=((finish.tv_sec*1000000+finish.tv_usec)-(start.tv_sec*1000000+start.tv_usec));
  86         update_stats();
  87         return list;
  88 }
  89
  90 HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4> * SCGenerator::getBadrfset() {
  91         return &badrfset;
  92 }
  93
  94 HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > * SCGenerator::getAnnotatedReadSet() {
  95         return &annotatedReadSet;
  96 }
  97
  98 void SCGenerator::print_list(action_list_t *list) {
  99         model_print("---------------------------------------------------------------------\n");
 100         if (cyclic || hasBadRF)
 101                 model_print("Not SC\n");
 102         unsigned int hash = 0;
 103
 104         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 105                 const ModelAction *act = *it;
 106                 if (act->get_seq_number() > 0) {
 107                         if (badrfset.contains(act))
 108                                 model_print("BRF ");
 109                         act->print();
 110                         if (badrfset.contains(act)) {
 111                                 model_print("Desired Rf: %u \n", badrfset.get(act)->get_seq_number());
 112                         }
 113                 }
 114                 hash = hash ^ (hash << 3) ^ ((*it)->hash());
 115         }
 116         model_print("HASH %u\n", hash);
 117         model_print("---------------------------------------------------------------------\n");
 118 }
 119
 120
 121 action_list_t * SCGenerator::generateSC(action_list_t *list) {
 122         int numactions=buildVectors(&threadlists, &maxthreads, list);
 123         stats->actions+=numactions;
 124
 125         // Analyze which actions we should ignore in the partially SC analysis
 126         if (annotationMode) {
 127                 collectAnnotatedReads();
 128                 if (annotationError) {
 129                         model_print("Annotation error!\n");
 130                         return NULL;
 131                 }
 132         }
 133
 134         computeCV(list);
 135
 136         action_list_t *sclist = new action_list_t();
 137         ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
 138         int * choices = (int *) model_calloc(1, sizeof(int)*numactions);
 139         int endchoice = 0;
 140         int currchoice = 0;
 141         int lastchoice = -1;
 142         while (true) {
 143                 int numActions = getNextActions(array);
 144                 if (numActions == 0)
 145                         break;
 146                 ModelAction * act=pruneArray(array, numActions);
 147                 if (act == NULL) {
 148                         if (currchoice < endchoice) {
 149                                 act = array[choices[currchoice]];
 150                                 //check whether there is still another option
 151                                 if ((choices[currchoice]+1)<numActions)
 152                                         lastchoice=currchoice;
 153                                 currchoice++;
 154                         } else {
 155                                 act = array[0];
 156                                 choices[currchoice]=0;
 157                                 if (numActions>1)
 158                                         lastchoice=currchoice;
 159                                 currchoice++;
 160                         }
 161                 }
 162                 thread_id_t tid = act->get_tid();
 163                 //remove action
 164                 threadlists[id_to_int(tid)].pop_front();
 165                 //add ordering constraints from this choice
 166                 if (updateConstraints(act)) {
 167                         //propagate changes if we have them
 168                         bool prevc=cyclic;
 169                         computeCV(list);
 170                         if (!prevc && cyclic) {
 171                                 model_print("ROLLBACK in SC\n");
 172                                 //check whether we have another choice
 173                                 if (lastchoice != -1) {
 174                                         //have to reset everything
 175                                         choices[lastchoice]++;
 176                                         endchoice=lastchoice+1;
 177                                         currchoice=0;
 178                                         lastchoice=-1;
 179
 180                                         reset(list);
 181                                         buildVectors(&threadlists, &maxthreads, list);
 182                                         computeCV(list);
 183                                         sclist->clear();
 184                                         continue;
 185
 186                                 }
 187                         }
 188                 }
 189                 //add action to end
 190                 sclist->push_back(act);
 191         }
 192         model_free(array);
 193         return sclist;
 194 }
 195
 196 void SCGenerator::update_stats() {
 197         if (cyclic) {
 198                 stats->nonsccount++;
 199         } else {
 200                 stats->sccount++;
 201         }
 202 }
 203
 204 int SCGenerator::buildVectors(SnapVector<action_list_t> *threadlist, int *maxthread,
 205         action_list_t *list) {
 206         *maxthread = 0;
 207         int numactions = 0;
 208         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 209                 ModelAction *act = *it;
 210                 numactions++;
 211                 int threadid = id_to_int(act->get_tid());
 212                 if (threadid > *maxthread) {
 213                         threadlist->resize(threadid + 1);
 214                         *maxthread = threadid;
 215                 }
 216                 (*threadlist)[threadid].push_back(act);
 217         }
 218         return numactions;
 219 }
 220
 221
 222 bool SCGenerator::updateConstraints(ModelAction *act) {
 223         bool changed = false;
 224         for (int i = 0; i <= maxthreads; i++) {
 225                 thread_id_t tid = int_to_id(i);
 226                 if (tid == act->get_tid())
 227                         continue;
 228
 229                 action_list_t *list = &threadlists[id_to_int(tid)];
 230                 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
 231                         ModelAction *write = *rit;
 232                         if (!write->is_write())
 233                                 continue;
 234                         ClockVector *writecv = cvmap.get(write);
 235                         if (writecv->synchronized_since(act))
 236                                 break;
 237                         if (write->get_location() == act->get_location()) {
 238                                 //write is sc after act
 239                                 merge(writecv, write, act);
 240                                 changed = true;
 241                                 break;
 242                         }
 243                 }
 244         }
 245         return changed;
 246 }
 247
 248 void SCGenerator::computeCV(action_list_t *list) {
 249         bool changed = true;
 250         bool firsttime = true;
 251         ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
 252
 253         while (changed) {
 254                 changed = changed&firsttime;
 255                 firsttime = false;
 256                 bool updateFuture = false;
 257
 258                 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 259                         ModelAction *act = *it;
 260                         ModelAction *lastact = last_act[id_to_int(act->get_tid())];
 261                         if (act->is_thread_start())
 262                                 lastact = execution->get_thread(act)->get_creation();
 263                         last_act[id_to_int(act->get_tid())] = act;
 264                         ClockVector *cv = cvmap.get(act);
 265                         if (cv == NULL) {
 266                                 cv = new ClockVector(act->get_cv(), act);
 267                                 cvmap.put(act, cv);
 268                         }
 269
 270                         if (lastact != NULL) {
 271                                 merge(cv, act, lastact);
 272                         }
 273                         if (act->is_thread_join()) {
 274                                 Thread *joinedthr = act->get_thread_operand();
 275                                 ModelAction *finish = execution->get_last_action(joinedthr->get_id());
 276                                 changed |= merge(cv, act, finish);
 277                         }
 278                         if (act->is_read()) {
 279                                 if (fastVersion) {
 280                                         changed |= processReadFast(act, cv);
 281                                 } else if (annotatedReadSet.contains(act)) {
 282                                         changed |= processAnnotatedReadSlow(act, cv, &updateFuture);
 283                                 } else {
 284                                         changed |= processReadSlow(act, cv, &updateFuture);
 285                                 }
 286                         }
 287                 }
 288                 /* Reset the last action array */
 289                 if (changed) {
 290                         bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *));
 291                 } else {
 292                         if (!fastVersion) {
 293                                 if (!allowNonSC) {
 294                                         allowNonSC = true;
 295                                         changed = true;
 296                                 } else {
 297                                         break;
 298                                 }
 299                         }
 300                 }
 301         }
 302         model_free(last_act);
 303 }
 304
 305 bool SCGenerator::processReadFast(ModelAction *read, ClockVector *cv) {
 306         bool changed = false;
 307
 308         /* Merge in the clock vector from the write */
 309         const ModelAction *write = read->get_reads_from();
 310         if (!write) { // The case where the write is a promise
 311                 return false;
 312         }
 313         ClockVector *writecv = cvmap.get(write);
 314         changed |= merge(cv, read, write) && (*read < *write);
 315
 316         for (int i = 0; i <= maxthreads; i++) {
 317                 thread_id_t tid = int_to_id(i);
 318                 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
 319                 if (list == NULL)
 320                         continue;
 321                 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
 322                         ModelAction *write2 = *rit;
 323                         if (!write2->is_write())
 324                                 continue;
 325                         if (write2 == write)
 326                                 continue;
 327                         if (write2 == read) // If read is a RMW
 328                                 continue;
 329
 330                         ClockVector *write2cv = cvmap.get(write2);
 331                         if (write2cv == NULL)
 332                                 continue;
 333                         /* write -sc-> write2 &&
 334                                  write -rf-> R =>
 335                                  R -sc-> write2 */
 336                         if (write2cv->synchronized_since(write)) {
 337                                 changed |= merge(write2cv, write2, read);
 338
 339                         }
 340
 341                         //looking for earliest write2 in iteration to satisfy this
 342                         /* write2 -sc-> R &&
 343                                  write -rf-> R =>
 344                                  write2 -sc-> write */
 345                         if (cv->synchronized_since(write2)) {
 346                                 changed |= writecv == NULL || merge(writecv, write, write2);
 347                                 break;
 348                         }
 349                 }
 350         }
 351         return changed;
 352 }
 353
 354 bool SCGenerator::processReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture) {
 355         bool changed = false;
 356
 357         /* Merge in the clock vector from the write */
 358         const ModelAction *write = read->get_reads_from();
 359         ClockVector *writecv = cvmap.get(write);
 360         if ((*write < *read) || ! *updateFuture) {
 361                 bool status = merge(cv, read, write) && (*read < *write);
 362                 changed |= status;
 363                 *updateFuture = status;
 364         }
 365
 366         for (int i = 0; i <= maxthreads; i++) {
 367                 thread_id_t tid = int_to_id(i);
 368                 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
 369                 if (list == NULL)
 370                         continue;
 371                 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
 372                         ModelAction *write2 = *rit;
 373                         if (!write2->is_write())
 374                                 continue;
 375                         if (write2 == write)
 376                                 continue;
 377                         if (write2 == read) // If read is a RMW
 378                                 continue;
 379
 380                         ClockVector *write2cv = cvmap.get(write2);
 381                         if (write2cv == NULL)
 382                                 continue;
 383
 384                         /* write -sc-> write2 &&
 385                                  write -rf-> R =>
 386                                  R -sc-> write2 */
 387                         if (write2cv->synchronized_since(write)) {
 388                                 if ((*read < *write2) || ! *updateFuture) {
 389                                         bool status = merge(write2cv, write2, read);
 390                                         changed |= status;
 391                                         *updateFuture |= status && (*write2 < *read);
 392                                 }
 393                         }
 394
 395                         //looking for earliest write2 in iteration to satisfy this
 396                         /* write2 -sc-> R &&
 397                                  write -rf-> R =>
 398                                  write2 -sc-> write */
 399                         if (cv->synchronized_since(write2)) {
 400                                 if ((*write2 < *write) || ! *updateFuture) {
 401                                         bool status = writecv == NULL || merge(writecv, write, write2);
 402                                         changed |= status;
 403                                         *updateFuture |= status && (*write < *write2);
 404                                 }
 405                                 break;
 406                         }
 407                 }
 408         }
 409         return changed;
 410 }
 411
 412 bool SCGenerator::processAnnotatedReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture) {
 413         bool changed = false;
 414
 415         /* Merge in the clock vector from the write */
 416         const ModelAction *write = read->get_reads_from();
 417         if ((*write < *read) || ! *updateFuture) {
 418                 bool status = merge(cv, read, write) && (*read < *write);
 419                 changed |= status;
 420                 *updateFuture = status;
 421         }
 422         return changed;
 423 }
 424
 425 int SCGenerator::getNextActions(ModelAction **array) {
 426         int count=0;
 427
 428         for (int t = 0; t <= maxthreads; t++) {
 429                 action_list_t *tlt = &threadlists[t];
 430                 if (tlt->empty())
 431                         continue;
 432                 ModelAction *act = tlt->front();
 433                 ClockVector *cv = cvmap.get(act);
 434
 435                 /* Find the earliest in SC ordering */
 436                 for (int i = 0; i <= maxthreads; i++) {
 437                         if ( i == t )
 438                                 continue;
 439                         action_list_t *threadlist = &threadlists[i];
 440                         if (threadlist->empty())
 441                                 continue;
 442                         ModelAction *first = threadlist->front();
 443                         if (cv->synchronized_since(first)) {
 444                                 act = NULL;
 445                                 break;
 446                         }
 447                 }
 448                 if (act != NULL) {
 449                         array[count++]=act;
 450                 }
 451         }
 452         if (count != 0)
 453                 return count;
 454         for (int t = 0; t <= maxthreads; t++) {
 455                 action_list_t *tlt = &threadlists[t];
 456                 if (tlt->empty())
 457                         continue;
 458                 ModelAction *act = tlt->front();
 459                 ClockVector *cv = act->get_cv();
 460
 461                 /* Find the earliest in SC ordering */
 462                 for (int i = 0; i <= maxthreads; i++) {
 463                         if ( i == t )
 464                                 continue;
 465                         action_list_t *threadlist = &threadlists[i];
 466                         if (threadlist->empty())
 467                                 continue;
 468                         ModelAction *first = threadlist->front();
 469                         if (cv->synchronized_since(first)) {
 470                                 act = NULL;
 471                                 break;
 472                         }
 473                 }
 474                 if (act != NULL) {
 475                         array[count++]=act;
 476                 }
 477         }
 478
 479         ASSERT(count==0 || cyclic);
 480
 481         return count;
 482 }
 483
 484 bool SCGenerator::merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2) {
 485         ClockVector *cv2 = cvmap.get(act2);
 486         if (cv2 == NULL)
 487                 return true;
 488
 489         if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) {
 490                 cyclic = true;
 491                 //refuse to introduce cycles into clock vectors
 492                 return false;
 493         }
 494         if (fastVersion) {
 495                 bool status = cv->merge(cv2);
 496                 return status;
 497         } else {
 498                 bool merged;
 499                 if (allowNonSC) {
 500                         merged = cv->merge(cv2);
 501                         if (merged)
 502                                 allowNonSC = false;
 503                         return merged;
 504                 } else {
 505                         if (act2->happens_before(act) ||
 506                                 (act->is_seqcst() && act2->is_seqcst() && *act2 < *act)) {
 507                                 return cv->merge(cv2);
 508                         } else {
 509                                 return false;
 510                         }
 511                 }
 512         }
 513
 514 }
 515
 516 void SCGenerator::check_rf1(action_list_t *list) {
 517         bool hasBadRF1 = false;
 518         HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > badrfset1;
 519         HashTable<void *, const ModelAction *, uintptr_t, 4 > lastwrmap1;
 520         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 521                 const ModelAction *act = *it;
 522                 if (act->is_read()) {
 523                         if (act->get_reads_from() != lastwrmap1.get(act->get_location())) {
 524                                 badrfset1.put(act, lastwrmap1.get(act->get_location()));
 525                                 hasBadRF1 = true;
 526                         }
 527                 }
 528                 if (act->is_write())
 529                         lastwrmap1.put(act->get_location(), act);
 530         }
 531         if (cyclic != hasBadRF1 && !annotationMode) {
 532                 if (cyclic)
 533                         model_print("Assert failure & non-SC\n");
 534                 else
 535                         model_print("Assert failure & SC\n");
 536                 if (fastVersion) {
 537                         model_print("Fast\n");
 538                 } else {
 539                         model_print("Slow\n");
 540                 }
 541                 print_list(list);
 542         }
 543         if (!annotationMode) {
 544                 ASSERT (cyclic == hasBadRF1);
 545         }
 546 }
 547
 548 void SCGenerator::check_rf(action_list_t *list) {
 549         hasBadRF = false;
 550         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 551                 const ModelAction *act = *it;
 552                 if (act->is_read()) {
 553                         const ModelAction *write = act->get_reads_from();
 554                         if (write && write != lastwrmap.get(act->get_location())) {
 555                                 badrfset.put(act, lastwrmap.get(act->get_location()));
 556                                 hasBadRF = true;
 557                         }
 558                 }
 559                 if (act->is_write())
 560                         lastwrmap.put(act->get_location(), act);
 561         }
 562         if (cyclic != hasBadRF && !annotationMode) {
 563                 if (cyclic)
 564                         model_print("Assert failure & non-SC\n");
 565                 else
 566                         model_print("Assert failure & SC\n");
 567                 if (fastVersion) {
 568                         model_print("Fast\n");
 569                 } else {
 570                         model_print("Slow\n");
 571                 }
 572                 print_list(list);
 573         }
 574         if (!annotationMode) {
 575                 ASSERT (cyclic == hasBadRF);
 576         }
 577 }
 578
 579 void SCGenerator::reset(action_list_t *list) {
 580         for (int t = 0; t <= maxthreads; t++) {
 581                 action_list_t *tlt = &threadlists[t];
 582                 tlt->clear();
 583         }
 584         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 585                 ModelAction *act = *it;
 586                 delete cvmap.get(act);
 587                 cvmap.put(act, NULL);
 588         }
 589
 590         cyclic=false;
 591 }
 592
 593 ModelAction* SCGenerator::pruneArray(ModelAction **array, int count) {
 594         /* No choice */
 595         if (count == 1)
 596                 return array[0];
 597
 598         /* Choose first non-write action */
 599         ModelAction *nonwrite=NULL;
 600         for(int i=0;i<count;i++) {
 601                 if (!array[i]->is_write())
 602                         if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number())
 603                                 nonwrite = array[i];
 604         }
 605         if (nonwrite != NULL)
 606                 return nonwrite;
 607
 608         /* Look for non-conflicting action */
 609         ModelAction *nonconflict=NULL;
 610         for(int a=0;a<count;a++) {
 611                 ModelAction *act=array[a];
 612                 for (int i = 0; i <= maxthreads && act != NULL; i++) {
 613                         thread_id_t tid = int_to_id(i);
 614                         if (tid == act->get_tid())
 615                                 continue;
 616
 617                         action_list_t *list = &threadlists[id_to_int(tid)];
 618                         for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
 619                                 ModelAction *write = *rit;
 620                                 if (!write->is_write())
 621                                         continue;
 622                                 ClockVector *writecv = cvmap.get(write);
 623                                 if (writecv->synchronized_since(act))
 624                                         break;
 625                                 if (write->get_location() == act->get_location()) {
 626                                         //write is sc after act
 627                                         act = NULL;
 628                                         break;
 629                                 }
 630                         }
 631                 }
 632                 if (act != NULL) {
 633                         if (nonconflict == NULL || nonconflict->get_seq_number() > act->get_seq_number())
 634                                 nonconflict=act;
 635                 }
 636         }
 637         return nonconflict;
 638 }
 639
 640 /** This routine is operated based on the built threadlists */
 641 void SCGenerator::collectAnnotatedReads() {
 642         for (unsigned i = 1; i < threadlists.size(); i++) {
 643                 action_list_t *list = &threadlists.at(i);
 644                 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 645                         ModelAction *act = *it;
 646                         if (!IS_SC_ANNO(act))
 647                                 continue;
 648                         if (!IS_ANNO_BEGIN(act)) {
 649                                 model_print("SC annotation should begin with a BEGIN annotation\n");
 650                                 annotationError = true;
 651                                 return;
 652                         }
 653                         act = *++it;
 654                         while (!IS_ANNO_END(act) && it != list->end()) {
 655                                 // Look for the actions to keep in this loop
 656                                 ModelAction *nextAct = *++it;
 657                                 if (!IS_ANNO_KEEP(nextAct)) { // Annotated reads
 658                                         act->print();
 659                                         annotatedReadSet.put(act, act);
 660                                         annotatedReadSetSize++;
 661                                         if (IS_ANNO_END(nextAct))
 662                                                 break;
 663                                 }
 664                         }
 665                         if (it == list->end()) {
 666                                 model_print("SC annotation should end with a END annotation\n");
 667                                 annotationError = true;
 668                                 return;
 669                         }
 670                 }
 671         }
 672 }