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
 658         if(op1 == MCID_NODEP) {
 659                 record->getSet(VC_BASEINDEX + 0)->add(val1);
 660         }
 661
 662         if(op2 == MCID_NODEP) {
 663                 record->getSet(VC_BASEINDEX + 1)->add(val2);
 664         }
 665
 666         MCID eqmcid=getNextMCID();
 667         ASSERT(EPList->size()==eqmcid);
 668         EPList->push_back(epvalue);
 669         currexecpoint->incrementTop();
 670         *retval=eqmcid;
 671         return eq;
 672 }
 673
 674 /** @brief Processes an uninterpretted function. */
 675
 676 MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint numids, MCID *mcids) {
 677         bool isNew=false;
 678         EPRecord * record=getOrCreateCurrRecord(FUNCTION, &isNew, 0, numids, len, false);
 679         if (isNew) {
 680                 if (functionidentifier == 0)
 681                         record->setCompletedGoal(new CGoalSet(), false);
 682                 else {
 683                         if (sharedgoals->size()<=functionidentifier) {
 684                                 sharedgoals->resize(functionidentifier+1);
 685                                 sharedfuncrecords->resize(functionidentifier+1);
 686                         }
 687                         if ((*sharedgoals)[functionidentifier]==NULL) {
 688                                 (*sharedgoals)[functionidentifier]=new CGoalSet();
 689                                 (*sharedfuncrecords)[functionidentifier]=new RecordSet();
 690                         }
 691                         record->setCompletedGoal((*sharedgoals)[functionidentifier], true);
 692                         (*sharedfuncrecords)[functionidentifier]->add(record);
 693
 694                         for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
 695                                 EPRecord *input=getEPRecord(mcids[i-VC_BASEINDEX]);
 696                                 IntIterator *inputit=input->getReturnValueSet()->iterator();
 697                                 IntHashSet *recinputset=record->getSet(i);
 698                                 while(inputit->hasNext()) {
 699                                         uint64_t inputval=inputit->next();
 700                                         recinputset->add(inputval);
 701                                 }
 702                                 delete inputit;
 703                         }
 704
 705                         CGoalIterator *cit=(*sharedgoals)[functionidentifier]->iterator();
 706                         while(cit->hasNext()) {
 707                                 CGoal *goal=cit->next();
 708                                 evalGoal(record, goal);
 709                         }
 710                         delete cit;
 711                 }
 712         }
 713         val=val&getmask(len);
 714         EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
 715         recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
 716
 717         uint64_t valarray[numids+VC_BASEINDEX];
 718         for(uint i=0;i<VC_BASEINDEX;i++) {
 719                 valarray[i]=0;
 720         }
 721         for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
 722                 valarray[i]=getEPValue(mcids[i-VC_BASEINDEX])->getValue();
 723         }
 724
 725         MCID fnmcid=getNextMCID();
 726         ASSERT(EPList->size()==fnmcid);
 727         EPList->push_back(epvalue);
 728         currexecpoint->incrementTop();
 729
 730         CGoal *goal=new CGoal(numids+VC_BASEINDEX, valarray);
 731         if (record->completedGoalSet()->contains(goal)) {
 732                 delete goal;
 733         } else {
 734                 scheduler->setNewFlag();
 735                 planner->getConstGen()->achievedGoal(record);
 736 #ifdef PRINT_ACHIEVED_GOALS
 737                 model_print("Achieved goal:");goal->print();model_print("\n");
 738 #endif
 739 #ifdef STATS
 740                 planner->getConstGen()->curr_stat->fgoals++;
 741 #endif
 742                 goal->setOutput(val);
 743                 record->completedGoalSet()->add(goal);
 744                 recordFunctionChange(record, val);
 745                 if (functionidentifier != 0) {
 746                         RecordIterator *rit=(*sharedfuncrecords)[functionidentifier]->iterator();
 747                         while(rit->hasNext()) {
 748                                 EPRecord *func=rit->next();
 749                                 if (func == record)
 750                                         continue;
 751                                 evalGoal(func, goal);
 752                         }
 753                         delete rit;
 754                 }
 755         }
 756
 757         return fnmcid;
 758 }
 759
 760 void MCExecution::evalGoal(EPRecord *record, CGoal *goal) {
 761         for(uint i=VC_BASEINDEX;i<goal->getNum();i++) {
 762                 uint64_t input=goal->getValue(i);
 763                 if (!record->getSet(i)->contains(input))
 764                         return;
 765         }
 766         //Have all input, propagate output
 767         recordFunctionChange(record, goal->getOutput());
 768 }
 769
 770 /** @brief Returns the next thread id. */
 771
 772 thread_id_t MCExecution::get_next_tid() {
 773         return int_to_id(snap_fields->next_thread_id++);
 774 }
 775
 776 /** @brief Registers a new thread */
 777
 778 void MCExecution::add_thread(Thread *t) {
 779         ThreadList->push_back(t);
 780         ExecPoint * ep=new ExecPoint(4, t->get_id());
 781         ep->push(EP_COUNTER,0);
 782         ExecPointList->push_back(ep);
 783         CurrBranchList->push_back(NULL);
 784 #ifdef TSO
 785         storebuffer->push_back(new SnapList<EPValue *>());
 786 #endif
 787 }
 788
 789 /** @brief Records currently executing thread. */
 790
 791 void MCExecution::set_current_thread(Thread *t) {
 792         if (curr_thread) {
 793                 uint oldtid=id_to_int(curr_thread->get_id());
 794                 (*CurrBranchList)[oldtid]=currbranch;
 795         }
 796         curr_thread=t;
 797         currexecpoint=(t==NULL) ? NULL : (*ExecPointList)[id_to_int(t->get_id())];
 798         currbranch=(t==NULL) ? NULL : (*CurrBranchList)[id_to_int(t->get_id())];
 799 }
 800
 801 void MCExecution::threadStart(EPRecord *parent) {
 802         EPRecord *threadstart=getOrCreateCurrRecord(THREADBEGIN, NULL, 0, 0, 8, false);
 803         if (parent!=NULL) {
 804                 parent->setChildRecord(threadstart);
 805         }
 806         currexecpoint->incrementTop();
 807 }
 808
 809 /** @brief Create a new thread. */
 810
 811 void MCExecution::threadCreate(thrd_t *t, thrd_start_t start, void *arg) {
 812         EPRecord *threadstart=getOrCreateCurrRecord(THREADCREATE, NULL, 0, 0, 8, false);
 813         currexecpoint->incrementTop();
 814         Thread *th = new Thread(get_next_tid(), t, start, arg, curr_thread, threadstart);
 815         add_thread(th);
 816 }
 817
 818 /** @brief Joins with a thread. */
 819
 820 void MCExecution::threadJoin(Thread *blocking) {
 821         while(true) {
 822                 if (blocking->is_complete()) {
 823                         EPRecord *join=getOrCreateCurrRecord(THREADJOIN, NULL, 0, 0, 8, false);
 824                         currexecpoint->incrementTop();
 825                         join->setJoinThread(blocking->get_id());
 826                         return;
 827                 }
 828                 get_current_thread()->set_waiting(blocking);
 829                 scheduler->check_preempt();
 830                 get_current_thread()->set_waiting(NULL);
 831         }
 832 }
 833
 834 /** @brief Finishes a thread. */
 835
 836 void MCExecution::threadFinish() {
 837         Thread *th = get_current_thread();
 838         /* Wake up any joining threads */
 839         for (unsigned int i = 0;i < get_num_threads();i++) {
 840                 Thread *waiting = get_thread(int_to_id(i));
 841                 if (waiting->waiting_on() == th) {
 842                         waiting->set_waiting(NULL);
 843                 }
 844         }
 845         th->complete();
 846         scheduler->check_preempt();
 847 }
 848
 849 /** @brief Thread yield. */
 850
 851 void MCExecution::threadYield() {
 852         getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
 853         currexecpoint->incrementTop();
 854         if (model->params.noexecyields) {
 855                 threadFinish();
 856         }
 857 }
 858
 859 /** @brief Thread yield. */
 860
 861 void * MCExecution::alloc(size_t size) {
 862         bool isNew;
 863         EPRecord *record=getOrCreateCurrRecord(ALLOC, &isNew, 0, 0, 8, false);
 864         currexecpoint->incrementTop();
 865         if (isNew) {
 866                 size_t allocsize=((size<<1)+7)&~((size_t)(7));
 867                 record->setSize(allocsize);
 868                 void *ptr=real_user_malloc(size);
 869                 record->setPtr(ptr);
 870                 return ptr;
 871         } else {
 872                 if (size>record->getSize()) {
 873                         model_print("Allocation size changed too much\n");
 874                         exit(-1);
 875                 }
 876                 void *ptr=record->getPtr();
 877                 return ptr;
 878         }
 879 }
 880
 881 /** @brief Record enter loop. */
 882
 883 void MCExecution::enterLoop() {
 884         EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
 885
 886         //push the loop iteration counter
 887         currexecpoint->push(EP_LOOP,0);
 888         //push the curr iteration statement counter
 889         currexecpoint->push(EP_COUNTER,0);
 890         EPRecord * lpstartrecord=getOrCreateCurrRecord(LOOPSTART, NULL, 0, 0, 8, false);
 891         record->setChildRecord(lpstartrecord);
 892
 893         currexecpoint->incrementTop();
 894         if (DBG_ENABLED()) {
 895                 model_print("ENLOOP ");
 896                 currexecpoint->print();
 897                 model_print("\n");
 898         }
 899 }
 900
 901 /** @brief Record exit loop. */
 902
 903 void MCExecution::exitLoop() {
 904         ExecPointType type;
 905         EPRecord *breakstate=NULL;
 906
 907         /* Record last statement */
 908         uint tid=id_to_int(currexecpoint->get_tid());
 909
 910         if (!currexecpoint->directInLoop()) {
 911                 breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
 912                 currexecpoint->incrementTop();
 913         } else {
 914                 breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
 915                 currexecpoint->incrementTop();
 916         }
 917
 918         /* Get Last Record */
 919         EPRecord *lastrecord=(currbranch==NULL) ? (*alwaysexecuted)[tid] : currbranch->lastrecord;
 920
 921         /* Remember last record as loop exit for this execution.  */
 922         if (lastloopexit->size()<=tid) {
 923                 lastloopexit->resize(tid+1);
 924         }
 925         (*lastloopexit)[tid]=lastrecord;
 926
 927         do {
 928                 type=currexecpoint->getType();
 929                 currexecpoint->pop();
 930                 if (type==EP_BRANCH) {
 931                         //we crossed a branch, fix currbranch
 932                         EPRecord *branch=currbranch->getRecord();
 933                         currbranch=branch->getBranch();
 934                 }
 935         } while(type!=EP_LOOP);
 936
 937         if (DBG_ENABLED()) {
 938                 model_print("EXLOOP ");
 939                 currexecpoint->print();
 940                 model_print("\n");
 941         }
 942         EPRecord *loopenter=EPTable->get(currexecpoint);
 943         currexecpoint->incrementTop();
 944         EPRecord *labelrec=getOrCreateCurrRecord(LABEL, NULL, 0, 0, 8, false);
 945         if (loopenter->getNextRecord()==NULL) {
 946                 loopenter->setNextRecord(labelrec);
 947         }
 948         breakstate->setNextRecord(labelrec);
 949         currexecpoint->incrementTop();
 950 }
 951
 952 /** @brief Record next loop iteration. */
 953 void MCExecution::loopIterate() {
 954         currexecpoint->pop();
 955         //increment the iteration counter
 956         currexecpoint->incrementTop();
 957         currexecpoint->push(EP_COUNTER,0);
 958 }
 959
 960 /** @brief Helper function to add new item to a StoreLoadHashTable */
 961
 962 void addTable(StoreLoadHashTable *table, const void *addr, EPRecord *record) {
 963         RecordSet * rset=table->get(addr);
 964         if (rset==NULL) {
 965                 rset=new RecordSet();
 966                 table->put(addr, rset);
 967         }
 968         rset->add(record);
 969 }
 970
 971 /** @brief Update mapping from address to stores to that address. */
 972
 973 void MCExecution::addStoreTable(const void *addr, EPRecord *record) {
 974         addTable(storetable, addr, record);
 975 }
 976
 977 /** @brief Update mapping from address to loads from that address. */
 978
 979 void MCExecution::addLoadTable(const void *addr, EPRecord *record) {
 980         addTable(loadtable, addr, record);
 981 }
 982
 983 /** @brief Update mapping from address to loads from that address. */
 984
 985 RecordSet * MCExecution::getLoadTable(const void *addr) {
 986         return loadtable->get(addr);
 987 }
 988
 989 /** @brief Update mapping from address to stores to that address. */
 990
 991 RecordSet * MCExecution::getStoreTable(const void *addr) {
 992         return storetable->get(addr);
 993 }
 994
 995 /** @brief Registers that component index of deprecord depends on record. */
 996
 997 void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsigned int index) {
 998         EPRecordSet *set=eprecorddep->get(record);
 999         if (set==NULL) {
1000                 set=new EPRecordSet();
1001                 eprecorddep->put(record, set);
1002         }
1003         struct RecordIntPair pair={deprecord, index};
1004
1005         if (!set->contains(&pair)) {
1006                 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
1007                 *p=pair;
1008                 set->add(p);
1009         }
1010
1011         if (!revrecorddep->contains(&pair)) {
1012                 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
1013                 *p=pair;
1014                 revrecorddep->put(p, new ModelVector<EPRecord *>());
1015         }
1016
1017         ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
1018         for(uint i=0;i<recvec->size();i++) {
1019                 if ((*recvec)[i]==record)
1020                         return;
1021         }
1022         recvec->push_back(record);
1023 }
1024
1025 ModelVector<EPRecord *> * MCExecution::getRevDependences(EPRecord *record, uint index) {
1026         struct RecordIntPair pair={record, index};
1027         return revrecorddep->get(&pair);
1028 }