mcexecution.cc

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 #include "mcexecution.h"
  11 #include "mcschedule.h"
  12 #include "planner.h"
  13 #include <stdarg.h>
  14 #include "cgoal.h"
  15 #include "change.h"
  16 #include "mcutil.h"
  17 #include "model.h"
  18 #include <fcntl.h>
  19 #include <unistd.h>
  20 #include <string.h>
  21 #include "constgen.h"
  22
  23 MCExecution_snapshot::MCExecution_snapshot() :
  24         next_thread_id(0)
  25 {
  26 }
  27
  28 MCExecution_snapshot::~MCExecution_snapshot() {
  29 }
  30
  31
  32 MCExecution::MCExecution() :
  33         EPTable(new EPHashTable()),
  34         EPValueTable(new EPValueHashTable()),
  35         memtable(new MemHashTable()),
  36         storetable(new StoreLoadHashTable()),
  37         loadtable(new StoreLoadHashTable()),
  38         EPList(new SnapVector<EPValue *>()),
  39         ThreadList(new SnapVector<Thread *>()),
  40         ExecPointList(new SnapVector<ExecPoint *>()),
  41         CurrBranchList(new SnapVector<EPValue *>()),
  42         currexecpoint(NULL),
  43         scheduler(new MCScheduler(this)),
  44         planner(new Planner(this)),
  45         snap_fields(new MCExecution_snapshot()),
  46         curr_thread(NULL),
  47         currbranch(NULL),
  48         eprecorddep(new EPRecordDepHashTable()),
  49         revrecorddep(new RevDepHashTable()),
  50         alwaysexecuted(new ModelVector<EPRecord *>()),
  51         lastloopexit(new ModelVector<EPRecord *>()),
  52         joinvec(new ModelVector<EPRecord *>()),
  53         sharedgoals(new ModelVector<CGoalSet *>()),
  54         sharedfuncrecords(new ModelVector<RecordSet *>()),
  55         currid(MCID_INIT),
  56         schedule_graph(0)
  57 {
  58         EPList->push_back(NULL);                        //avoid using MCID of 0
  59 #ifdef TSO
  60         storebuffer = new SnapVector<SnapList<EPValue *> *>();
  61 #endif
  62 }
  63
  64 MCExecution::~MCExecution() {
  65         reset();
  66         delete EPTable;
  67         delete EPValueTable;
  68         delete memtable;
  69         delete EPList;
  70         delete ThreadList;
  71         delete ExecPointList;
  72         delete scheduler;
  73         delete snap_fields;
  74         delete eprecorddep;
  75         delete revrecorddep;
  76         delete joinvec;
  77         delete alwaysexecuted;
  78         delete lastloopexit;
  79 #ifdef TSO
  80         for(uint i=0;i<storebuffer->size();i++) {
  81                 SnapList<EPValue *> *list=(*storebuffer)[i];
  82                 if (list != NULL)
  83                         delete list;
  84         }
  85         delete storebuffer;
  86 #endif
  87         for(uint i=0;i<sharedgoals->size();i++) {
  88                 CGoalSet *c=(*sharedgoals)[i];
  89                 if (c != NULL)
  90                         delete c;
  91         }
  92         delete sharedgoals;
  93         for(uint i=0;i<sharedfuncrecords->size();i++) {
  94                 RecordSet *rs=(*sharedfuncrecords)[i];
  95                 if (rs != NULL)
  96                         delete rs;
  97         }
  98         delete sharedfuncrecords;
  99 }
 100
 101 /** @brief Resets MCExecution object for next execution. */
 102
 103 void MCExecution::reset() {
 104         currid=MCID_INIT;
 105         currbranch=NULL;
 106         alwaysexecuted->clear();
 107 }
 108
 109 void MCExecution::dumpExecution() {
 110         char buffer[128];
 111         sprintf(buffer, "exec%u.dot",schedule_graph);
 112         schedule_graph++;
 113         int file=open(buffer,O_WRONLY|O_TRUNC|O_CREAT, S_IRWXU);
 114         model_dprintf(file, "digraph execution {\n");
 115         EPRecord *last=NULL;
 116         for(uint i=0;i<EPList->size();i++) {
 117                 EPValue *epv=(*EPList)[i];
 118                 if (epv==NULL)
 119                         continue;
 120                 EPRecord *record=epv->getRecord();
 121                 model_dprintf(file, "%lu[label=\"",(uintptr_t)record);
 122                 record->print(file);
 123                 model_dprintf(file, "\"];\n");
 124                 if (last!=NULL)
 125                         model_dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record);
 126                 last=record;
 127         }
 128         model_dprintf(file, "}\n");
 129         close(file);
 130 }
 131
 132 /** @brief Records the MCID and returns the next MCID */
 133
 134 MCID MCExecution::loadMCID(MCID maddr, uintptr_t offset) {
 135         scheduler->check_preempt();
 136         id_addr=maddr;
 137         id_addr_offset=offset;
 138         return id_retval=getNextMCID();
 139 }
 140
 141 /** @brief Records the address and value MCIDs. */
 142
 143 void MCExecution::storeMCID(MCID maddr, uintptr_t offset, MCID val) {
 144 #ifndef TSO
 145         scheduler->check_preempt();
 146 #endif
 147         id_addr=maddr;
 148         id_addr_offset=offset;
 149         id_value=val;
 150 }
 151
 152 /** @brief Records MCIDs for a RMW. */
 153
 154 MCID MCExecution::nextRMW(MCID maddr, uintptr_t offset, MCID oldval, MCID valarg) {
 155         scheduler->check_preempt();
 156         id_addr=maddr;
 157         id_addr_offset=offset;
 158         id_oldvalue=oldval;
 159         id_value=valarg;
 160         id_retval=getNextMCID();
 161         return id_retval;
 162 }
 163
 164 uint64_t dormwaction(enum atomicop op, void *addr, uint len, uint64_t currval, uint64_t oldval, uint64_t valarg, uint64_t *newval) {
 165         uint64_t retval;
 166         uint64_t memval;
 167         switch(op) {
 168         case ADD:
 169                 retval=currval;
 170                 memval=currval+valarg;
 171                 break;
 172         case CAS:
 173                 retval=currval;
 174                 if (currval==oldval) {
 175                         memval=valarg;
 176                 } else {
 177                         memval=currval;
 178                 }
 179                 break;
 180         case EXC:
 181                 retval=currval;
 182                 memval=valarg;
 183                 break;
 184         default:
 185                 ASSERT(false);
 186                 return -1;
 187         }
 188
 189         *newval=memval&getmask(len);
 190
 191         if (op==ADD || (op==CAS && (currval==oldval)) || (op == EXC)) {
 192                 switch(len) {
 193                 case 1:
 194                         *((uint8_t *)addr)=*newval;
 195                         break;
 196                 case 2:
 197                         *((uint16_t *)addr)=*newval;
 198                         break;
 199                 case 4:
 200                         *((uint32_t *)addr)=*newval;
 201                         break;
 202                 case 8:
 203                         *((uint64_t *)addr)=*newval;
 204                         break;
 205                 }
 206         }
 207         return retval;
 208 }
 209
 210 /** @brief Implement atomic RMW. */
 211 uint64_t MCExecution::rmw(enum atomicop op, void *addr, uint len, uint64_t currval, uint64_t oldval, uint64_t valarg) {
 212         uint64_t newval;
 213         uint64_t retval=dormwaction(op, addr, len, currval, oldval, valarg, &newval);
 214         if (DBG_ENABLED()) {
 215                 model_print("RMW %p oldval=%llu valarg=%llu retval=%llu", addr, oldval, valarg, retval);
 216                 currexecpoint->print();
 217                 model_print("\n");
 218         }
 219
 220         int num_mcids=(op==ADD) ? 1 : 2;
 221         EPRecord * record=getOrCreateCurrRecord(RMW, NULL, id_addr_offset, VC_RMWOUTINDEX-VC_RFINDEX, len, false);
 222         record->setRMW(op);
 223
 224         recordRMWChange(record, addr, valarg, oldval, newval);
 225         addLoadTable(addr, record);
 226         addStoreTable(addr, record);
 227         EPValue * epvalue=getEPValue(record, NULL, addr, retval, len);
 228         MCID vcrf=memtable->get(addr);
 229         MCID mcids[]={id_value, id_oldvalue};
 230         recordContext(epvalue, vcrf, id_addr, num_mcids, mcids);
 231         ASSERT(EPList->size()==id_retval);
 232         EPList->push_back(epvalue);
 233         memtable->put(addr, id_retval);
 234         currexecpoint->incrementTop();
 235         return retval;
 236 }
 237
 238 /** @brief Gets an EPRecord for the current execution point.  */
 239
 240 EPRecord * MCExecution::getOrCreateCurrRecord(EventType et, bool * isNew, uintptr_t offset,  unsigned int numinputs, uint len, bool br_anyvalue) {
 241         EPRecord *record=EPTable->get(currexecpoint);
 242         if (isNew!=NULL)
 243                 *isNew=(record==NULL);
 244         if (record==NULL) {
 245                 ExecPoint * ep=new ExecPoint(currexecpoint);
 246                 record=new EPRecord(et, ep, currbranch, offset, numinputs, len, br_anyvalue);
 247                 if (et==THREADJOIN) {
 248                         joinvec->push_back(record);
 249                 }
 250                 EPTable->put(ep, record);
 251         } else {
 252                 ASSERT(record->getOffset()==offset);
 253         }
 254         if (currbranch==NULL) {
 255                 uint tid=id_to_int(currexecpoint->get_tid());
 256                 if (alwaysexecuted->size()<=tid) {
 257                         alwaysexecuted->resize(tid+1);
 258                 }
 259                 if ((*alwaysexecuted)[tid]!=NULL && et != LABEL && et != LOOPSTART)
 260                         (*alwaysexecuted)[tid]->setNextRecord(record);
 261                 (*alwaysexecuted)[tid]=record;
 262         } else {
 263                 if (currbranch->firstrecord==NULL)
 264                         currbranch->firstrecord=record;
 265                 if (currbranch->lastrecord!=NULL && et != LABEL && et != LOOPSTART)
 266                         currbranch->lastrecord->setNextRecord(record);
 267                 currbranch->lastrecord=record;
 268         }
 269
 270         return record;
 271 }
 272
 273 /** @brief Gets an EPValue for the current record and value. */
 274
 275 EPValue * MCExecution::getEPValue(EPRecord * record, bool * isNew,  const void *addr, uint64_t val, int len) {
 276         ExecPoint * ep=record->getEP();
 277         EPValue * epvalue=new EPValue(ep, record, addr, val,len);
 278         EPValue * curr=EPValueTable->get(epvalue);
 279         if (curr!=NULL) {
 280                 if (isNew!=NULL)
 281                         *isNew=false;
 282                 delete epvalue;
 283         } else {
 284                 if (isNew!=NULL)
 285                         *isNew=true;
 286                 EPValueTable->put(epvalue, epvalue);
 287                 record->addEPValue(epvalue);
 288                 curr=epvalue;
 289         }
 290         return curr;
 291 }
 292
 293 /** @brief Lookup EPRecord for the MCID. */
 294
 295 EPRecord * MCExecution::getEPRecord(MCID id) {
 296         return (*EPList)[id]->getRecord();
 297 }
 298
 299 /** @brief Lookup EPValue for the MCID. */
 300
 301 EPValue * MCExecution::getEPValue(MCID id) {
 302         return (*EPList)[id];
 303 }
 304
 305 #ifdef TSO
 306 bool MCExecution::isEmptyStoreBuffer(thread_id_t tid) {
 307         SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
 308         return list->empty();
 309 }
 310
 311 void MCExecution::doStore(thread_id_t tid) {
 312         SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
 313         EPValue * epval=list->front();
 314         list->pop_front();
 315         if (DBG_ENABLED()) {
 316                 model_print("tid = %d: ", tid);
 317         }
 318         doStore(epval);
 319 }
 320
 321 void MCExecution::doStore(EPValue *epval) {
 322         const void *addr=epval->getAddr();
 323         uint64_t val=epval->getValue();
 324         int len=epval->getLen();
 325         if (DBG_ENABLED()) {
 326                 model_print("flushing %d bytes *(%p) = %llu", len, addr, val);
 327                 currexecpoint->print();
 328                 model_print("\n");
 329         }
 330         switch(len) {
 331         case 1:
 332                 (*(uint8_t *)addr) = (uint8_t)val;
 333                 break;
 334         case 2:
 335                 (*(uint16_t *)addr) = (uint16_t)val;
 336                 break;
 337         case 4:
 338                 (*(uint32_t *)addr) = (uint32_t)val;
 339                 break;
 340         case 8:
 341                 (*(uint64_t *)addr) = (uint64_t)val;
 342                 break;
 343         }
 344 }
 345
 346 void MCExecution::fence() {
 347         scheduler->check_preempt();
 348         getOrCreateCurrRecord(FENCE, NULL, 0, 0, 8, false);
 349         currexecpoint->incrementTop();
 350         uint tid=id_to_int(currexecpoint->get_tid());
 351         SnapList<EPValue *> * list=(*storebuffer)[tid];
 352         while(!list->empty()) {
 353                 EPValue * epval=list->front();
 354                 list->pop_front();
 355                 doStore(epval);
 356         }
 357 }
 358 #endif
 359
 360 /** @brief EPValue is the corresponding epvalue object.
 361                 For loads rf is the store we read from.
 362                 For loads or stores, addr is the MCID for the provided address.
 363                 numids is the number of MCID's we take in.
 364                 We then list that number of MCIDs for everything we depend on.
 365  */
 366
 367 void MCExecution::recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids) {
 368         EPRecord *currrecord=epv->getRecord();
 369
 370         for(int i=0;i<numids;i++) {
 371                 MCID id=mcids[i];
 372                 if (id != MCID_NODEP) {
 373                         EPRecord * epi=getEPRecord(id);
 374                         addRecordDepTable(epi,currrecord, VC_BASEINDEX+i);
 375                 }
 376         }
 377         if (rf != MCID_NODEP) {
 378                 EPRecord *eprf=getEPRecord(rf);
 379                 addRecordDepTable(eprf,currrecord, VC_RFINDEX);
 380         }
 381         if (addr != MCID_NODEP) {
 382                 EPRecord *epaddr=getEPRecord(addr);
 383                 addRecordDepTable(epaddr,currrecord, VC_ADDRINDEX);
 384         }
 385 }
 386
 387 /** @brief Processes a store. */
 388
 389 void MCExecution::store(void *addr, uint64_t val, int len) {
 390 #ifndef TSO
 391         switch(len) {
 392         case 1:
 393                 (*(uint8_t *)addr) = (uint8_t)val;
 394                 break;
 395         case 2:
 396                 (*(uint16_t *)addr) = (uint16_t)val;
 397                 break;
 398         case 4:
 399                 (*(uint32_t *)addr) = (uint32_t)val;
 400                 break;
 401         case 8:
 402                 (*(uint64_t *)addr) = (uint64_t)val;
 403                 break;
 404         }
 405 #endif
 406
 407         if (DBG_ENABLED()) {
 408                 model_print("STORE *%p=%llu ", addr, val);
 409                 currexecpoint->print();
 410                 model_print("\n");
 411         }
 412         EPRecord * record=getOrCreateCurrRecord(STORE, NULL, id_addr_offset, 1, len, false);
 413         recordStoreChange(record, addr, val);
 414         addStoreTable(addr, record);
 415         EPValue * epvalue=getEPValue(record, NULL, addr, val, len);
 416 #ifdef TSO
 417         uint tid=id_to_int(currexecpoint->get_tid());
 418         (*storebuffer)[tid]->push_back(epvalue);
 419 #endif
 420         MCID mcids[]={id_value};
 421         recordContext(epvalue, MCID_NODEP, id_addr, 1, mcids);
 422         MCID stmcid=getNextMCID();
 423         ASSERT(stmcid==EPList->size());
 424         EPList->push_back(epvalue);
 425         memtable->put(addr, stmcid);
 426         currexecpoint->incrementTop();
 427 }
 428
 429 void MCExecution::recordFunctionChange(EPRecord *function, uint64_t val) {
 430         if (function->getSet(VC_FUNCOUTINDEX)->add(val))
 431                 planner->addChange(new MCChange(function, val, VC_FUNCOUTINDEX));
 432 }
 433
 434 void MCExecution::recordRMWChange(EPRecord *rmw, const void *addr, uint64_t valarg, uint64_t oldval, uint64_t newval) {
 435         if (!rmw->hasAddr(addr)) {
 436                 rmw->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
 437                 planner->addChange(new MCChange(rmw, (uint64_t)addr, VC_ADDRINDEX));
 438         }
 439         rmw->getSet(VC_BASEINDEX)->add(valarg);
 440         if (rmw->getOp()==CAS)
 441                 rmw->getSet(VC_OLDVALCASINDEX)->add(oldval);
 442         if (!rmw->getSet(VC_RMWOUTINDEX)->contains(newval)) {
 443                 rmw->getSet(VC_RMWOUTINDEX)->add(newval);
 444                 planner->addChange(new MCChange(rmw, newval, VC_RMWOUTINDEX));
 445         }
 446 }
 447
 448 void MCExecution::recordLoadChange(EPRecord *load, const void *addr) {
 449         if (!load->hasAddr(addr)) {
 450                 load->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
 451                 planner->addChange(new MCChange(load, (uint64_t)addr, VC_ADDRINDEX));
 452         }
 453 }
 454
 455 void MCExecution::recordStoreChange(EPRecord *store, const void *addr, uint64_t val) {
 456         if (!store->hasAddr(addr)) {
 457                 store->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
 458                 planner->addChange(new MCChange(store, (uint64_t)addr, VC_ADDRINDEX));
 459         }
 460         if (!store->hasValue(val)) {
 461                 store->getSet(VC_BASEINDEX)->add(val);
 462                 planner->addChange(new MCChange(store, val, VC_BASEINDEX));
 463         }
 464 }
 465
 466 /** @brief Processes a load. */
 467
 468 uint64_t MCExecution::load(const void *addr, int len) {
 469 #ifdef TSO
 470         uint64_t val=0;
 471         bool found=false;
 472         uint tid=id_to_int(currexecpoint->get_tid());
 473         SnapList<EPValue *> *list=(*storebuffer)[tid];
 474         for(SnapList<EPValue *>::reverse_iterator it=list->rbegin();it != list->rend();it++) {
 475                 EPValue *epval=*it;
 476                 const void *epaddr=epval->getAddr();
 477                 if (epaddr == addr) {
 478                         val = epval->getValue();
 479                         found = true;
 480                         break;
 481                 }
 482         }
 483         if (!found) {
 484                 switch(len) {
 485                 case 1:
 486                         val=*(uint8_t *) addr;
 487                         break;
 488                 case 2:
 489                         val=*(uint16_t *) addr;
 490                         break;
 491                 case 4:
 492                         val=*(uint32_t *) addr;
 493                         break;
 494                 case 8:
 495                         val=*(uint64_t *) addr;
 496                         break;
 497                 }
 498         }
 499 #else
 500         uint64_t val=0;
 501         switch(len) {
 502         case 1:
 503                 val=*(uint8_t *) addr;
 504                 break;
 505         case 2:
 506                 val=*(uint16_t *) addr;
 507                 break;
 508         case 4:
 509                 val=*(uint32_t *) addr;
 510                 break;
 511         case 8:
 512                 val=*(uint64_t *) addr;
 513                 break;
 514         }
 515 #endif
 516
 517         if (DBG_ENABLED()) {
 518                 model_print("%llu(mid=%u)=LOAD %p ", val, id_retval, addr);
 519                 currexecpoint->print();
 520                 model_print("\n");
 521         }
 522         ASSERT(id_addr==MCID_NODEP || (getEPValue(id_addr)->getValue()+id_addr_offset)==((uint64_t)addr));
 523         EPRecord * record=getOrCreateCurrRecord(LOAD, NULL, id_addr_offset, 0, len, false);
 524         recordLoadChange(record, addr);
 525         addLoadTable(addr, record);
 526         EPValue * epvalue=getEPValue(record, NULL, addr, val, len);
 527         MCID vcrf=memtable->get(addr);
 528         recordContext(epvalue, vcrf, id_addr, 0, NULL);
 529         ASSERT(EPList->size()==id_retval);
 530         EPList->push_back(epvalue);
 531         currexecpoint->incrementTop();
 532         return val;
 533 }
 534
 535 /** @brief Processes a branch. */
 536
 537 MCID MCExecution::branchDir(MCID dirid, int direction, int numdirs, bool anyvalue) {
 538         if (DBG_ENABLED()) {
 539                 model_print("BRANCH dir=%u mid=%u", direction, dirid);
 540                 currexecpoint->print();
 541                 model_print("\n");
 542         }
 543         EPRecord * record=getOrCreateCurrRecord(BRANCHDIR, NULL, 0, 1, numdirs, anyvalue);
 544         bool isNew;
 545         EPValue * epvalue=getEPValue(record, &isNew, NULL, direction, 32);
 546         if (isNew) {
 547 #ifdef PRINT_ACHIEVED_GOALS
 548                 model_print("Achieved Goal: BRANCH dir=%u mid=%u", direction, dirid);
 549                 currexecpoint->print();model_print("\n");
 550 #endif
 551 #ifdef STATS
 552                 planner->getConstGen()->curr_stat->bgoals++;
 553 #endif
 554                 planner->getConstGen()->achievedGoal(record);
 555                 scheduler->setNewFlag();
 556         }
 557         //record that we took a branch
 558         currbranch=epvalue;
 559         currbranch->lastrecord=NULL;
 560         MCID mcids[]={dirid};
 561         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
 562         MCID brmcid=getNextMCID();
 563         ASSERT(EPList->size()==brmcid);
 564         EPList->push_back(epvalue);
 565         //push the direction of the branch
 566         currexecpoint->push(EP_BRANCH,direction);
 567         //push the statement counter for the branch
 568         currexecpoint->push(EP_COUNTER,0);
 569
 570         return brmcid;
 571 }
 572
 573 /** @brief Processes a merge with a previous branch.  mcid gives the
 574                 branch we merged. */
 575
 576 void MCExecution::merge(MCID mcid) {
 577         EPValue * epvalue=getEPValue(mcid);
 578         ExecPoint *ep=epvalue->getEP();
 579         //rollback current branch
 580         currbranch=EPTable->get(ep)->getBranch();
 581         int orig_length=ep->getSize();
 582         int curr_length=currexecpoint->getSize();
 583         for(int i=0;i<curr_length-orig_length;i++)
 584                 currexecpoint->pop();
 585         //increment top
 586         currexecpoint->incrementTop();
 587         //now we can create the merge point
 588         if (DBG_ENABLED()) {
 589                 model_print("MERGE mid=%u", mcid);
 590                 currexecpoint->print();
 591                 model_print("\n");
 592         }
 593         getOrCreateCurrRecord(MERGE, NULL, 0, 0, 8, false);
 594         currexecpoint->incrementTop();
 595 }
 596
 597 /** @brief Phi function. */
 598 MCID MCExecution::phi(MCID input) {
 599         EPRecord * record=getOrCreateCurrRecord(FUNCTION, NULL, 0, 1, 8, false);
 600         record->setPhi();
 601         EPValue *epinput=getEPValue(input);
 602         EPValue * epvalue=getEPValue(record, NULL, NULL, epinput->getValue(), 8);
 603
 604         MCID mcids[]={input};
 605         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
 606
 607         MCID fnmcid=getNextMCID();
 608         ASSERT(EPList->size()==fnmcid);
 609         EPList->push_back(epvalue);
 610         currexecpoint->incrementTop();
 611
 612         return fnmcid;
 613 }
 614
 615 /** @brief Phi function for loops. */
 616 MCID MCExecution::loop_phi(MCID input) {
 617         EPRecord * record=getOrCreateCurrRecord(FUNCTION, NULL, 0, 1, 8, false);
 618         record->setLoopPhi();
 619         EPValue *epinput=getEPValue(input);
 620         EPValue * epvalue=getEPValue(record, NULL, NULL, epinput->getValue(), 8);
 621
 622         MCID mcids[]={input};
 623         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
 624
 625         uint tid=id_to_int(currexecpoint->get_tid());
 626         EPRecord *exitrec=(*lastloopexit)[tid];
 627
 628         EPRecordIDSet *phiset=record->getPhiLoopTable();
 629         struct RecordIDPair rip={exitrec,getEPRecord(input)};
 630         if (!phiset->contains(&rip)) {
 631                 struct RecordIDPair *p=(struct RecordIDPair *)model_malloc(sizeof(struct RecordIDPair));
 632                 *p=rip;
 633                 phiset->add(p);
 634         }
 635
 636         MCID fnmcid=getNextMCID();
 637         ASSERT(EPList->size()==fnmcid);
 638         EPList->push_back(epvalue);
 639         currexecpoint->incrementTop();
 640
 641         return fnmcid;
 642 }
 643
 644 uint64_t MCExecution::equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, MCID *retval) {
 645         uint64_t eq=(val1==val2);
 646         bool isNew=false;
 647         int len=8;
 648         EPRecord * record=getOrCreateCurrRecord(EQUALS, &isNew, 0, 2, len, false);
 649         EPValue * epvalue=getEPValue(record, NULL, NULL, eq, len);
 650         getEPValue(record, NULL, NULL, 1-eq, len);
 651         MCID mcids[]={op1, op2};
 652         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 2, mcids);
 653         if (isNew) {
 654                 recordFunctionChange(record, 0);
 655                 recordFunctionChange(record, 1);
 656         }
 657         MCID eqmcid=getNextMCID();
 658         ASSERT(EPList->size()==eqmcid);
 659         EPList->push_back(epvalue);
 660         currexecpoint->incrementTop();
 661         *retval=eqmcid;
 662         return eq;
 663 }
 664
 665 /** @brief Processes an uninterpretted function. */
 666
 667 MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint numids, MCID *mcids) {
 668         bool isNew=false;
 669         EPRecord * record=getOrCreateCurrRecord(FUNCTION, &isNew, 0, numids, len, false);
 670         if (isNew) {
 671                 if (functionidentifier == 0)
 672                         record->setCompletedGoal(new CGoalSet(), false);
 673                 else {
 674                         if (sharedgoals->size()<=functionidentifier) {
 675                                 sharedgoals->resize(functionidentifier+1);
 676                                 sharedfuncrecords->resize(functionidentifier+1);
 677                         }
 678                         if ((*sharedgoals)[functionidentifier]==NULL) {
 679                                 (*sharedgoals)[functionidentifier]=new CGoalSet();
 680                                 (*sharedfuncrecords)[functionidentifier]=new RecordSet();
 681                         }
 682                         record->setCompletedGoal((*sharedgoals)[functionidentifier], true);
 683                         (*sharedfuncrecords)[functionidentifier]->add(record);
 684
 685                         for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
 686                                 EPRecord *input=getEPRecord(mcids[i-VC_BASEINDEX]);
 687                                 IntIterator *inputit=input->getReturnValueSet()->iterator();
 688                                 IntHashSet *recinputset=record->getSet(i);
 689                                 while(inputit->hasNext()) {
 690                                         uint64_t inputval=inputit->next();
 691                                         recinputset->add(inputval);
 692                                 }
 693                                 delete inputit;
 694                         }
 695
 696                         CGoalIterator *cit=(*sharedgoals)[functionidentifier]->iterator();
 697                         while(cit->hasNext()) {
 698                                 CGoal *goal=cit->next();
 699                                 evalGoal(record, goal);
 700                         }
 701                         delete cit;
 702                 }
 703         }
 704         val=val&getmask(len);
 705         EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
 706         recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
 707
 708         uint64_t valarray[numids+VC_BASEINDEX];
 709         for(uint i=0;i<VC_BASEINDEX;i++) {
 710                 valarray[i]=0;
 711         }
 712         for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
 713                 valarray[i]=getEPValue(mcids[i-VC_BASEINDEX])->getValue();
 714         }
 715
 716         MCID fnmcid=getNextMCID();
 717         ASSERT(EPList->size()==fnmcid);
 718         EPList->push_back(epvalue);
 719         currexecpoint->incrementTop();
 720
 721         CGoal *goal=new CGoal(numids+VC_BASEINDEX, valarray);
 722         if (record->completedGoalSet()->contains(goal)) {
 723                 delete goal;
 724         } else {
 725                 scheduler->setNewFlag();
 726                 planner->getConstGen()->achievedGoal(record);
 727 #ifdef PRINT_ACHIEVED_GOALS
 728                 model_print("Achieved goal:");goal->print();model_print("\n");
 729 #endif
 730 #ifdef STATS
 731                 planner->getConstGen()->curr_stat->fgoals++;
 732 #endif
 733                 goal->setOutput(val);
 734                 record->completedGoalSet()->add(goal);
 735                 recordFunctionChange(record, val);
 736                 if (functionidentifier != 0) {
 737                         RecordIterator *rit=(*sharedfuncrecords)[functionidentifier]->iterator();
 738                         while(rit->hasNext()) {
 739                                 EPRecord *func=rit->next();
 740                                 if (func == record)
 741                                         continue;
 742                                 evalGoal(func, goal);
 743                         }
 744                         delete rit;
 745                 }
 746         }
 747
 748         return fnmcid;
 749 }
 750
 751 void MCExecution::evalGoal(EPRecord *record, CGoal *goal) {
 752         for(uint i=VC_BASEINDEX;i<goal->getNum();i++) {
 753                 uint64_t input=goal->getValue(i);
 754                 if (!record->getSet(i)->contains(input))
 755                         return;
 756         }
 757         //Have all input, propagate output
 758         recordFunctionChange(record, goal->getOutput());
 759 }
 760
 761 /** @brief Returns the next thread id. */
 762
 763 thread_id_t MCExecution::get_next_tid() {
 764         return int_to_id(snap_fields->next_thread_id++);
 765 }
 766
 767 /** @brief Registers a new thread */
 768
 769 void MCExecution::add_thread(Thread *t) {
 770         ThreadList->push_back(t);
 771         ExecPoint * ep=new ExecPoint(4, t->get_id());
 772         ep->push(EP_COUNTER,0);
 773         ExecPointList->push_back(ep);
 774         CurrBranchList->push_back(NULL);
 775 #ifdef TSO
 776         storebuffer->push_back(new SnapList<EPValue *>());
 777 #endif
 778 }
 779
 780 /** @brief Records currently executing thread. */
 781
 782 void MCExecution::set_current_thread(Thread *t) {
 783         if (curr_thread) {
 784                 uint oldtid=id_to_int(curr_thread->get_id());
 785                 (*CurrBranchList)[oldtid]=currbranch;
 786         }
 787         curr_thread=t;
 788         currexecpoint=(t==NULL) ? NULL : (*ExecPointList)[id_to_int(t->get_id())];
 789         currbranch=(t==NULL) ? NULL : (*CurrBranchList)[id_to_int(t->get_id())];
 790 }
 791
 792 void MCExecution::threadStart(EPRecord *parent) {
 793         EPRecord *threadstart=getOrCreateCurrRecord(THREADBEGIN, NULL, 0, 0, 8, false);
 794         if (parent!=NULL) {
 795                 parent->setChildRecord(threadstart);
 796         }
 797         currexecpoint->incrementTop();
 798 }
 799
 800 /** @brief Create a new thread. */
 801
 802 void MCExecution::threadCreate(thrd_t *t, thrd_start_t start, void *arg) {
 803         EPRecord *threadstart=getOrCreateCurrRecord(THREADCREATE, NULL, 0, 0, 8, false);
 804         currexecpoint->incrementTop();
 805         Thread *th = new Thread(get_next_tid(), t, start, arg, curr_thread, threadstart);
 806         add_thread(th);
 807 }
 808
 809 /** @brief Joins with a thread. */
 810
 811 void MCExecution::threadJoin(Thread *blocking) {
 812         while(true) {
 813                 if (blocking->is_complete()) {
 814                         EPRecord *join=getOrCreateCurrRecord(THREADJOIN, NULL, 0, 0, 8, false);
 815                         currexecpoint->incrementTop();
 816                         join->setJoinThread(blocking->get_id());
 817                         return;
 818                 }
 819                 get_current_thread()->set_waiting(blocking);
 820                 scheduler->check_preempt();
 821                 get_current_thread()->set_waiting(NULL);
 822         }
 823 }
 824
 825 /** @brief Finishes a thread. */
 826
 827 void MCExecution::threadFinish() {
 828         Thread *th = get_current_thread();
 829         /* Wake up any joining threads */
 830         for (unsigned int i = 0;i < get_num_threads();i++) {
 831                 Thread *waiting = get_thread(int_to_id(i));
 832                 if (waiting->waiting_on() == th) {
 833                         waiting->set_waiting(NULL);
 834                 }
 835         }
 836         th->complete();
 837         scheduler->check_preempt();
 838 }
 839
 840 /** @brief Thread yield. */
 841
 842 void MCExecution::threadYield() {
 843         getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
 844         currexecpoint->incrementTop();
 845         if (model->params.noexecyields) {
 846                 threadFinish();
 847         }
 848 }
 849
 850 /** @brief Thread yield. */
 851
 852 void * MCExecution::alloc(size_t size) {
 853         bool isNew;
 854         EPRecord *record=getOrCreateCurrRecord(ALLOC, &isNew, 0, 0, 8, false);
 855         currexecpoint->incrementTop();
 856         if (isNew) {
 857                 size_t allocsize=((size<<1)+7)&~((size_t)(7));
 858                 record->setSize(allocsize);
 859                 void *ptr=real_user_malloc(size);
 860                 record->setPtr(ptr);
 861                 return ptr;
 862         } else {
 863                 if (size>record->getSize()) {
 864                         model_print("Allocation size changed too much\n");
 865                         exit(-1);
 866                 }
 867                 void *ptr=record->getPtr();
 868                 return ptr;
 869         }
 870 }
 871
 872 /** @brief Record enter loop. */
 873
 874 void MCExecution::enterLoop() {
 875         EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
 876
 877         //push the loop iteration counter
 878         currexecpoint->push(EP_LOOP,0);
 879         //push the curr iteration statement counter
 880         currexecpoint->push(EP_COUNTER,0);
 881         EPRecord * lpstartrecord=getOrCreateCurrRecord(LOOPSTART, NULL, 0, 0, 8, false);
 882         record->setChildRecord(lpstartrecord);
 883
 884         currexecpoint->incrementTop();
 885         if (DBG_ENABLED()) {
 886                 model_print("ENLOOP ");
 887                 currexecpoint->print();
 888                 model_print("\n");
 889         }
 890 }
 891
 892 /** @brief Record exit loop. */
 893
 894 void MCExecution::exitLoop() {
 895         ExecPointType type;
 896         EPRecord *breakstate=NULL;
 897
 898         /* Record last statement */
 899         uint tid=id_to_int(currexecpoint->get_tid());
 900
 901         if (!currexecpoint->directInLoop()) {
 902                 breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
 903                 currexecpoint->incrementTop();
 904         } else {
 905                 breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
 906                 currexecpoint->incrementTop();
 907         }
 908
 909         /* Get Last Record */
 910         EPRecord *lastrecord=(currbranch==NULL) ? (*alwaysexecuted)[tid] : currbranch->lastrecord;
 911
 912         /* Remember last record as loop exit for this execution.  */
 913         if (lastloopexit->size()<=tid) {
 914                 lastloopexit->resize(tid+1);
 915         }
 916         (*lastloopexit)[tid]=lastrecord;
 917
 918         do {
 919                 type=currexecpoint->getType();
 920                 currexecpoint->pop();
 921                 if (type==EP_BRANCH) {
 922                         //we crossed a branch, fix currbranch
 923                         EPRecord *branch=currbranch->getRecord();
 924                         currbranch=branch->getBranch();
 925                 }
 926         } while(type!=EP_LOOP);
 927
 928         if (DBG_ENABLED()) {
 929                 model_print("EXLOOP ");
 930                 currexecpoint->print();
 931                 model_print("\n");
 932         }
 933         EPRecord *loopenter=EPTable->get(currexecpoint);
 934         currexecpoint->incrementTop();
 935         EPRecord *labelrec=getOrCreateCurrRecord(LABEL, NULL, 0, 0, 8, false);
 936         if (loopenter->getNextRecord()==NULL) {
 937                 loopenter->setNextRecord(labelrec);
 938         }
 939         breakstate->setNextRecord(labelrec);
 940         currexecpoint->incrementTop();
 941 }
 942
 943 /** @brief Record next loop iteration. */
 944 void MCExecution::loopIterate() {
 945         currexecpoint->pop();
 946         //increment the iteration counter
 947         currexecpoint->incrementTop();
 948         currexecpoint->push(EP_COUNTER,0);
 949 }
 950
 951 /** @brief Helper function to add new item to a StoreLoadHashTable */
 952
 953 void addTable(StoreLoadHashTable *table, const void *addr, EPRecord *record) {
 954         RecordSet * rset=table->get(addr);
 955         if (rset==NULL) {
 956                 rset=new RecordSet();
 957                 table->put(addr, rset);
 958         }
 959         rset->add(record);
 960 }
 961
 962 /** @brief Update mapping from address to stores to that address. */
 963
 964 void MCExecution::addStoreTable(const void *addr, EPRecord *record) {
 965         addTable(storetable, addr, record);
 966 }
 967
 968 /** @brief Update mapping from address to loads from that address. */
 969
 970 void MCExecution::addLoadTable(const void *addr, EPRecord *record) {
 971         addTable(loadtable, addr, record);
 972 }
 973
 974 /** @brief Update mapping from address to loads from that address. */
 975
 976 RecordSet * MCExecution::getLoadTable(const void *addr) {
 977         return loadtable->get(addr);
 978 }
 979
 980 /** @brief Update mapping from address to stores to that address. */
 981
 982 RecordSet * MCExecution::getStoreTable(const void *addr) {
 983         return storetable->get(addr);
 984 }
 985
 986 /** @brief Registers that component index of deprecord depends on record. */
 987
 988 void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsigned int index) {
 989         EPRecordSet *set=eprecorddep->get(record);
 990         if (set==NULL) {
 991                 set=new EPRecordSet();
 992                 eprecorddep->put(record, set);
 993         }
 994         struct RecordIntPair pair={deprecord, index};
 995
 996         if (!set->contains(&pair)) {
 997                 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
 998                 *p=pair;
 999                 set->add(p);
1000         }
1001
1002         if (!revrecorddep->contains(&pair)) {
1003                 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
1004                 *p=pair;
1005                 revrecorddep->put(p, new ModelVector<EPRecord *>());
1006         }
1007
1008         ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
1009         for(uint i=0;i<recvec->size();i++) {
1010                 if ((*recvec)[i]==record)
1011                         return;
1012         }
1013         recvec->push_back(record);
1014 }
1015
1016 ModelVector<EPRecord *> * MCExecution::getRevDependences(EPRecord *record, uint index) {
1017         struct RecordIntPair pair={record, index};
1018         return revrecorddep->get(&pair);
1019 }