Fix yield bug part 2

diff --git a/config.h b/config.h
index b05bd54fb2771fb9bd8dca7828cf21136bcf04df..a172d1b78336ec6af7b4b0eec68d7f67cc550ceb 100644 (file)
--- 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 82042af420bedfdd4b7b29c084f64aeeb33c081d..e7f8c2d68004928529c2441d2024b0fe7208d85d 100644 (file)
--- 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 6cf4b5aae9598963b8e6a86b2fa6cf68c7319b78..68a4b77f115e5b6ff87571eeee1f5121eea786b6 100644 (file)
--- 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) {