X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=schedulebuilder.cc;h=68a4b77f115e5b6ff87571eeee1f5121eea786b6;hb=34698794dfbc5f8f8e757f9ea4d9afa051157ec7;hp=4473c74e3a97461d4187f0af61b3e4af581738bd;hpb=44e8eabc8f7a0ab23c29037a770463d8a2de7b4a;p=satcheck.git

diff --git a/schedulebuilder.cc b/schedulebuilder.cc
index 4473c74..68a4b77 100644
--- a/schedulebuilder.cc
+++ b/schedulebuilder.cc
@@ -13,6 +13,7 @@
 #include "constgen.h"
 #include "branchrecord.h"
 #include "storeloadset.h"
+#include "model.h"
 
 ScheduleBuilder::ScheduleBuilder(MCExecution *_execution, ConstGen *cgen) :
 	cg(cgen),
@@ -26,23 +27,27 @@ ScheduleBuilder::~ScheduleBuilder() {
 
 
 void neatPrint(EPRecord *r, ConstGen *cgen, bool *satsolution) {
-	StoreLoadSet * sls=cgen->getStoreLoadSet(r);
 	r->print();
-	model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
 	switch(r->getType()) {
 	case LOAD: {
-		model_print("rd=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+		StoreLoadSet * sls=cgen->getStoreLoadSet(r);
+		model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
+		model_print("rd=%llu ", sls->getValueEncoding(cgen, r, satsolution));
 	}
-		break;
+	break;
 	case STORE: {
-		model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
-
+		StoreLoadSet * sls=cgen->getStoreLoadSet(r);
+		model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
+		model_print("wr=%llu ", sls->getValueEncoding(cgen, r, satsolution));
 	}
-		break;
+	break;
 	case RMW: {
-		model_print("rd=%lu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
-		model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+		StoreLoadSet * sls=cgen->getStoreLoadSet(r);
+		model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
+		model_print("rd=%llu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
+		model_print("wr=%llu ", sls->getValueEncoding(cgen, r, satsolution));
 	}
+	break;
 	default:
 		;
 	}
@@ -65,7 +70,6 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 			EPRecord *next=processRecord(record, satsolution);
 #ifdef TSO
 			if (next != NULL) {
-			
 				if (next->getType()==STORE) {
 					stores[index]->push_back(next);
 					next=getNextRecord(next);
@@ -80,16 +84,18 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 			}
 #endif
 			if (next!=record) {
+#ifdef DUMP_SAT_SCHEDULE
+				neatPrint(record, cg, satsolution);
+#endif
 				threads[index]=next;
 				index=index-1;
 			}
 		}
 		//Now we have just memory operations, find the first one...make it go first
 		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;
@@ -97,7 +103,6 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 #ifdef TSO
 			if (!stores[index]->empty()) {
 				record=stores[index]->front();
-				
 				if (record!=NULL && (earliest==NULL ||
 														 cg->getOrder(record, earliest, satsolution))) {
 					earliest=record;
@@ -109,6 +114,10 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 		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) {
@@ -149,7 +158,7 @@ EPRecord * ScheduleBuilder::getNextRecord(EPRecord *record) {
 		if (!br->hasNextRecord())
 			next=NULL;
 	}
-	
+
 	if (next==NULL && record->getBranch()!=NULL) {
 		EPValue * epbr=record->getBranch();
 		EPRecord *branch=epbr->getRecord();
@@ -190,7 +199,7 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
 	case MERGE:
 	case ALLOC:
 	case EQUALS:
-	case FUNCTION: 
+	case FUNCTION:
 		/* Continue executing */
 		break;
 	case THREADCREATE:
@@ -208,9 +217,13 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
 		break;
 	case NONLOCALTRANS:
 		break;
+	case LOOPEXIT:
+		break;
 	case LABEL:
 		break;
 	case YIELD:
+		if (model->params.noexecyields)
+			return NULL;
 		break;
 	default:
 		ASSERT(0);