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=%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();
316 model_print("tid = %lu: ", 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) = %lu", 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=%lu ", 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("%lu(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);
657 MCID eqmcid=getNextMCID();
658 ASSERT(EPList->size()==eqmcid);
659 EPList->push_back(epvalue);
660 currexecpoint->incrementTop();
665 /** @brief Processes an uninterpretted function. */
667 MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint numids, MCID *mcids) {
669 EPRecord * record=getOrCreateCurrRecord(FUNCTION, &isNew, 0, numids, len, false);
671 if (functionidentifier == 0)
672 record->setCompletedGoal(new CGoalSet(), false);
674 if (sharedgoals->size()<=functionidentifier) {
675 sharedgoals->resize(functionidentifier+1);
676 sharedfuncrecords->resize(functionidentifier+1);
678 if ((*sharedgoals)[functionidentifier]==NULL) {
679 (*sharedgoals)[functionidentifier]=new CGoalSet();
680 (*sharedfuncrecords)[functionidentifier]=new RecordSet();
682 record->setCompletedGoal((*sharedgoals)[functionidentifier], true);
683 (*sharedfuncrecords)[functionidentifier]->add(record);
685 for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
686 EPRecord *input=getEPRecord(mcids[i-VC_BASEINDEX]);
687 IntIterator *inputit=input->getReturnValueSet()->iterator();
688 IntHashSet *recinputset=record->getSet(i);
689 while(inputit->hasNext()) {
690 uint64_t inputval=inputit->next();
691 recinputset->add(inputval);
696 CGoalIterator *cit=(*sharedgoals)[functionidentifier]->iterator();
697 while(cit->hasNext()) {
698 CGoal *goal=cit->next();
699 evalGoal(record, goal);
704 val=val&getmask(len);
705 EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
706 recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
708 uint64_t valarray[numids+VC_BASEINDEX];
709 for(uint i=0;i<VC_BASEINDEX;i++) {
712 for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
713 valarray[i]=getEPValue(mcids[i-VC_BASEINDEX])->getValue();
716 MCID fnmcid=getNextMCID();
717 ASSERT(EPList->size()==fnmcid);
718 EPList->push_back(epvalue);
719 currexecpoint->incrementTop();
721 CGoal *goal=new CGoal(numids+VC_BASEINDEX, valarray);
722 if (record->completedGoalSet()->contains(goal)) {
725 scheduler->setNewFlag();
726 planner->getConstGen()->achievedGoal(record);
727 #ifdef PRINT_ACHIEVED_GOALS
728 model_print("Achieved goal:");goal->print();model_print("\n");
731 planner->getConstGen()->curr_stat->fgoals++;
733 goal->setOutput(val);
734 record->completedGoalSet()->add(goal);
735 recordFunctionChange(record, val);
736 if (functionidentifier != 0) {
737 RecordIterator *rit=(*sharedfuncrecords)[functionidentifier]->iterator();
738 while(rit->hasNext()) {
739 EPRecord *func=rit->next();
742 evalGoal(func, goal);
751 void MCExecution::evalGoal(EPRecord *record, CGoal *goal) {
752 for(uint i=VC_BASEINDEX;i<goal->getNum();i++) {
753 uint64_t input=goal->getValue(i);
754 if (!record->getSet(i)->contains(input))
757 //Have all input, propagate output
758 recordFunctionChange(record, goal->getOutput());
761 /** @brief Returns the next thread id. */
763 thread_id_t MCExecution::get_next_tid() {
764 return int_to_id(snap_fields->next_thread_id++);
767 /** @brief Registers a new thread */
769 void MCExecution::add_thread(Thread *t) {
770 ThreadList->push_back(t);
771 ExecPoint * ep=new ExecPoint(4, t->get_id());
772 ep->push(EP_COUNTER,0);
773 ExecPointList->push_back(ep);
774 CurrBranchList->push_back(NULL);
776 storebuffer->push_back(new SnapList<EPValue *>());
780 /** @brief Records currently executing thread. */
782 void MCExecution::set_current_thread(Thread *t) {
784 uint oldtid=id_to_int(curr_thread->get_id());
785 (*CurrBranchList)[oldtid]=currbranch;
788 currexecpoint=(t==NULL)?NULL:(*ExecPointList)[id_to_int(t->get_id())];
789 currbranch=(t==NULL)?NULL:(*CurrBranchList)[id_to_int(t->get_id())];
792 void MCExecution::threadStart(EPRecord *parent) {
793 EPRecord *threadstart=getOrCreateCurrRecord(THREADBEGIN, NULL, 0, 0, 8, false);
795 parent->setChildRecord(threadstart);
797 currexecpoint->incrementTop();
800 /** @brief Create a new thread. */
802 void MCExecution::threadCreate(thrd_t *t, thrd_start_t start, void *arg) {
803 EPRecord *threadstart=getOrCreateCurrRecord(THREADCREATE, NULL, 0, 0, 8, false);
804 currexecpoint->incrementTop();
805 Thread *th = new Thread(get_next_tid(), t, start, arg, curr_thread, threadstart);
809 /** @brief Joins with a thread. */
811 void MCExecution::threadJoin(Thread *blocking) {
813 if (blocking->is_complete()) {
814 EPRecord *join=getOrCreateCurrRecord(THREADJOIN, NULL, 0, 0, 8, false);
815 currexecpoint->incrementTop();
816 join->setJoinThread(blocking->get_id());
819 get_current_thread()->set_waiting(blocking);
820 scheduler->check_preempt();
821 get_current_thread()->set_waiting(NULL);
825 /** @brief Finishes a thread. */
827 void MCExecution::threadFinish() {
828 Thread *th = get_current_thread();
829 /* Wake up any joining threads */
830 for (unsigned int i = 0; i < get_num_threads(); i++) {
831 Thread *waiting = get_thread(int_to_id(i));
832 if (waiting->waiting_on() == th) {
833 waiting->set_waiting(NULL);
837 scheduler->check_preempt();
840 /** @brief Thread yield. */
842 void MCExecution::threadYield() {
843 getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
844 currexecpoint->incrementTop();
847 /** @brief Thread yield. */
849 void * MCExecution::alloc(size_t size) {
851 EPRecord *record=getOrCreateCurrRecord(ALLOC, &isNew, 0, 0, 8, false);
852 currexecpoint->incrementTop();
854 size_t allocsize=((size<<1)+7)&~((size_t)(7));
855 record->setSize(allocsize);
856 void *ptr=real_user_malloc(size);
860 if (size>record->getSize()) {
861 model_print("Allocation size changed too much\n");
864 void *ptr=record->getPtr();
869 /** @brief Record enter loop. */
871 void MCExecution::enterLoop() {
872 EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
874 //push the loop iteration counter
875 currexecpoint->push(EP_LOOP,0);
876 //push the curr iteration statement counter
877 currexecpoint->push(EP_COUNTER,0);
878 EPRecord * lpstartrecord=getOrCreateCurrRecord(LOOPSTART, NULL, 0, 0, 8, false);
879 record->setChildRecord(lpstartrecord);
881 currexecpoint->incrementTop();
883 model_print("ENLOOP ");
884 currexecpoint->print();
889 /** @brief Record exit loop. */
891 void MCExecution::exitLoop() {
893 EPRecord *breakstate=NULL;
895 /* Record last statement */
896 uint tid=id_to_int(currexecpoint->get_tid());
898 if (!currexecpoint->directInLoop()) {
899 breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
900 currexecpoint->incrementTop();
902 breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
903 currexecpoint->incrementTop();
906 /* Get Last Record */
907 EPRecord *lastrecord=(currbranch==NULL)?(*alwaysexecuted)[tid]:currbranch->lastrecord;
909 /* Remember last record as loop exit for this execution. */
910 if (lastloopexit->size()<=tid) {
911 lastloopexit->resize(tid+1);
913 (*lastloopexit)[tid]=lastrecord;
916 type=currexecpoint->getType();
917 currexecpoint->pop();
918 if (type==EP_BRANCH) {
919 //we crossed a branch, fix currbranch
920 EPRecord *branch=currbranch->getRecord();
921 currbranch=branch->getBranch();
923 } while(type!=EP_LOOP);
926 model_print("EXLOOP ");
927 currexecpoint->print();
930 EPRecord *loopenter=EPTable->get(currexecpoint);
931 currexecpoint->incrementTop();
932 EPRecord *labelrec=getOrCreateCurrRecord(LABEL, NULL, 0, 0, 8, false);
933 if (loopenter->getNextRecord()==NULL) {
934 loopenter->setNextRecord(labelrec);
936 breakstate->setNextRecord(labelrec);
937 currexecpoint->incrementTop();
940 /** @brief Record next loop iteration. */
941 void MCExecution::loopIterate() {
942 currexecpoint->pop();
943 //increment the iteration counter
944 currexecpoint->incrementTop();
945 currexecpoint->push(EP_COUNTER,0);
948 /** @brief Helper function to add new item to a StoreLoadHashTable */
950 void addTable(StoreLoadHashTable *table, const void *addr, EPRecord *record) {
951 RecordSet * rset=table->get(addr);
953 rset=new RecordSet();
954 table->put(addr, rset);
959 /** @brief Update mapping from address to stores to that address. */
961 void MCExecution::addStoreTable(const void *addr, EPRecord *record) {
962 addTable(storetable, addr, record);
965 /** @brief Update mapping from address to loads from that address. */
967 void MCExecution::addLoadTable(const void *addr, EPRecord *record) {
968 addTable(loadtable, addr, record);
971 /** @brief Update mapping from address to loads from that address. */
973 RecordSet * MCExecution::getLoadTable(const void *addr) {
974 return loadtable->get(addr);
977 /** @brief Update mapping from address to stores to that address. */
979 RecordSet * MCExecution::getStoreTable(const void *addr) {
980 return storetable->get(addr);
983 /** @brief Registers that component index of deprecord depends on record. */
985 void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsigned int index) {
986 EPRecordSet *set=eprecorddep->get(record);
988 set=new EPRecordSet();
989 eprecorddep->put(record, set);
991 struct RecordIntPair pair={deprecord, index};
993 if (!set->contains(&pair)) {
994 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
999 if (!revrecorddep->contains(&pair)) {
1000 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
1002 revrecorddep->put(p, new ModelVector<EPRecord *>());
1005 ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
1006 for(uint i=0;i<recvec->size();i++) {
1007 if ((*recvec)[i]==record)
1010 recvec->push_back(record);
1013 ModelVector<EPRecord *> * MCExecution::getRevDependences(EPRecord *record, uint index) {
1014 struct RecordIntPair pair={record, index};
1015 return revrecorddep->get(&pair);