From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 19 Jul 2012 19:18:25 +0000 (-0700)
Subject: small changes (things still work) towards support RMW
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=b5518c866ccd232fa79a2911ce5c6bcaa2110076

small changes (things still work) towards support RMW

Reserve value field only for writes. Using it for reads will only make thinks
weird for RMW operations.

[Amended by Brian Norris]
---

diff --git a/action.cc b/action.cc
index b5c72c02..c617f0d7 100644
--- a/action.cc
+++ b/action.cc
@@ -28,12 +28,12 @@ ModelAction::~ModelAction()
 
 bool ModelAction::is_read() const
 {
-	return type == ATOMIC_READ;
+	return type == ATOMIC_READ || type == ATOMIC_RMW;
 }
 
 bool ModelAction::is_write() const
 {
-	return type == ATOMIC_WRITE || type == ATOMIC_INIT;
+	return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT;
 }
 
 bool ModelAction::is_rmw() const
@@ -85,6 +85,15 @@ bool ModelAction::same_thread(const ModelAction *act) const
 	return tid == act->tid;
 }
 
+void ModelAction::upgrade_rmw(ModelAction * act) {
+	ASSERT(is_read());
+	ASSERT(act->is_rmw());
+	//Upgrade our type to the act's type
+	this->type=act->type;
+	this->order=act->order;
+	this->value=act->value;
+}
+
 /** The is_synchronizing method should only explore interleavings if:
  *  (1) the operations are seq_cst and don't commute or
  *  (2) the reordering may establish or break a synchronization relation.
@@ -136,7 +145,6 @@ void ModelAction::read_from(const ModelAction *act)
 	if (act->is_release() && this->is_acquire())
 		cv->merge(act->cv);
 	reads_from = act;
-	value = act->value;
 }
 
 /**
@@ -182,8 +190,10 @@ void ModelAction::print(void) const
 		type_str = "unknown type";
 	}
 
+	uint64_t valuetoprint=type==ATOMIC_READ?reads_from->value:value;
+
 	printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %-12" PRIu64,
-			seq_number, id_to_int(tid), type_str, order, location, value);
+			seq_number, id_to_int(tid), type_str, order, location, valuetoprint);
 	if (reads_from)
 		printf(" Rf: %d", reads_from->get_seq_number());
 	if (cv) {
diff --git a/action.h b/action.h
index 36c72079..fff6bc82 100644
--- a/action.h
+++ b/action.h
@@ -80,6 +80,8 @@ public:
 		return get_seq_number() > act.get_seq_number();
 	}
 
+	void upgrade_rmw(ModelAction * act);
+
 	MEMALLOC
 private:
 
@@ -95,8 +97,7 @@ private:
 	/** The thread id that performed this action. */
 	thread_id_t tid;
 
-	/** The value read or written (if RMW, then the value written). This
-	 * should probably be something longer. */
+	/** The value written (for write or RMW; undefined for read) */
 	uint64_t value;
 
 	/** The action that this action reads from. Only valid for reads */
diff --git a/model.cc b/model.cc
index cf845ecd..1b379000 100644
--- a/model.cc
+++ b/model.cc
@@ -252,6 +252,15 @@ void ModelChecker::check_current_action(void)
 		return;
 	}
 
+	if (curr->is_rmw()) {
+		//We have a RMW action
+		process_rmw(curr);
+		//Force the current thread to continue since the RMW should be atomic
+		nextThread = thread_current()->get_id();
+		delete curr;
+		return;
+	}
+
 	tmp = node_stack->explore_action(curr);
 	if (tmp) {
 		/* Discard duplicate ModelAction; use action from NodeStack */
@@ -274,6 +283,10 @@ void ModelChecker::check_current_action(void)
 		th->set_creation(curr);
 	}
 
+	/* Is there a better interface for setting the next thread rather
+		 than this field/convoluted approach?  Perhaps like just returning
+		 it or something? */
+
 	nextThread = get_next_replay_thread();
 
 	Node *currnode = curr->get_node();
@@ -310,6 +323,15 @@ bool ModelChecker::isfeasible() {
 	return !cyclegraph->checkForCycles();
 }
 
+/** Process a RMW by converting previous read into a RMW. */
+void ModelChecker::process_rmw(ModelAction * act) {
+	int tid = id_to_int(act->get_tid());
+	std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
+	ASSERT(tid < (int) vec->size());
+	ModelAction *lastread=(*vec)[tid].back();
+	lastread->upgrade_rmw(act);
+}
+
 void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
 	std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
 	unsigned int i;
diff --git a/model.h b/model.h
index 4c0af0af..a4751099 100644
--- a/model.h
+++ b/model.h
@@ -83,6 +83,7 @@ private:
 	ModelAction * get_parent_action(thread_id_t tid);
 	ModelAction * get_last_seq_cst(const void *location);
 	void build_reads_from_past(ModelAction *curr);
+	void process_rmw(ModelAction * curr);
 	void r_modification_order(ModelAction * curr, const ModelAction *rf);
 	void w_modification_order(ModelAction * curr);