From: bdemsky <bdemsky@uci.edu>
Date: Wed, 21 Dec 2016 02:10:11 +0000 (-0800)
Subject: Fix yield bug part 2
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satcheck.git;a=commitdiff_plain;h=40913ce63d171f125117caab249218839fd4b083

Fix yield bug part 2
---

diff --git a/config.h b/config.h
index b05bd54..a172d1b 100644
--- a/config.h
+++ b/config.h
@@ -48,6 +48,9 @@
 /* Size of stack to allocate for a thread. */
 #define STACK_SIZE (1024 * 1024)
 
+/** Dump schedule extracted from SAT Solution */
+//#define DUMP_SAT_SCHEDULE
+
 /** Enable debugging assertions (via ASSERT()) */
 //#define CONFIG_ASSERT
 
diff --git a/constgen.cc b/constgen.cc
index 82042af..e7f8c2d 100644
--- a/constgen.cc
+++ b/constgen.cc
@@ -1490,19 +1490,20 @@ void ConstGen::computeYieldCond(EPRecord *record) {
 	ExecPoint *yieldep=record->getEP();
 	EPRecord *prevyield=NULL;
 	ExecPoint *prevyieldep=NULL;
-	
+
 	for(int i=(int)(yieldlist->size()-1);i>=0;i--) {
 		EPRecord *tmpyield=(*yieldlist)[i];
 		ExecPoint *tmpep=tmpyield->getEP();
-		//Do we have a previous yield operation
-		if (yieldep->compare(tmpep)==CR_BEFORE) {
+		//Do we have a previous yield operation from the same thread
+		if (tmpep->get_tid()==yieldep->get_tid() &&
+				yieldep->compare(tmpep)==CR_BEFORE) {
 			//Yes
 			prevyield=tmpyield;
 			prevyieldep=prevyield->getEP();
 			break;
 		}
 	}
-	
+
 	yieldlist->push_back(record);
 
 	ModelVector<Constraint *> * novel_branches=new ModelVector<Constraint *>();
@@ -1510,6 +1511,11 @@ void ConstGen::computeYieldCond(EPRecord *record) {
 	while(sri->hasNext()) {
 		EPRecord * unexploredbranch=sri->next();
 		ExecPoint * branchep=unexploredbranch->getEP();
+		if (branchep->get_tid()!=yieldep->get_tid()) {
+			//wrong thread
+			continue;
+		}
+
 		if (yieldep->compare(branchep)!=CR_BEFORE) {
 			//Branch does not occur before yield, so skip
 			continue;
@@ -1519,9 +1525,8 @@ void ConstGen::computeYieldCond(EPRecord *record) {
 		if (prevyield != NULL &&
 				prevyieldep->compare(branchep)==CR_BEFORE) {
 			//Branch occurs before previous yield, so we can safely skip this branch
-						continue;
+			continue;
 		}
-
 		//This is a branch that could prevent this yield from being executed
 		BranchRecord *br=branchtable->get(unexploredbranch);
 		Constraint * novel_branch=br->getNewBranch();
diff --git a/schedulebuilder.cc b/schedulebuilder.cc
index 6cf4b5a..68a4b77 100644
--- a/schedulebuilder.cc
+++ b/schedulebuilder.cc
@@ -70,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);
@@ -85,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;
 			}
@@ -112,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) {