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         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                 dprintf(file, "%lu[label=\"",(uintptr_t)record);
 122                 record->print(file);
 123                 dprintf(file, "\"];\n");
 124                 if (last!=NULL)
 125                         dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record);
 126                 last=record;
 127         }
 128         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=%lu valarg=%lu retval=%lu", 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         doStore(epval);
 316 }
 317
 318 void MCExecution::doStore(EPValue *epval) {
 319         const void *addr=epval->getAddr();
 320         uint64_t val=epval->getValue();
 321         int len=epval->getLen();
 322         if (DBG_ENABLED()) {
 323                 model_print("flushing %d bytes *(%p) = %lu", len, addr, val);
 324                 currexecpoint->print();
 325                 model_print("\n");
 326         }
 327         switch(len) {
 328         case 1:
 329                 (*(uint8_t *)addr) = (uint8_t)val;
 330                 break;
 331         case 2:
 332                 (*(uint16_t *)addr) = (uint16_t)val;
 333                 break;
 334         case 4:
 335                 (*(uint32_t *)addr) = (uint32_t)val;
 336                 break;
 337         case 8:
 338                 (*(uint64_t *)addr) = (uint64_t)val;
 339                 break;
 340         }
 341 }
 342
 343 void MCExecution::fence() {
 344         scheduler->check_preempt();
 345         getOrCreateCurrRecord(FENCE, NULL, 0, 0, 8, false);
 346         currexecpoint->incrementTop();
 347         uint tid=id_to_int(currexecpoint->get_tid());
 348         SnapList<EPValue *> * list=(*storebuffer)[tid];
 349         while(!list->empty()) {
 350                 EPValue * epval=list->front();
 351                 list->pop_front();
 352                 doStore(epval);
 353         }
 354 }
 355 #endif
 356
 357 /** @brief EPValue is the corresponding epvalue object.
 358                 For loads rf is the store we read from.
 359                 For loads or stores, addr is the MCID for the provided address.
 360                 numids is the number of MCID's we take in.
 361                 We then list that number of MCIDs for everything we depend on.
 362 */
 363
 364 void MCExecution::recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids) {
 365         EPRecord *currrecord=epv->getRecord();
 366
 367         for(int i=0;i<numids;i++) {
 368                 MCID id=mcids[i];
 369                 if (id != MCID_NODEP) {
 370                         EPRecord * epi=getEPRecord(id);
 371                         addRecordDepTable(epi,currrecord, VC_BASEINDEX+i);
 372                 }
 373         }
 374         if (rf != MCID_NODEP) {
 375                 EPRecord *eprf=getEPRecord(rf);
 376                 addRecordDepTable(eprf,currrecord, VC_RFINDEX);
 377         }
 378         if (addr != MCID_NODEP) {
 379                 EPRecord *epaddr=getEPRecord(addr);
 380                 addRecordDepTable(epaddr,currrecord, VC_ADDRINDEX);
 381         }
 382 }
 383
 384 /** @brief Processes a store. */
 385
 386 void MCExecution::store(void *addr, uint64_t val, int len) {
 387 #ifndef TSO
 388         switch(len) {
 389         case 1:
 390                 (*(uint8_t *)addr) = (uint8_t)val;
 391                 break;
 392         case 2:
 393                 (*(uint16_t *)addr) = (uint16_t)val;
 394                 break;
 395         case 4:
 396                 (*(uint32_t *)addr) = (uint32_t)val;
 397                 break;
 398         case 8:
 399                 (*(uint64_t *)addr) = (uint64_t)val;
 400                 break;
 401         }
 402 #endif
 403
 404         if (DBG_ENABLED()) {
 405                 model_print("STORE *%p=%lu ", addr, val);
 406                 currexecpoint->print();
 407                 model_print("\n");
 408         }
 409         EPRecord * record=getOrCreateCurrRecord(STORE, NULL, id_addr_offset, 1, len, false);
 410         recordStoreChange(record, addr, val);
 411         addStoreTable(addr, record);
 412         EPValue * epvalue=getEPValue(record, NULL, addr, val, len);
 413 #ifdef TSO
 414         uint tid=id_to_int(currexecpoint->get_tid());
 415         (*storebuffer)[tid]->push_back(epvalue);
 416 #endif
 417         MCID mcids[]={id_value};
 418         recordContext(epvalue, MCID_NODEP, id_addr, 1, mcids);
 419         MCID stmcid=getNextMCID();
 420         ASSERT(stmcid==EPList->size());
 421         EPList->push_back(epvalue);
 422         memtable->put(addr, stmcid);
 423         currexecpoint->incrementTop();
 424 }
 425
 426 void MCExecution::recordFunctionChange(EPRecord *function, uint64_t val) {
 427         if (function->getSet(VC_FUNCOUTINDEX)->add(val))
 428                 planner->addChange(new MCChange(function, val, VC_FUNCOUTINDEX));
 429 }
 430
 431 void MCExecution::recordRMWChange(EPRecord *rmw, const void *addr, uint64_t valarg, uint64_t oldval, uint64_t newval) {
 432         if (!rmw->hasAddr(addr)) {
 433                 rmw->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
 434                 planner->addChange(new MCChange(rmw, (uint64_t)addr, VC_ADDRINDEX));
 435         }
 436         rmw->getSet(VC_BASEINDEX)->add(valarg);
 437         if (rmw->getOp()==CAS)
 438                 rmw->getSet(VC_OLDVALCASINDEX)->add(oldval);
 439         if (!rmw->getSet(VC_RMWOUTINDEX)->contains(newval)) {
 440                 rmw->getSet(VC_RMWOUTINDEX)->add(newval);
 441                 planner->addChange(new MCChange(rmw, newval, VC_RMWOUTINDEX));
 442         }
 443 }
 444
 445 void MCExecution::recordLoadChange(EPRecord *load, const void *addr) {
 446         if (!load->hasAddr(addr)) {
 447                 load->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
 448                 planner->addChange(new MCChange(load, (uint64_t)addr, VC_ADDRINDEX));
 449         }
 450 }
 451
 452 void MCExecution::recordStoreChange(EPRecord *store, const void *addr, uint64_t val) {
 453         if (!store->hasAddr(addr)) {
 454                 store->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
 455                 planner->addChange(new MCChange(store, (uint64_t)addr, VC_ADDRINDEX));
 456         }
 457         if (!store->hasValue(val)) {
 458                 store->getSet(VC_BASEINDEX)->add(val);
 459                 planner->addChange(new MCChange(store, val, VC_BASEINDEX));
 460         }
 461 }
 462
 463 /** @brief Processes a load. */
 464
 465 uint64_t MCExecution::load(const void *addr, int len) {
 466 #ifdef TSO
 467         uint64_t val=0;
 468         bool found=false;
 469         uint tid=id_to_int(currexecpoint->get_tid());
 470         SnapList<EPValue *> *list=(*storebuffer)[tid];
 471         for(SnapList<EPValue *>::reverse_iterator it=list->rbegin(); it != list->rend(); it++) {
 472                 EPValue *epval=*it;
 473                 const void *epaddr=epval->getAddr();
 474                 if (epaddr == addr) {
 475                         val = epval->getValue();
 476                         found = true;
 477                         break;
 478                 }
 479         }
 480         if (!found) {
 481                 switch(len) {
 482                 case 1:
 483                         val=*(uint8_t *) addr;
 484                         break;
 485                 case 2:
 486                         val=*(uint16_t *) addr;
 487                         break;
 488                 case 4:
 489                         val=*(uint32_t *) addr;
 490                         break;
 491                 case 8:
 492                         val=*(uint64_t *) addr;
 493                         break;
 494                 }
 495         }
 496 #else
 497         uint64_t val=0;
 498         switch(len) {
 499         case 1:
 500                 val=*(uint8_t *) addr;
 501                 break;
 502         case 2:
 503                 val=*(uint16_t *) addr;
 504                 break;
 505         case 4:
 506                 val=*(uint32_t *) addr;
 507                 break;
 508         case 8:
 509                 val=*(uint64_t *) addr;
 510                 break;
 511         }
 512 #endif
 513
 514         if (DBG_ENABLED()) {
 515                 model_print("%lu(mid=%u)=LOAD %p ", val, id_retval, addr);
 516                 currexecpoint->print();
 517                 model_print("\n");
 518         }
 519         ASSERT(id_addr==MCID_NODEP || (getEPValue(id_addr)->getValue()+id_addr_offset)==((uint64_t)addr));
 520         EPRecord * record=getOrCreateCurrRecord(LOAD, NULL, id_addr_offset, 0, len, false);
 521         recordLoadChange(record, addr);
 522         addLoadTable(addr, record);
 523         EPValue * epvalue=getEPValue(record, NULL, addr, val, len);
 524         MCID vcrf=memtable->get(addr);
 525         recordContext(epvalue, vcrf, id_addr, 0, NULL);
 526         ASSERT(EPList->size()==id_retval);
 527         EPList->push_back(epvalue);
 528         currexecpoint->incrementTop();
 529         return val;
 530 }
 531
 532 /** @brief Processes a branch. */
 533
 534 MCID MCExecution::branchDir(MCID dirid, int direction, int numdirs, bool anyvalue) {
 535         if (DBG_ENABLED()) {
 536                 model_print("BRANCH dir=%u mid=%u", direction, dirid);
 537                 currexecpoint->print();
 538                 model_print("\n");
 539         }
 540         EPRecord * record=getOrCreateCurrRecord(BRANCHDIR, NULL, 0, 1, numdirs, anyvalue);
 541         bool isNew;
 542         EPValue * epvalue=getEPValue(record, &isNew, NULL, direction, 32);
 543         if (isNew) {
 544 #ifdef PRINT_ACHIEVED_GOALS
 545                 model_print("Achieved Goal: BRANCH dir=%u mid=%u", direction, dirid);
 546                 currexecpoint->print();model_print("\n");
 547 #endif
 548 #ifdef STATS
 549                 planner->getConstGen()->curr_stat->bgoals++;
 550 #endif
 551                 planner->getConstGen()->achievedGoal(record);
 552                 scheduler->setNewFlag();
 553         }
 554         //record that we took a branch
 555         currbranch=epvalue;
 556         currbranch->lastrecord=NULL;
 557         MCID mcids[]={dirid};
 558         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
 559         MCID brmcid=getNextMCID();
 560         ASSERT(EPList->size()==brmcid);
 561         EPList->push_back(epvalue);
 562         //push the direction of the branch
 563         currexecpoint->push(EP_BRANCH,direction);
 564         //push the statement counter for the branch
 565         currexecpoint->push(EP_COUNTER,0);
 566
 567         return brmcid;
 568 }
 569
 570 /** @brief Processes a merge with a previous branch.  mcid gives the
 571                 branch we merged. */
 572
 573 void MCExecution::merge(MCID mcid) {
 574         EPValue * epvalue=getEPValue(mcid);
 575         ExecPoint *ep=epvalue->getEP();
 576         //rollback current branch
 577         currbranch=EPTable->get(ep)->getBranch();
 578         int orig_length=ep->getSize();
 579         int curr_length=currexecpoint->getSize();
 580         for(int i=0;i<curr_length-orig_length;i++)
 581                 currexecpoint->pop();
 582         //increment top
 583         currexecpoint->incrementTop();
 584         //now we can create the merge point
 585         if (DBG_ENABLED()) {
 586                 model_print("MERGE mid=%u", mcid);
 587                 currexecpoint->print();
 588                 model_print("\n");
 589         }
 590         getOrCreateCurrRecord(MERGE, NULL, 0, 0, 8, false);
 591         currexecpoint->incrementTop();
 592 }
 593
 594 /** @brief Phi function. */
 595 MCID MCExecution::phi(MCID input) {
 596         EPRecord * record=getOrCreateCurrRecord(FUNCTION, NULL, 0, 1, 8, false);
 597         record->setPhi();
 598         EPValue *epinput=getEPValue(input);
 599         EPValue * epvalue=getEPValue(record, NULL, NULL, epinput->getValue(), 8);
 600
 601         MCID mcids[]={input};
 602         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
 603
 604         MCID fnmcid=getNextMCID();
 605         ASSERT(EPList->size()==fnmcid);
 606         EPList->push_back(epvalue);
 607         currexecpoint->incrementTop();
 608
 609         return fnmcid;
 610 }
 611
 612 /** @brief Phi function for loops. */
 613 MCID MCExecution::loop_phi(MCID input) {
 614         EPRecord * record=getOrCreateCurrRecord(FUNCTION, NULL, 0, 1, 8, false);
 615         record->setLoopPhi();
 616         EPValue *epinput=getEPValue(input);
 617         EPValue * epvalue=getEPValue(record, NULL, NULL, epinput->getValue(), 8);
 618
 619         MCID mcids[]={input};
 620         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
 621
 622         uint tid=id_to_int(currexecpoint->get_tid());
 623         EPRecord *exitrec=(*lastloopexit)[tid];
 624
 625         EPRecordIDSet *phiset=record->getPhiLoopTable();
 626         struct RecordIDPair rip={exitrec,getEPRecord(input)};
 627         if (!phiset->contains(&rip)) {
 628                 struct RecordIDPair *p=(struct RecordIDPair *)model_malloc(sizeof(struct RecordIDPair));
 629                 *p=rip;
 630                 phiset->add(p);
 631         }
 632
 633         MCID fnmcid=getNextMCID();
 634         ASSERT(EPList->size()==fnmcid);
 635         EPList->push_back(epvalue);
 636         currexecpoint->incrementTop();
 637
 638         return fnmcid;
 639 }
 640
 641 uint64_t MCExecution::equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, MCID *retval) {
 642         uint64_t eq=(val1==val2);
 643         bool isNew=false;
 644         int len=8;
 645         EPRecord * record=getOrCreateCurrRecord(EQUALS, &isNew, 0, 2, len, false);
 646         EPValue * epvalue=getEPValue(record, NULL, NULL, eq, len);
 647         getEPValue(record, NULL, NULL, 1-eq, len);
 648         MCID mcids[]={op1, op2};
 649         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 2, mcids);
 650         if (isNew) {
 651                 recordFunctionChange(record, 0);
 652                 recordFunctionChange(record, 1);
 653         }
 654         MCID eqmcid=getNextMCID();
 655         ASSERT(EPList->size()==eqmcid);
 656         EPList->push_back(epvalue);
 657         currexecpoint->incrementTop();
 658         *retval=eqmcid;
 659         return eq;
 660 }
 661
 662 /** @brief Processes an uninterpretted function. */
 663
 664 MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint numids, MCID *mcids) {
 665         bool isNew=false;
 666         EPRecord * record=getOrCreateCurrRecord(FUNCTION, &isNew, 0, numids, len, false);
 667         if (isNew) {
 668                 if (functionidentifier == 0)
 669                         record->setCompletedGoal(new CGoalSet(), false);
 670                 else {
 671                         if (sharedgoals->size()<=functionidentifier) {
 672                                 sharedgoals->resize(functionidentifier+1);
 673                                 sharedfuncrecords->resize(functionidentifier+1);
 674                         }
 675                         if ((*sharedgoals)[functionidentifier]==NULL) {
 676                                 (*sharedgoals)[functionidentifier]=new CGoalSet();
 677                                 (*sharedfuncrecords)[functionidentifier]=new RecordSet();
 678                         }
 679                         record->setCompletedGoal((*sharedgoals)[functionidentifier], true);
 680                         (*sharedfuncrecords)[functionidentifier]->add(record);
 681
 682                         for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
 683                                 EPRecord *input=getEPRecord(mcids[i-VC_BASEINDEX]);
 684                                 IntIterator *inputit=input->getReturnValueSet()->iterator();
 685                                 IntHashSet *recinputset=record->getSet(i);
 686                                 while(inputit->hasNext()) {
 687                                         uint64_t inputval=inputit->next();
 688                                         recinputset->add(inputval);
 689                                 }
 690                                 delete inputit;
 691                         }
 692
 693                         CGoalIterator *cit=(*sharedgoals)[functionidentifier]->iterator();
 694                         while(cit->hasNext()) {
 695                                 CGoal *goal=cit->next();
 696                                 evalGoal(record, goal);
 697                         }
 698                         delete cit;
 699                 }
 700         }
 701         val=val&getmask(len);
 702         EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
 703         recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
 704
 705         uint64_t valarray[numids+VC_BASEINDEX];
 706         for(uint i=0;i<VC_BASEINDEX;i++) {
 707                 valarray[i]=0;
 708         }
 709         for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
 710                 valarray[i]=getEPValue(mcids[i-VC_BASEINDEX])->getValue();
 711         }
 712
 713         MCID fnmcid=getNextMCID();
 714         ASSERT(EPList->size()==fnmcid);
 715         EPList->push_back(epvalue);
 716         currexecpoint->incrementTop();
 717
 718         CGoal *goal=new CGoal(numids+VC_BASEINDEX, valarray);
 719         if (record->completedGoalSet()->contains(goal)) {
 720                 delete goal;
 721         } else {
 722                 scheduler->setNewFlag();
 723                 planner->getConstGen()->achievedGoal(record);
 724 #ifdef PRINT_ACHIEVED_GOALS
 725                 model_print("Achieved goal:");goal->print();model_print("\n");
 726 #endif
 727 #ifdef STATS
 728                 planner->getConstGen()->curr_stat->fgoals++;
 729 #endif
 730                 goal->setOutput(val);
 731                 record->completedGoalSet()->add(goal);
 732                 recordFunctionChange(record, val);
 733                 if (functionidentifier != 0) {
 734                         RecordIterator *rit=(*sharedfuncrecords)[functionidentifier]->iterator();
 735                         while(rit->hasNext()) {
 736                                 EPRecord *func=rit->next();
 737                                 if (func == record)
 738                                         continue;
 739                                 evalGoal(func, goal);
 740                         }
 741                         delete rit;
 742                 }
 743         }
 744
 745         return fnmcid;
 746 }
 747
 748 void MCExecution::evalGoal(EPRecord *record, CGoal *goal) {
 749         for(uint i=VC_BASEINDEX;i<goal->getNum();i++) {
 750                 uint64_t input=goal->getValue(i);
 751                 if (!record->getSet(i)->contains(input))
 752                         return;
 753         }
 754         //Have all input, propagate output
 755         recordFunctionChange(record, goal->getOutput());
 756 }
 757
 758 /** @brief Returns the next thread id. */
 759
 760 thread_id_t MCExecution::get_next_tid() {
 761         return int_to_id(snap_fields->next_thread_id++);
 762 }
 763
 764 /** @brief Registers a new thread */
 765
 766 void MCExecution::add_thread(Thread *t) {
 767         ThreadList->push_back(t);
 768         ExecPoint * ep=new ExecPoint(4, t->get_id());
 769         ep->push(EP_COUNTER,0);
 770         ExecPointList->push_back(ep);
 771         CurrBranchList->push_back(NULL);
 772 #ifdef TSO
 773         storebuffer->push_back(new SnapList<EPValue *>());
 774 #endif
 775 }
 776
 777 /** @brief Records currently executing thread. */
 778
 779 void MCExecution::set_current_thread(Thread *t) {
 780         if (curr_thread) {
 781                 uint oldtid=id_to_int(curr_thread->get_id());
 782                 (*CurrBranchList)[oldtid]=currbranch;
 783         }
 784         curr_thread=t;
 785         currexecpoint=(t==NULL)?NULL:(*ExecPointList)[id_to_int(t->get_id())];
 786         currbranch=(t==NULL)?NULL:(*CurrBranchList)[id_to_int(t->get_id())];
 787 }
 788
 789 void MCExecution::threadStart(EPRecord *parent) {
 790         EPRecord *threadstart=getOrCreateCurrRecord(THREADBEGIN, NULL, 0, 0, 8, false);
 791         if (parent!=NULL) {
 792                 parent->setChildRecord(threadstart);
 793         }
 794         currexecpoint->incrementTop();
 795 }
 796
 797 /** @brief Create a new thread. */
 798
 799 void MCExecution::threadCreate(thrd_t *t, thrd_start_t start, void *arg) {
 800         EPRecord *threadstart=getOrCreateCurrRecord(THREADCREATE, NULL, 0, 0, 8, false);
 801         currexecpoint->incrementTop();
 802         Thread *th = new Thread(get_next_tid(), t, start, arg, curr_thread, threadstart);
 803         add_thread(th);
 804 }
 805
 806 /** @brief Joins with a thread. */
 807
 808 void MCExecution::threadJoin(Thread *blocking) {
 809         while(true) {
 810                 if (blocking->is_complete()) {
 811                         EPRecord *join=getOrCreateCurrRecord(THREADJOIN, NULL, 0, 0, 8, false);
 812                         currexecpoint->incrementTop();
 813                         join->setJoinThread(blocking->get_id());
 814                         return;
 815                 }
 816                 get_current_thread()->set_waiting(blocking);
 817                 scheduler->check_preempt();
 818                 get_current_thread()->set_waiting(NULL);
 819         }
 820 }
 821
 822 /** @brief Finishes a thread. */
 823
 824 void MCExecution::threadFinish() {
 825         Thread *th = get_current_thread();
 826         /* Wake up any joining threads */
 827         for (unsigned int i = 0; i < get_num_threads(); i++) {
 828                 Thread *waiting = get_thread(int_to_id(i));
 829                 if (waiting->waiting_on() == th) {
 830                         waiting->set_waiting(NULL);
 831                 }
 832         }
 833         th->complete();
 834         scheduler->check_preempt();
 835 }
 836
 837 /** @brief Thread yield. */
 838
 839 void MCExecution::threadYield() {
 840         getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
 841         currexecpoint->incrementTop();
 842 }
 843
 844 /** @brief Thread yield. */
 845
 846 void * MCExecution::alloc(size_t size) {
 847         bool isNew;
 848         EPRecord *record=getOrCreateCurrRecord(ALLOC, &isNew, 0, 0, 8, false);
 849         currexecpoint->incrementTop();
 850         if (isNew) {
 851                 size_t allocsize=((size<<1)+7)&~((size_t)(7));
 852                 record->setSize(allocsize);
 853                 void *ptr=real_user_malloc(size);
 854                 record->setPtr(ptr);
 855                 return ptr;
 856         } else {
 857                 if (size>record->getSize()) {
 858                         model_print("Allocation size changed too much\n");
 859                         exit(-1);
 860                 }
 861                 void *ptr=record->getPtr();
 862                 return ptr;
 863         }
 864 }
 865
 866 /** @brief Record enter loop. */
 867
 868 void MCExecution::enterLoop() {
 869         EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
 870
 871         //push the loop iteration counter
 872         currexecpoint->push(EP_LOOP,0);
 873         //push the curr iteration statement counter
 874         currexecpoint->push(EP_COUNTER,0);
 875         EPRecord * lpstartrecord=getOrCreateCurrRecord(LOOPSTART, NULL, 0, 0, 8, false);
 876         record->setChildRecord(lpstartrecord);
 877
 878         currexecpoint->incrementTop();
 879         if (DBG_ENABLED()) {
 880                 model_print("ENLOOP ");
 881                 currexecpoint->print();
 882                 model_print("\n");
 883         }
 884 }
 885
 886 /** @brief Record exit loop. */
 887
 888 void MCExecution::exitLoop() {
 889         ExecPointType type;
 890         EPRecord *breakstate=NULL;
 891
 892         /* Record last statement */
 893         uint tid=id_to_int(currexecpoint->get_tid());
 894
 895         if (!currexecpoint->directInLoop()) {
 896                 breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
 897                 currexecpoint->incrementTop();
 898         }
 899
 900         /* Get Last Record */
 901         EPRecord *lastrecord=(currbranch==NULL)?(*alwaysexecuted)[tid]:currbranch->lastrecord;
 902
 903         /* Remember last record as loop exit for this execution.  */
 904         if (lastloopexit->size()<=tid) {
 905                 lastloopexit->resize(tid+1);
 906         }
 907         (*lastloopexit)[tid]=lastrecord;
 908
 909         do {
 910                 type=currexecpoint->getType();
 911                 currexecpoint->pop();
 912                 if (type==EP_BRANCH) {
 913                         //we crossed a branch, fix currbranch
 914                         EPRecord *branch=currbranch->getRecord();
 915                         currbranch=branch->getBranch();
 916                 }
 917         } while(type!=EP_LOOP);
 918
 919         if (DBG_ENABLED()) {
 920                 model_print("EXLOOP ");
 921                 currexecpoint->print();
 922                 model_print("\n");
 923         }
 924         EPRecord *loopenter=EPTable->get(currexecpoint);
 925         currexecpoint->incrementTop();
 926         EPRecord *labelrec=getOrCreateCurrRecord(LABEL, NULL, 0, 0, 8, false);
 927         if (loopenter->getNextRecord()==NULL) {
 928                 loopenter->setNextRecord(labelrec);
 929         }
 930         if (breakstate!=NULL) {
 931                 breakstate->setNextRecord(labelrec);
 932         }
 933         currexecpoint->incrementTop();
 934 }
 935
 936 /** @brief Record next loop iteration. */
 937 void MCExecution::loopIterate() {
 938         currexecpoint->pop();
 939         //increment the iteration counter
 940         currexecpoint->incrementTop();
 941         currexecpoint->push(EP_COUNTER,0);
 942 }
 943
 944 /** @brief Helper function to add new item to a StoreLoadHashTable */
 945
 946 void addTable(StoreLoadHashTable *table, const void *addr, EPRecord *record) {
 947         RecordSet * rset=table->get(addr);
 948         if (rset==NULL) {
 949                 rset=new RecordSet();
 950                 table->put(addr, rset);
 951         }
 952         rset->add(record);
 953 }
 954
 955 /** @brief Update mapping from address to stores to that address. */
 956
 957 void MCExecution::addStoreTable(const void *addr, EPRecord *record) {
 958         addTable(storetable, addr, record);
 959 }
 960
 961 /** @brief Update mapping from address to loads from that address. */
 962
 963 void MCExecution::addLoadTable(const void *addr, EPRecord *record) {
 964         addTable(loadtable, addr, record);
 965 }
 966
 967 /** @brief Update mapping from address to loads from that address. */
 968
 969 RecordSet * MCExecution::getLoadTable(const void *addr) {
 970         return loadtable->get(addr);
 971 }
 972
 973 /** @brief Update mapping from address to stores to that address. */
 974
 975 RecordSet * MCExecution::getStoreTable(const void *addr) {
 976         return storetable->get(addr);
 977 }
 978
 979 /** @brief Registers that component index of deprecord depends on record. */
 980
 981 void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsigned int index) {
 982         EPRecordSet *set=eprecorddep->get(record);
 983         if (set==NULL) {
 984                 set=new EPRecordSet();
 985                 eprecorddep->put(record, set);
 986         }
 987         struct RecordIntPair pair={deprecord, index};
 988
 989         if (!set->contains(&pair)) {
 990                 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
 991                 *p=pair;
 992                 set->add(p);
 993         }
 994
 995         if (!revrecorddep->contains(&pair)) {
 996                 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
 997                 *p=pair;
 998                 revrecorddep->put(p, new ModelVector<EPRecord *>());
 999         }
1000
1001         ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
1002         for(uint i=0;i<recvec->size();i++) {
1003                 if ((*recvec)[i]==record)
1004                         return;
1005         }
1006         recvec->push_back(record);
1007 }
1008
1009 ModelVector<EPRecord *> * MCExecution::getRevDependences(EPRecord *record, uint index) {
1010         struct RecordIntPair pair={record, index};
1011         return revrecorddep->get(&pair);
1012 }