1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
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.
10 #include "mcexecution.h"
11 #include "mcschedule.h"
23 MCExecution_snapshot::MCExecution_snapshot() :
28 MCExecution_snapshot::~MCExecution_snapshot() {
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 *>()),
43 scheduler(new MCScheduler(this)),
44 planner(new Planner(this)),
45 snap_fields(new MCExecution_snapshot()),
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 *>()),
58 EPList->push_back(NULL); //avoid using MCID of 0
60 storebuffer = new SnapVector<SnapList<EPValue *> *>();
64 MCExecution::~MCExecution() {
77 delete alwaysexecuted;
80 for(uint i=0;i<storebuffer->size();i++) {
81 SnapList<EPValue *> *list=(*storebuffer)[i];
87 for(uint i=0;i<sharedgoals->size();i++) {
88 CGoalSet *c=(*sharedgoals)[i];
93 for(uint i=0;i<sharedfuncrecords->size();i++) {
94 RecordSet *rs=(*sharedfuncrecords)[i];
98 delete sharedfuncrecords;
101 /** @brief Resets MCExecution object for next execution. */
103 void MCExecution::reset() {
106 alwaysexecuted->clear();
109 void MCExecution::dumpExecution() {
111 sprintf(buffer, "exec%u.dot",schedule_graph);
113 int file=open(buffer,O_WRONLY|O_TRUNC|O_CREAT, S_IRWXU);
114 model_dprintf(file, "digraph execution {\n");
116 for(uint i=0;i<EPList->size();i++) {
117 EPValue *epv=(*EPList)[i];
120 EPRecord *record=epv->getRecord();
121 model_dprintf(file, "%lu[label=\"",(uintptr_t)record);
123 model_dprintf(file, "\"];\n");
125 model_dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record);
128 model_dprintf(file, "}\n");
132 /** @brief Records the MCID and returns the next MCID */
134 MCID MCExecution::loadMCID(MCID maddr, uintptr_t offset) {
135 scheduler->check_preempt();
137 id_addr_offset=offset;
138 return id_retval=getNextMCID();
141 /** @brief Records the address and value MCIDs. */
143 void MCExecution::storeMCID(MCID maddr, uintptr_t offset, MCID val) {
145 scheduler->check_preempt();
148 id_addr_offset=offset;
152 /** @brief Records MCIDs for a RMW. */
154 MCID MCExecution::nextRMW(MCID maddr, uintptr_t offset, MCID oldval, MCID valarg) {
155 scheduler->check_preempt();
157 id_addr_offset=offset;
160 id_retval=getNextMCID();
164 uint64_t dormwaction(enum atomicop op, void *addr, uint len, uint64_t currval, uint64_t oldval, uint64_t valarg, uint64_t *newval) {
170 memval=currval+valarg;
174 if (currval==oldval) {
189 *newval=memval&getmask(len);
191 if (op==ADD || (op==CAS && (currval==oldval)) || (op == EXC)) {
194 *((uint8_t *)addr)=*newval;
197 *((uint16_t *)addr)=*newval;
200 *((uint32_t *)addr)=*newval;
203 *((uint64_t *)addr)=*newval;
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) {
213 uint64_t retval=dormwaction(op, addr, len, currval, oldval, valarg, &newval);
215 model_print("RMW %p oldval=%llu valarg=%llu retval=%llu", addr, oldval, valarg, retval);
216 currexecpoint->print();
220 int num_mcids=(op==ADD) ? 1 : 2;
221 EPRecord * record=getOrCreateCurrRecord(RMW, NULL, id_addr_offset, VC_RMWOUTINDEX-VC_RFINDEX, len, false);
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();
238 /** @brief Gets an EPRecord for the current execution point. */
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);
243 *isNew=(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);
250 EPTable->put(ep, record);
252 ASSERT(record->getOffset()==offset);
254 if (currbranch==NULL) {
255 uint tid=id_to_int(currexecpoint->get_tid());
256 if (alwaysexecuted->size()<=tid) {
257 alwaysexecuted->resize(tid+1);
259 if ((*alwaysexecuted)[tid]!=NULL && et != LABEL && et != LOOPSTART)
260 (*alwaysexecuted)[tid]->setNextRecord(record);
261 (*alwaysexecuted)[tid]=record;
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;
273 /** @brief Gets an EPValue for the current record and value. */
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);
286 EPValueTable->put(epvalue, epvalue);
287 record->addEPValue(epvalue);
293 /** @brief Lookup EPRecord for the MCID. */
295 EPRecord * MCExecution::getEPRecord(MCID id) {
296 return (*EPList)[id]->getRecord();
299 /** @brief Lookup EPValue for the MCID. */
301 EPValue * MCExecution::getEPValue(MCID id) {
302 return (*EPList)[id];
306 bool MCExecution::isEmptyStoreBuffer(thread_id_t tid) {
307 SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
308 return list->empty();
311 void MCExecution::doStore(thread_id_t tid) {
312 SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
313 EPValue * epval=list->front();
316 model_print("tid = %d: ", tid);
321 void MCExecution::doStore(EPValue *epval) {
322 const void *addr=epval->getAddr();
323 uint64_t val=epval->getValue();
324 int len=epval->getLen();
326 model_print("flushing %d bytes *(%p) = %llu", len, addr, val);
327 currexecpoint->print();
332 (*(uint8_t *)addr) = (uint8_t)val;
335 (*(uint16_t *)addr) = (uint16_t)val;
338 (*(uint32_t *)addr) = (uint32_t)val;
341 (*(uint64_t *)addr) = (uint64_t)val;
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();
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.
367 void MCExecution::recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids) {
368 EPRecord *currrecord=epv->getRecord();
370 for(int i=0;i<numids;i++) {
372 if (id != MCID_NODEP) {
373 EPRecord * epi=getEPRecord(id);
374 addRecordDepTable(epi,currrecord, VC_BASEINDEX+i);
377 if (rf != MCID_NODEP) {
378 EPRecord *eprf=getEPRecord(rf);
379 addRecordDepTable(eprf,currrecord, VC_RFINDEX);
381 if (addr != MCID_NODEP) {
382 EPRecord *epaddr=getEPRecord(addr);
383 addRecordDepTable(epaddr,currrecord, VC_ADDRINDEX);
387 /** @brief Processes a store. */
389 void MCExecution::store(void *addr, uint64_t val, int len) {
393 (*(uint8_t *)addr) = (uint8_t)val;
396 (*(uint16_t *)addr) = (uint16_t)val;
399 (*(uint32_t *)addr) = (uint32_t)val;
402 (*(uint64_t *)addr) = (uint64_t)val;
408 model_print("STORE *%p=%llu ", addr, val);
409 currexecpoint->print();
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);
417 uint tid=id_to_int(currexecpoint->get_tid());
418 (*storebuffer)[tid]->push_back(epvalue);
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();
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));
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));
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));
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));
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));
460 if (!store->hasValue(val)) {
461 store->getSet(VC_BASEINDEX)->add(val);
462 planner->addChange(new MCChange(store, val, VC_BASEINDEX));
466 /** @brief Processes a load. */
468 uint64_t MCExecution::load(const void *addr, int len) {
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++) {
476 const void *epaddr=epval->getAddr();
477 if (epaddr == addr) {
478 val = epval->getValue();
486 val=*(uint8_t *) addr;
489 val=*(uint16_t *) addr;
492 val=*(uint32_t *) addr;
495 val=*(uint64_t *) addr;
503 val=*(uint8_t *) addr;
506 val=*(uint16_t *) addr;
509 val=*(uint32_t *) addr;
512 val=*(uint64_t *) addr;
518 model_print("%llu(mid=%u)=LOAD %p ", val, id_retval, addr);
519 currexecpoint->print();
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();
535 /** @brief Processes a branch. */
537 MCID MCExecution::branchDir(MCID dirid, int direction, int numdirs, bool anyvalue) {
539 model_print("BRANCH dir=%u mid=%u", direction, dirid);
540 currexecpoint->print();
543 EPRecord * record=getOrCreateCurrRecord(BRANCHDIR, NULL, 0, 1, numdirs, anyvalue);
545 EPValue * epvalue=getEPValue(record, &isNew, NULL, direction, 32);
547 #ifdef PRINT_ACHIEVED_GOALS
548 model_print("Achieved Goal: BRANCH dir=%u mid=%u", direction, dirid);
549 currexecpoint->print();model_print("\n");
552 planner->getConstGen()->curr_stat->bgoals++;
554 planner->getConstGen()->achievedGoal(record);
555 scheduler->setNewFlag();
557 //record that we took a branch
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);
573 /** @brief Processes a merge with a previous branch. mcid gives the
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();
586 currexecpoint->incrementTop();
587 //now we can create the merge point
589 model_print("MERGE mid=%u", mcid);
590 currexecpoint->print();
593 getOrCreateCurrRecord(MERGE, NULL, 0, 0, 8, false);
594 currexecpoint->incrementTop();
597 /** @brief Phi function. */
598 MCID MCExecution::phi(MCID input) {
599 EPRecord * record=getOrCreateCurrRecord(FUNCTION, NULL, 0, 1, 8, false);
601 EPValue *epinput=getEPValue(input);
602 EPValue * epvalue=getEPValue(record, NULL, NULL, epinput->getValue(), 8);
604 MCID mcids[]={input};
605 recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
607 MCID fnmcid=getNextMCID();
608 ASSERT(EPList->size()==fnmcid);
609 EPList->push_back(epvalue);
610 currexecpoint->incrementTop();
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);
622 MCID mcids[]={input};
623 recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
625 uint tid=id_to_int(currexecpoint->get_tid());
626 EPRecord *exitrec=(*lastloopexit)[tid];
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));
636 MCID fnmcid=getNextMCID();
637 ASSERT(EPList->size()==fnmcid);
638 EPList->push_back(epvalue);
639 currexecpoint->incrementTop();
644 uint64_t MCExecution::equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, MCID *retval) {
645 uint64_t eq=(val1==val2);
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);
654 recordFunctionChange(record, 0);
655 recordFunctionChange(record, 1);
658 if(op1 == MCID_NODEP) {
659 record->getSet(VC_BASEINDEX + 0)->add(val1);
662 if(op2 == MCID_NODEP) {
663 record->getSet(VC_BASEINDEX + 1)->add(val2);
666 MCID eqmcid=getNextMCID();
667 ASSERT(EPList->size()==eqmcid);
668 EPList->push_back(epvalue);
669 currexecpoint->incrementTop();
674 /** @brief Processes an uninterpretted function. */
676 MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint numids, MCID *mcids) {
678 EPRecord * record=getOrCreateCurrRecord(FUNCTION, &isNew, 0, numids, len, false);
680 if (functionidentifier == 0)
681 record->setCompletedGoal(new CGoalSet(), false);
683 if (sharedgoals->size()<=functionidentifier) {
684 sharedgoals->resize(functionidentifier+1);
685 sharedfuncrecords->resize(functionidentifier+1);
687 if ((*sharedgoals)[functionidentifier]==NULL) {
688 (*sharedgoals)[functionidentifier]=new CGoalSet();
689 (*sharedfuncrecords)[functionidentifier]=new RecordSet();
691 record->setCompletedGoal((*sharedgoals)[functionidentifier], true);
692 (*sharedfuncrecords)[functionidentifier]->add(record);
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);
705 CGoalIterator *cit=(*sharedgoals)[functionidentifier]->iterator();
706 while(cit->hasNext()) {
707 CGoal *goal=cit->next();
708 evalGoal(record, goal);
713 val=val&getmask(len);
714 EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
715 recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
717 uint64_t valarray[numids+VC_BASEINDEX];
718 for(uint i=0;i<VC_BASEINDEX;i++) {
721 for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
722 valarray[i]=getEPValue(mcids[i-VC_BASEINDEX])->getValue();
725 MCID fnmcid=getNextMCID();
726 ASSERT(EPList->size()==fnmcid);
727 EPList->push_back(epvalue);
728 currexecpoint->incrementTop();
730 CGoal *goal=new CGoal(numids+VC_BASEINDEX, valarray);
731 if (record->completedGoalSet()->contains(goal)) {
734 scheduler->setNewFlag();
735 planner->getConstGen()->achievedGoal(record);
736 #ifdef PRINT_ACHIEVED_GOALS
737 model_print("Achieved goal:");goal->print();model_print("\n");
740 planner->getConstGen()->curr_stat->fgoals++;
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();
751 evalGoal(func, goal);
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))
766 //Have all input, propagate output
767 recordFunctionChange(record, goal->getOutput());
770 /** @brief Returns the next thread id. */
772 thread_id_t MCExecution::get_next_tid() {
773 return int_to_id(snap_fields->next_thread_id++);
776 /** @brief Registers a new thread */
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);
785 storebuffer->push_back(new SnapList<EPValue *>());
789 /** @brief Records currently executing thread. */
791 void MCExecution::set_current_thread(Thread *t) {
793 uint oldtid=id_to_int(curr_thread->get_id());
794 (*CurrBranchList)[oldtid]=currbranch;
797 currexecpoint=(t==NULL) ? NULL : (*ExecPointList)[id_to_int(t->get_id())];
798 currbranch=(t==NULL) ? NULL : (*CurrBranchList)[id_to_int(t->get_id())];
801 void MCExecution::threadStart(EPRecord *parent) {
802 EPRecord *threadstart=getOrCreateCurrRecord(THREADBEGIN, NULL, 0, 0, 8, false);
804 parent->setChildRecord(threadstart);
806 currexecpoint->incrementTop();
809 /** @brief Create a new thread. */
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);
818 /** @brief Joins with a thread. */
820 void MCExecution::threadJoin(Thread *blocking) {
822 if (blocking->is_complete()) {
823 EPRecord *join=getOrCreateCurrRecord(THREADJOIN, NULL, 0, 0, 8, false);
824 currexecpoint->incrementTop();
825 join->setJoinThread(blocking->get_id());
828 get_current_thread()->set_waiting(blocking);
829 scheduler->check_preempt();
830 get_current_thread()->set_waiting(NULL);
834 /** @brief Finishes a thread. */
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);
846 scheduler->check_preempt();
849 /** @brief Thread yield. */
851 void MCExecution::threadYield() {
852 getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
853 currexecpoint->incrementTop();
854 if (model->params.noexecyields) {
859 /** @brief Thread yield. */
861 void * MCExecution::alloc(size_t size) {
863 EPRecord *record=getOrCreateCurrRecord(ALLOC, &isNew, 0, 0, 8, false);
864 currexecpoint->incrementTop();
866 size_t allocsize=((size<<1)+7)&~((size_t)(7));
867 record->setSize(allocsize);
868 void *ptr=real_user_malloc(size);
872 if (size>record->getSize()) {
873 model_print("Allocation size changed too much\n");
876 void *ptr=record->getPtr();
881 /** @brief Record enter loop. */
883 void MCExecution::enterLoop() {
884 EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
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);
893 currexecpoint->incrementTop();
895 model_print("ENLOOP ");
896 currexecpoint->print();
901 /** @brief Record exit loop. */
903 void MCExecution::exitLoop() {
905 EPRecord *breakstate=NULL;
907 /* Record last statement */
908 uint tid=id_to_int(currexecpoint->get_tid());
910 if (!currexecpoint->directInLoop()) {
911 breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
912 currexecpoint->incrementTop();
914 breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
915 currexecpoint->incrementTop();
918 /* Get Last Record */
919 EPRecord *lastrecord=(currbranch==NULL) ? (*alwaysexecuted)[tid] : currbranch->lastrecord;
921 /* Remember last record as loop exit for this execution. */
922 if (lastloopexit->size()<=tid) {
923 lastloopexit->resize(tid+1);
925 (*lastloopexit)[tid]=lastrecord;
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();
935 } while(type!=EP_LOOP);
938 model_print("EXLOOP ");
939 currexecpoint->print();
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);
948 breakstate->setNextRecord(labelrec);
949 currexecpoint->incrementTop();
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);
960 /** @brief Helper function to add new item to a StoreLoadHashTable */
962 void addTable(StoreLoadHashTable *table, const void *addr, EPRecord *record) {
963 RecordSet * rset=table->get(addr);
965 rset=new RecordSet();
966 table->put(addr, rset);
971 /** @brief Update mapping from address to stores to that address. */
973 void MCExecution::addStoreTable(const void *addr, EPRecord *record) {
974 addTable(storetable, addr, record);
977 /** @brief Update mapping from address to loads from that address. */
979 void MCExecution::addLoadTable(const void *addr, EPRecord *record) {
980 addTable(loadtable, addr, record);
983 /** @brief Update mapping from address to loads from that address. */
985 RecordSet * MCExecution::getLoadTable(const void *addr) {
986 return loadtable->get(addr);
989 /** @brief Update mapping from address to stores to that address. */
991 RecordSet * MCExecution::getStoreTable(const void *addr) {
992 return storetable->get(addr);
995 /** @brief Registers that component index of deprecord depends on record. */
997 void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsigned int index) {
998 EPRecordSet *set=eprecorddep->get(record);
1000 set=new EPRecordSet();
1001 eprecorddep->put(record, set);
1003 struct RecordIntPair pair={deprecord, index};
1005 if (!set->contains(&pair)) {
1006 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
1011 if (!revrecorddep->contains(&pair)) {
1012 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
1014 revrecorddep->put(p, new ModelVector<EPRecord *>());
1017 ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
1018 for(uint i=0;i<recvec->size();i++) {
1019 if ((*recvec)[i]==record)
1022 recvec->push_back(record);
1025 ModelVector<EPRecord *> * MCExecution::getRevDependences(EPRecord *record, uint index) {
1026 struct RecordIntPair pair={record, index};
1027 return revrecorddep->get(&pair);