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 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 dprintf(file, "%lu[label=\"",(uintptr_t)record);
123 dprintf(file, "\"];\n");
125 dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record);
128 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=%lu valarg=%lu retval=%lu", 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();
318 void MCExecution::doStore(EPValue *epval) {
319 const void *addr=epval->getAddr();
320 uint64_t val=epval->getValue();
321 int len=epval->getLen();
323 model_print("flushing %d bytes *(%p) = %lu", len, addr, val);
324 currexecpoint->print();
329 (*(uint8_t *)addr) = (uint8_t)val;
332 (*(uint16_t *)addr) = (uint16_t)val;
335 (*(uint32_t *)addr) = (uint32_t)val;
338 (*(uint64_t *)addr) = (uint64_t)val;
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();
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.
364 void MCExecution::recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids) {
365 EPRecord *currrecord=epv->getRecord();
367 for(int i=0;i<numids;i++) {
369 if (id != MCID_NODEP) {
370 EPRecord * epi=getEPRecord(id);
371 addRecordDepTable(epi,currrecord, VC_BASEINDEX+i);
374 if (rf != MCID_NODEP) {
375 EPRecord *eprf=getEPRecord(rf);
376 addRecordDepTable(eprf,currrecord, VC_RFINDEX);
378 if (addr != MCID_NODEP) {
379 EPRecord *epaddr=getEPRecord(addr);
380 addRecordDepTable(epaddr,currrecord, VC_ADDRINDEX);
384 /** @brief Processes a store. */
386 void MCExecution::store(void *addr, uint64_t val, int len) {
390 (*(uint8_t *)addr) = (uint8_t)val;
393 (*(uint16_t *)addr) = (uint16_t)val;
396 (*(uint32_t *)addr) = (uint32_t)val;
399 (*(uint64_t *)addr) = (uint64_t)val;
405 model_print("STORE *%p=%lu ", addr, val);
406 currexecpoint->print();
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);
414 uint tid=id_to_int(currexecpoint->get_tid());
415 (*storebuffer)[tid]->push_back(epvalue);
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();
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));
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));
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));
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));
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));
457 if (!store->hasValue(val)) {
458 store->getSet(VC_BASEINDEX)->add(val);
459 planner->addChange(new MCChange(store, val, VC_BASEINDEX));
463 /** @brief Processes a load. */
465 uint64_t MCExecution::load(const void *addr, int len) {
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++) {
473 const void *epaddr=epval->getAddr();
474 if (epaddr == addr) {
475 val = epval->getValue();
483 val=*(uint8_t *) addr;
486 val=*(uint16_t *) addr;
489 val=*(uint32_t *) addr;
492 val=*(uint64_t *) addr;
500 val=*(uint8_t *) addr;
503 val=*(uint16_t *) addr;
506 val=*(uint32_t *) addr;
509 val=*(uint64_t *) addr;
515 model_print("%lu(mid=%u)=LOAD %p ", val, id_retval, addr);
516 currexecpoint->print();
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();
532 /** @brief Processes a branch. */
534 MCID MCExecution::branchDir(MCID dirid, int direction, int numdirs, bool anyvalue) {
536 model_print("BRANCH dir=%u mid=%u", direction, dirid);
537 currexecpoint->print();
540 EPRecord * record=getOrCreateCurrRecord(BRANCHDIR, NULL, 0, 1, numdirs, anyvalue);
542 EPValue * epvalue=getEPValue(record, &isNew, NULL, direction, 32);
544 #ifdef PRINT_ACHIEVED_GOALS
545 model_print("Achieved Goal: BRANCH dir=%u mid=%u", direction, dirid);
546 currexecpoint->print();model_print("\n");
549 planner->getConstGen()->curr_stat->bgoals++;
551 planner->getConstGen()->achievedGoal(record);
552 scheduler->setNewFlag();
554 //record that we took a branch
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);
570 /** @brief Processes a merge with a previous branch. mcid gives the
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();
583 currexecpoint->incrementTop();
584 //now we can create the merge point
586 model_print("MERGE mid=%u", mcid);
587 currexecpoint->print();
590 getOrCreateCurrRecord(MERGE, NULL, 0, 0, 8, false);
591 currexecpoint->incrementTop();
594 /** @brief Phi function. */
595 MCID MCExecution::phi(MCID input) {
596 EPRecord * record=getOrCreateCurrRecord(FUNCTION, NULL, 0, 1, 8, false);
598 EPValue *epinput=getEPValue(input);
599 EPValue * epvalue=getEPValue(record, NULL, NULL, epinput->getValue(), 8);
601 MCID mcids[]={input};
602 recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
604 MCID fnmcid=getNextMCID();
605 ASSERT(EPList->size()==fnmcid);
606 EPList->push_back(epvalue);
607 currexecpoint->incrementTop();
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);
619 MCID mcids[]={input};
620 recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
622 uint tid=id_to_int(currexecpoint->get_tid());
623 EPRecord *exitrec=(*lastloopexit)[tid];
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));
633 MCID fnmcid=getNextMCID();
634 ASSERT(EPList->size()==fnmcid);
635 EPList->push_back(epvalue);
636 currexecpoint->incrementTop();
641 uint64_t MCExecution::equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, MCID *retval) {
642 uint64_t eq=(val1==val2);
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);
651 recordFunctionChange(record, 0);
652 recordFunctionChange(record, 1);
654 MCID eqmcid=getNextMCID();
655 ASSERT(EPList->size()==eqmcid);
656 EPList->push_back(epvalue);
657 currexecpoint->incrementTop();
662 /** @brief Processes an uninterpretted function. */
664 MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint numids, MCID *mcids) {
666 EPRecord * record=getOrCreateCurrRecord(FUNCTION, &isNew, 0, numids, len, false);
668 if (functionidentifier == 0)
669 record->setCompletedGoal(new CGoalSet(), false);
671 if (sharedgoals->size()<=functionidentifier) {
672 sharedgoals->resize(functionidentifier+1);
673 sharedfuncrecords->resize(functionidentifier+1);
675 if ((*sharedgoals)[functionidentifier]==NULL) {
676 (*sharedgoals)[functionidentifier]=new CGoalSet();
677 (*sharedfuncrecords)[functionidentifier]=new RecordSet();
679 record->setCompletedGoal((*sharedgoals)[functionidentifier], true);
680 (*sharedfuncrecords)[functionidentifier]->add(record);
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);
693 CGoalIterator *cit=(*sharedgoals)[functionidentifier]->iterator();
694 while(cit->hasNext()) {
695 CGoal *goal=cit->next();
696 evalGoal(record, goal);
701 val=val&getmask(len);
702 EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
703 recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
705 uint64_t valarray[numids+VC_BASEINDEX];
706 for(uint i=0;i<VC_BASEINDEX;i++) {
709 for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
710 valarray[i]=getEPValue(mcids[i-VC_BASEINDEX])->getValue();
713 MCID fnmcid=getNextMCID();
714 ASSERT(EPList->size()==fnmcid);
715 EPList->push_back(epvalue);
716 currexecpoint->incrementTop();
718 CGoal *goal=new CGoal(numids+VC_BASEINDEX, valarray);
719 if (record->completedGoalSet()->contains(goal)) {
722 scheduler->setNewFlag();
723 planner->getConstGen()->achievedGoal(record);
724 #ifdef PRINT_ACHIEVED_GOALS
725 model_print("Achieved goal:");goal->print();model_print("\n");
728 planner->getConstGen()->curr_stat->fgoals++;
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();
739 evalGoal(func, goal);
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))
754 //Have all input, propagate output
755 recordFunctionChange(record, goal->getOutput());
758 /** @brief Returns the next thread id. */
760 thread_id_t MCExecution::get_next_tid() {
761 return int_to_id(snap_fields->next_thread_id++);
764 /** @brief Registers a new thread */
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);
773 storebuffer->push_back(new SnapList<EPValue *>());
777 /** @brief Records currently executing thread. */
779 void MCExecution::set_current_thread(Thread *t) {
781 uint oldtid=id_to_int(curr_thread->get_id());
782 (*CurrBranchList)[oldtid]=currbranch;
785 currexecpoint=(t==NULL)?NULL:(*ExecPointList)[id_to_int(t->get_id())];
786 currbranch=(t==NULL)?NULL:(*CurrBranchList)[id_to_int(t->get_id())];
789 void MCExecution::threadStart(EPRecord *parent) {
790 EPRecord *threadstart=getOrCreateCurrRecord(THREADBEGIN, NULL, 0, 0, 8, false);
792 parent->setChildRecord(threadstart);
794 currexecpoint->incrementTop();
797 /** @brief Create a new thread. */
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);
806 /** @brief Joins with a thread. */
808 void MCExecution::threadJoin(Thread *blocking) {
810 if (blocking->is_complete()) {
811 EPRecord *join=getOrCreateCurrRecord(THREADJOIN, NULL, 0, 0, 8, false);
812 currexecpoint->incrementTop();
813 join->setJoinThread(blocking->get_id());
816 get_current_thread()->set_waiting(blocking);
817 scheduler->check_preempt();
818 get_current_thread()->set_waiting(NULL);
822 /** @brief Finishes a thread. */
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);
834 scheduler->check_preempt();
837 /** @brief Thread yield. */
839 void MCExecution::threadYield() {
840 getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
841 currexecpoint->incrementTop();
844 /** @brief Thread yield. */
846 void * MCExecution::alloc(size_t size) {
848 EPRecord *record=getOrCreateCurrRecord(ALLOC, &isNew, 0, 0, 8, false);
849 currexecpoint->incrementTop();
851 size_t allocsize=((size<<1)+7)&~((size_t)(7));
852 record->setSize(allocsize);
853 void *ptr=real_user_malloc(size);
857 if (size>record->getSize()) {
858 model_print("Allocation size changed too much\n");
861 void *ptr=record->getPtr();
866 /** @brief Record enter loop. */
868 void MCExecution::enterLoop() {
869 EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
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);
878 currexecpoint->incrementTop();
880 model_print("ENLOOP ");
881 currexecpoint->print();
886 /** @brief Record exit loop. */
888 void MCExecution::exitLoop() {
890 EPRecord *breakstate=NULL;
892 /* Record last statement */
893 uint tid=id_to_int(currexecpoint->get_tid());
895 if (!currexecpoint->directInLoop()) {
896 breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
897 currexecpoint->incrementTop();
899 breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
900 currexecpoint->incrementTop();
903 /* Get Last Record */
904 EPRecord *lastrecord=(currbranch==NULL)?(*alwaysexecuted)[tid]:currbranch->lastrecord;
906 /* Remember last record as loop exit for this execution. */
907 if (lastloopexit->size()<=tid) {
908 lastloopexit->resize(tid+1);
910 (*lastloopexit)[tid]=lastrecord;
913 type=currexecpoint->getType();
914 currexecpoint->pop();
915 if (type==EP_BRANCH) {
916 //we crossed a branch, fix currbranch
917 EPRecord *branch=currbranch->getRecord();
918 currbranch=branch->getBranch();
920 } while(type!=EP_LOOP);
923 model_print("EXLOOP ");
924 currexecpoint->print();
927 EPRecord *loopenter=EPTable->get(currexecpoint);
928 currexecpoint->incrementTop();
929 EPRecord *labelrec=getOrCreateCurrRecord(LABEL, NULL, 0, 0, 8, false);
930 if (loopenter->getNextRecord()==NULL) {
931 loopenter->setNextRecord(labelrec);
933 breakstate->setNextRecord(labelrec);
934 currexecpoint->incrementTop();
937 /** @brief Record next loop iteration. */
938 void MCExecution::loopIterate() {
939 currexecpoint->pop();
940 //increment the iteration counter
941 currexecpoint->incrementTop();
942 currexecpoint->push(EP_COUNTER,0);
945 /** @brief Helper function to add new item to a StoreLoadHashTable */
947 void addTable(StoreLoadHashTable *table, const void *addr, EPRecord *record) {
948 RecordSet * rset=table->get(addr);
950 rset=new RecordSet();
951 table->put(addr, rset);
956 /** @brief Update mapping from address to stores to that address. */
958 void MCExecution::addStoreTable(const void *addr, EPRecord *record) {
959 addTable(storetable, addr, record);
962 /** @brief Update mapping from address to loads from that address. */
964 void MCExecution::addLoadTable(const void *addr, EPRecord *record) {
965 addTable(loadtable, addr, record);
968 /** @brief Update mapping from address to loads from that address. */
970 RecordSet * MCExecution::getLoadTable(const void *addr) {
971 return loadtable->get(addr);
974 /** @brief Update mapping from address to stores to that address. */
976 RecordSet * MCExecution::getStoreTable(const void *addr) {
977 return storetable->get(addr);
980 /** @brief Registers that component index of deprecord depends on record. */
982 void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsigned int index) {
983 EPRecordSet *set=eprecorddep->get(record);
985 set=new EPRecordSet();
986 eprecorddep->put(record, set);
988 struct RecordIntPair pair={deprecord, index};
990 if (!set->contains(&pair)) {
991 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
996 if (!revrecorddep->contains(&pair)) {
997 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
999 revrecorddep->put(p, new ModelVector<EPRecord *>());
1002 ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
1003 for(uint i=0;i<recvec->size();i++) {
1004 if ((*recvec)[i]==record)
1007 recvec->push_back(record);
1010 ModelVector<EPRecord *> * MCExecution::getRevDependences(EPRecord *record, uint index) {
1011 struct RecordIntPair pair={record, index};
1012 return revrecorddep->get(&pair);