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<SnapList<EPValue *> *>();
#endif
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;i<EPList->size();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);
}
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);
SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
return list->empty();
}
-
+
void MCExecution::doStore(thread_id_t tid) {
SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
EPValue * epval=list->front();
list->pop_front();
+ if (DBG_ENABLED()) {
+ model_print("tid = %d: ", tid);
+ }
doStore(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;
#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();
break;
}
#endif
-
+
if (DBG_ENABLED()) {
- model_print("STORE *%p=%lu ", addr, val);
+ model_print("STORE *%p=%llu ", addr, val);
currexecpoint->print();
model_print("\n");
}
bool found=false;
uint tid=id_to_int(currexecpoint->get_tid());
SnapList<EPValue *> *list=(*storebuffer)[tid];
- for(SnapList<EPValue *>::reverse_iterator it=list->rbegin(); it != list->rend(); it++) {
+ for(SnapList<EPValue *>::reverse_iterator it=list->rbegin();it != list->rend();it++) {
EPValue *epval=*it;
const void *epaddr=epval->getAddr();
if (epaddr == addr) {
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");
}
}
/** @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);
for(int i=0;i<curr_length-orig_length;i++)
currexecpoint->pop();
//increment top
- currexecpoint->incrementTop();
+ currexecpoint->incrementTop();
//now we can create the merge point
if (DBG_ENABLED()) {
model_print("MERGE mid=%u", mcid);
MCID mcids[]={input};
recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
-
+
MCID fnmcid=getNextMCID();
ASSERT(EPList->size()==fnmcid);
EPList->push_back(epvalue);
*p=rip;
phiset->add(p);
}
-
+
MCID fnmcid=getNextMCID();
ASSERT(EPList->size()==fnmcid);
EPList->push_back(epvalue);
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;i<VC_BASEINDEX;i++) {
valarray[i]=0;
delete rit;
}
}
-
+
return fnmcid;
}
(*CurrBranchList)[oldtid]=currbranch;
}
curr_thread=t;
- currexecpoint=(t==NULL)?NULL:(*ExecPointList)[id_to_int(t->get_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) {
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);
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 ");
/* Record last statement */
uint tid=id_to_int(currexecpoint->get_tid());
-
+
if (!currexecpoint->directInLoop()) {
breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
currexecpoint->incrementTop();
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);
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<EPRecord *>());
}
-
+
ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
for(uint i=0;i<recvec->size();i++) {
if ((*recvec)[i]==record)
projects / satcheck.git / blobdiff