Fix TSO Bugs

diff --git a/constgen.cc b/constgen.cc
index cf584646b340ce7d160aba52c1e49e1e8fb797ab..6e452ac747eac71bfb68fee065faef6c4d8daca7 100644 (file)
--- a/constgen.cc
+++ b/constgen.cc
@@ -192,7 +192,7 @@ bool ConstGen::canReuseEncoding() {
                Constraint *var=goalvararray[i];
                if (var != NULL) {
                        if (solution[var->getVar()]) {
-                               //                              if (goalvararray[i] != NULL)
+                               //if (goalvararray[i] != NULL)
                                //model_print("SAT clearing goal %d.\n", i);
 
                                goalvararray[i]=NULL;
@@ -201,7 +201,7 @@ bool ConstGen::canReuseEncoding() {
        }
 
        schedulebuilder->buildSchedule(solution);
-       model_free(solution);   
+       model_free(solution);
 
        return true;
 }
@@ -746,6 +746,15 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
                                Constraint *c13=getOrderConstraint(t1rec, t3rec);
 #ifdef TSO
                                Constraint *c32=getOrderConstraint(t3rec, t2rec);
+                               if (!c32->isFalse()) {
+                                       //Have a store->load that could be reordered, need to generate other constraint
+                                       Constraint *c12=getOrderConstraint(t1rec, t2rec);
+                                       Constraint *c23=getOrderConstraint(t2rec, t3rec);
+                                       Constraint *c31=getOrderConstraint(t3rec, t1rec);
+                                       Constraint *slarray[] = {c31, c23, c12};
+                                       Constraint * intradelayedstore=new Constraint(OR, 3, slarray);
+                                       ADDCONSTRAINT(intradelayedstore, "intradelayedstore");
+                               }
                                Constraint * array[]={c21, c32, c13};
                                Constraint *intratransorder=new Constraint(OR, 3, array);
 #else
@@ -759,6 +768,16 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
                                Constraint *c02=getOrderConstraint(t0rec, t2rec);
 #ifdef TSO
                                Constraint *c10=getOrderConstraint(t1rec, t0rec);
+
+                               if (!c10->isFalse()) {
+                                       //Have a store->load that could be reordered, need to generate other constraint
+                                       Constraint *c01=getOrderConstraint(t0rec, t1rec);
+                                       Constraint *c12=getOrderConstraint(t1rec, t2rec);
+                                       Constraint *c20=getOrderConstraint(t2rec, t0rec);
+                                       Constraint *slarray[] = {c01, c12, c20};
+                                       Constraint * intradelayedstore=new Constraint(OR, 3, slarray);
+                                       ADDCONSTRAINT(intradelayedstore, "intradelayedstore");
+                               }
                                Constraint * array[]={c10, c21, c02};
                                Constraint *intratransorder=new Constraint(OR, 3, array);
 #else

diff --git a/loadrf.cc b/loadrf.cc
index 1b9c551b01d3887dda68605651465dbbf86405f5..f536c1bf336d2340012f4dd3231d99dc58d18e47 100644 (file)
--- a/loadrf.cc
+++ b/loadrf.cc
@@ -84,12 +84,28 @@ void LoadRF::genConstraints(ConstGen *cg) {
                        Constraint * storebeforeconflict=cg->getOrderConstraint(store, conflictstore);
                        if (storebeforeconflict->isFalse())
                                continue;
+#ifdef TSO
+                       //Have to cover the same thread case
+                       Constraint *conflictbeforeload;
+                       if (conflictstore->getEP()->get_tid()==load->getEP()->get_tid()) {
+                               if (conflictstore->getEP()->compare(load->getEP())==CR_AFTER)
+                                       conflictbeforeload=&ctrue;
+                               else
+                                       conflictbeforeload=&cfalse;
+                       } else {
+                               conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
+                       }
+                       if (conflictbeforeload->isFalse()) {
+                               storebeforeconflict->freerec();
+                               continue;
+                       }
+#else
                        Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);    
                        if (conflictbeforeload->isFalse()) {
                                storebeforeconflict->freerec();
                                continue;
                        }
-
+#endif
                        rfconst=generateConstraint(numvars, vars, storeindex);
                        Constraint *array[]={storebeforeconflict,
                                                                                                         conflictbeforeload,

diff --git a/mcexecution.cc b/mcexecution.cc
index 404569a1ff92e927098d2b0830d80a44f6f71025..36afe0b81f030112102e0f7a07e2ae1c9e69c09f 100644 (file)
--- a/mcexecution.cc
+++ b/mcexecution.cc
@@ -312,6 +312,9 @@ void MCExecution::doStore(thread_id_t tid) {
        SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
        EPValue * epval=list->front();
        list->pop_front();
+       if (DBG_ENABLED()) {
+               model_print("tid = %lu: ", tid);
+       }
        doStore(epval);
 }