X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=schedulebuilder.cc;h=68a4b77f115e5b6ff87571eeee1f5121eea786b6;hb=HEAD;hp=cc17b1e025d9bcddab4dfce489644df235f5b30e;hpb=e3e2836db3e10d5d1b7a262c7b34f247af076b7a;p=satcheck.git

diff --git a/schedulebuilder.cc b/schedulebuilder.cc
index cc17b1e..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),
@@ -31,22 +32,22 @@ void neatPrint(EPRecord *r, ConstGen *cgen, bool *satsolution) {
 	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:
 		;
 	}
@@ -69,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);
@@ -84,6 +84,9 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 			}
 #endif
 			if (next!=record) {
+#ifdef DUMP_SAT_SCHEDULE
+				neatPrint(record, cg, satsolution);
+#endif
 				threads[index]=next;
 				index=index-1;
 			}
@@ -92,7 +95,7 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 		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;
@@ -111,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) {
@@ -151,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();
@@ -192,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:
@@ -215,6 +222,8 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
 	case LABEL:
 		break;
 	case YIELD:
+		if (model->params.noexecyields)
+			return NULL;
 		break;
 	default:
 		ASSERT(0);