#include "constgen.h"
#include "branchrecord.h"
#include "storeloadset.h"
+#include "model.h"
ScheduleBuilder::ScheduleBuilder(MCExecution *_execution, ConstGen *cgen) :
cg(cgen),
case LOAD: {
StoreLoadSet * sls=cgen->getStoreLoadSet(r);
model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
- model_print("rd=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+ model_print("rd=%llu ", sls->getValueEncoding(cgen, r, satsolution));
}
- break;
+ break;
case STORE: {
StoreLoadSet * sls=cgen->getStoreLoadSet(r);
model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
- model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+ model_print("wr=%llu ", sls->getValueEncoding(cgen, r, satsolution));
}
- break;
+ break;
case RMW: {
StoreLoadSet * sls=cgen->getStoreLoadSet(r);
model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
- model_print("rd=%lu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
- model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+ model_print("rd=%llu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
+ model_print("wr=%llu ", sls->getValueEncoding(cgen, r, satsolution));
}
- break;
+ break;
default:
;
}
EPRecord *next=processRecord(record, satsolution);
#ifdef TSO
if (next != NULL) {
-
if (next->getType()==STORE) {
stores[index]->push_back(next);
next=getNextRecord(next);
}
#endif
if (next!=record) {
+#ifdef DUMP_SAT_SCHEDULE
+ neatPrint(record, cg, satsolution);
+#endif
threads[index]=next;
index=index-1;
}
EPRecord *earliest=NULL;
for(uint index=0;index<threads.size();index++) {
EPRecord *record=threads[index];
-
+
if (record!=NULL && (earliest==NULL ||
cg->getOrder(record, earliest, satsolution))) {
earliest=record;
if (earliest == NULL)
break;
+#ifdef DUMP_SAT_SCHEDULE
+ neatPrint(earliest, cg, satsolution);
+#endif
+
for(uint index=0;index<threads.size();index++) {
EPRecord *record=threads[index];
if (record==earliest) {
if (!br->hasNextRecord())
next=NULL;
}
-
+
if (next==NULL && record->getBranch()!=NULL) {
EPValue * epbr=record->getBranch();
EPRecord *branch=epbr->getRecord();
case MERGE:
case ALLOC:
case EQUALS:
- case FUNCTION:
+ case FUNCTION:
/* Continue executing */
break;
case THREADCREATE:
case LABEL:
break;
case YIELD:
+ if (model->params.noexecyields)
+ return NULL;
break;
default:
ASSERT(0);