X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satcheck.git;a=blobdiff_plain;f=mcexecution.cc;h=59ea44aeb34d6b091b004c8e9f55385c67862bbf;hp=1166731c1b6758a88f3c0e5b680dbb147e6d32ed;hb=dda2d5d103b32f8505374712936af1daf42ec061;hpb=44e8eabc8f7a0ab23c29037a770463d8a2de7b4a diff --git a/mcexecution.cc b/mcexecution.cc index 1166731..59ea44a 100644 --- a/mcexecution.cc +++ b/mcexecution.cc @@ -55,7 +55,7 @@ MCExecution::MCExecution() : currid(MCID_INIT), schedule_graph(0) { - EPList->push_back(NULL);//avoid using MCID of 0 + EPList->push_back(NULL); //avoid using MCID of 0 #ifdef TSO storebuffer = new SnapVector *>(); #endif @@ -111,21 +111,21 @@ void MCExecution::dumpExecution() { sprintf(buffer, "exec%u.dot",schedule_graph); schedule_graph++; int file=open(buffer,O_WRONLY|O_TRUNC|O_CREAT, S_IRWXU); - dprintf(file, "digraph execution {\n"); + model_dprintf(file, "digraph execution {\n"); EPRecord *last=NULL; for(uint i=0;isize();i++) { EPValue *epv=(*EPList)[i]; if (epv==NULL) continue; EPRecord *record=epv->getRecord(); - dprintf(file, "%lu[label=\"",(uintptr_t)record); + model_dprintf(file, "%lu[label=\"",(uintptr_t)record); record->print(file); - dprintf(file, "\"];\n"); + model_dprintf(file, "\"];\n"); if (last!=NULL) - dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record); + model_dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record); last=record; } - dprintf(file, "}\n"); + model_dprintf(file, "}\n"); close(file); } @@ -212,12 +212,12 @@ uint64_t MCExecution::rmw(enum atomicop op, void *addr, uint len, uint64_t currv uint64_t newval; uint64_t retval=dormwaction(op, addr, len, currval, oldval, valarg, &newval); if (DBG_ENABLED()) { - model_print("RMW %p oldval=%lu valarg=%lu retval=%lu", addr, oldval, valarg, retval); + model_print("RMW %p oldval=%llu valarg=%llu retval=%llu", addr, oldval, valarg, retval); currexecpoint->print(); model_print("\n"); } - int num_mcids=(op==ADD)?1:2; + int num_mcids=(op==ADD) ? 1 : 2; EPRecord * record=getOrCreateCurrRecord(RMW, NULL, id_addr_offset, VC_RMWOUTINDEX-VC_RFINDEX, len, false); record->setRMW(op); @@ -307,11 +307,14 @@ bool MCExecution::isEmptyStoreBuffer(thread_id_t tid) { SnapList * list=(*storebuffer)[id_to_int(tid)]; return list->empty(); } - + void MCExecution::doStore(thread_id_t tid) { SnapList * list=(*storebuffer)[id_to_int(tid)]; EPValue * epval=list->front(); list->pop_front(); + if (DBG_ENABLED()) { + model_print("tid = %d: ", tid); + } doStore(epval); } @@ -320,10 +323,10 @@ void MCExecution::doStore(EPValue *epval) { uint64_t val=epval->getValue(); int len=epval->getLen(); if (DBG_ENABLED()) { - model_print("flushing %d bytes *(%p) = %lu", len, addr, val); + model_print("flushing %d bytes *(%p) = %llu", len, addr, val); currexecpoint->print(); model_print("\n"); - } + } switch(len) { case 1: (*(uint8_t *)addr) = (uint8_t)val; @@ -355,11 +358,11 @@ void MCExecution::fence() { #endif /** @brief EPValue is the corresponding epvalue object. - For loads rf is the store we read from. - For loads or stores, addr is the MCID for the provided address. - numids is the number of MCID's we take in. - We then list that number of MCIDs for everything we depend on. -*/ + For loads rf is the store we read from. + For loads or stores, addr is the MCID for the provided address. + numids is the number of MCID's we take in. + We then list that number of MCIDs for everything we depend on. + */ void MCExecution::recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids) { EPRecord *currrecord=epv->getRecord(); @@ -400,9 +403,9 @@ void MCExecution::store(void *addr, uint64_t val, int len) { break; } #endif - + if (DBG_ENABLED()) { - model_print("STORE *%p=%lu ", addr, val); + model_print("STORE *%p=%llu ", addr, val); currexecpoint->print(); model_print("\n"); } @@ -468,7 +471,7 @@ uint64_t MCExecution::load(const void *addr, int len) { bool found=false; uint tid=id_to_int(currexecpoint->get_tid()); SnapList *list=(*storebuffer)[tid]; - for(SnapList::reverse_iterator it=list->rbegin(); it != list->rend(); it++) { + for(SnapList::reverse_iterator it=list->rbegin();it != list->rend();it++) { EPValue *epval=*it; const void *epaddr=epval->getAddr(); if (epaddr == addr) { @@ -510,9 +513,9 @@ uint64_t MCExecution::load(const void *addr, int len) { break; } #endif - + if (DBG_ENABLED()) { - model_print("%lu(mid=%u)=LOAD %p ", val, id_retval, addr); + model_print("%llu(mid=%u)=LOAD %p ", val, id_retval, addr); currexecpoint->print(); model_print("\n"); } @@ -568,7 +571,7 @@ MCID MCExecution::branchDir(MCID dirid, int direction, int numdirs, bool anyvalu } /** @brief Processes a merge with a previous branch. mcid gives the - branch we merged. */ + branch we merged. */ void MCExecution::merge(MCID mcid) { EPValue * epvalue=getEPValue(mcid); @@ -580,7 +583,7 @@ void MCExecution::merge(MCID mcid) { for(int i=0;ipop(); //increment top - currexecpoint->incrementTop(); + currexecpoint->incrementTop(); //now we can create the merge point if (DBG_ENABLED()) { model_print("MERGE mid=%u", mcid); @@ -600,7 +603,7 @@ MCID MCExecution::phi(MCID input) { MCID mcids[]={input}; recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids); - + MCID fnmcid=getNextMCID(); ASSERT(EPList->size()==fnmcid); EPList->push_back(epvalue); @@ -629,7 +632,7 @@ MCID MCExecution::loop_phi(MCID input) { *p=rip; phiset->add(p); } - + MCID fnmcid=getNextMCID(); ASSERT(EPList->size()==fnmcid); EPList->push_back(epvalue); @@ -701,7 +704,7 @@ MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint val=val&getmask(len); EPValue * epvalue=getEPValue(record, NULL, NULL, val, len); recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids); - + uint64_t valarray[numids+VC_BASEINDEX]; for(uint i=0;iget_id())]; - currbranch=(t==NULL)?NULL:(*CurrBranchList)[id_to_int(t->get_id())]; + currexecpoint=(t==NULL) ? NULL : (*ExecPointList)[id_to_int(t->get_id())]; + currbranch=(t==NULL) ? NULL : (*CurrBranchList)[id_to_int(t->get_id())]; } void MCExecution::threadStart(EPRecord *parent) { @@ -824,7 +827,7 @@ void MCExecution::threadJoin(Thread *blocking) { void MCExecution::threadFinish() { Thread *th = get_current_thread(); /* Wake up any joining threads */ - for (unsigned int i = 0; i < get_num_threads(); i++) { + for (unsigned int i = 0;i < get_num_threads();i++) { Thread *waiting = get_thread(int_to_id(i)); if (waiting->waiting_on() == th) { waiting->set_waiting(NULL); @@ -867,14 +870,14 @@ void * MCExecution::alloc(size_t size) { void MCExecution::enterLoop() { EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false); - + //push the loop iteration counter currexecpoint->push(EP_LOOP,0); //push the curr iteration statement counter currexecpoint->push(EP_COUNTER,0); EPRecord * lpstartrecord=getOrCreateCurrRecord(LOOPSTART, NULL, 0, 0, 8, false); record->setChildRecord(lpstartrecord); - + currexecpoint->incrementTop(); if (DBG_ENABLED()) { model_print("ENLOOP "); @@ -891,15 +894,18 @@ void MCExecution::exitLoop() { /* Record last statement */ uint tid=id_to_int(currexecpoint->get_tid()); - + if (!currexecpoint->directInLoop()) { breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false); currexecpoint->incrementTop(); + } else { + breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false); + currexecpoint->incrementTop(); } - + /* Get Last Record */ - EPRecord *lastrecord=(currbranch==NULL)?(*alwaysexecuted)[tid]:currbranch->lastrecord; - + EPRecord *lastrecord=(currbranch==NULL) ? (*alwaysexecuted)[tid] : currbranch->lastrecord; + /* Remember last record as loop exit for this execution. */ if (lastloopexit->size()<=tid) { lastloopexit->resize(tid+1); @@ -927,9 +933,7 @@ void MCExecution::exitLoop() { if (loopenter->getNextRecord()==NULL) { loopenter->setNextRecord(labelrec); } - if (breakstate!=NULL) { - breakstate->setNextRecord(labelrec); - } + breakstate->setNextRecord(labelrec); currexecpoint->incrementTop(); } @@ -987,17 +991,17 @@ void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsig struct RecordIntPair pair={deprecord, index}; if (!set->contains(&pair)) { - struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair)); + struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair)); *p=pair; set->add(p); } if (!revrecorddep->contains(&pair)) { - struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair)); + struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair)); *p=pair; revrecorddep->put(p, new ModelVector()); } - + ModelVector * recvec=revrecorddep->get(&pair); for(uint i=0;isize();i++) { if ((*recvec)[i]==record)