From 0174ae3f85cabaca148065bb9a83019dc5260e64 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 23 Nov 2016 22:29:18 -0800
Subject: [PATCH] Fix TSO Bugs

---
 constgen.cc    | 23 +++++++++++++++++++++--
 loadrf.cc      | 18 +++++++++++++++++-
 mcexecution.cc |  3 +++
 3 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/constgen.cc b/constgen.cc
index cf58464..6e452ac 100644
--- 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 1b9c551..f536c1b 100644
--- 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 404569a..36afe0b 100644
--- 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);
 }
 
-- 
2.34.1