X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=2f9ec63f00d5e6bf113c18d17386dfc22eeea7cd;hb=39c0de028fe3b1c1d229ecf715007c751ddab445;hp=82b90601048845f32a9af77d57e938e8fb11450f;hpb=7888740e94be8706a4e09ae216dcf2e378257617;p=c11tester.git

diff --git a/model.cc b/model.cc
index 82b90601..2f9ec63f 100644
--- a/model.cc
+++ b/model.cc
@@ -91,6 +91,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
 	pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
 	thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
+	thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
 	node_stack(new NodeStack()),
 	priv(new struct model_snapshot_members()),
 	mo_graph(new CycleGraph())
@@ -120,6 +121,7 @@ ModelChecker::~ModelChecker()
 	delete pending_rel_seqs;
 
 	delete thrd_last_action;
+	delete thrd_last_fence_release;
 	delete node_stack;
 	delete scheduler;
 	delete mo_graph;
@@ -703,7 +705,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 				continue;
 			}
 
-			curr->read_from(reads_from);
+			read_from(curr, reads_from);
 			mo_graph->commitChanges();
 			mo_check_promises(curr->get_tid(), reads_from);
 
@@ -712,7 +714,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 			/* Read from future value */
 			value = curr->get_node()->get_future_value();
 			modelclock_t expiration = curr->get_node()->get_future_value_expiration();
-			curr->read_from(NULL);
+			read_from(curr, NULL);
 			Promise *valuepromise = new Promise(curr, value, expiration);
 			promises->push_back(valuepromise);
 		}
@@ -1024,6 +1026,10 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
 
 		/* Always compute new clock vector */
 		newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+		/* Assign most recent release fence */
+		newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
+
 		/*
 		 * Perform one-time actions when pushing new ModelAction onto
 		 * NodeStack
@@ -1041,6 +1047,34 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
 	}
 }
 
+/**
+ * @brief Establish reads-from relation between two actions
+ *
+ * Perform basic operations involved with establishing a concrete rf relation,
+ * including setting the ModelAction data and checking for release sequences.
+ *
+ * @param act The action that is reading (must be a read)
+ * @param rf The action from which we are reading (must be a write)
+ *
+ * @return True if this read established synchronization
+ */
+bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
+{
+	act->set_read_from(rf);
+	if (rf != NULL && act->is_acquire()) {
+		rel_heads_list_t release_heads;
+		get_release_seq_heads(act, &release_heads);
+		int num_heads = release_heads.size();
+		for (unsigned int i = 0; i < release_heads.size(); i++)
+			if (!act->synchronize_with(release_heads[i])) {
+				set_bad_synchronization();
+				num_heads--;
+			}
+		return num_heads > 0;
+	}
+	return false;
+}
+
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -1998,6 +2032,12 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 		thrd_last_action->resize(get_num_threads());
 	(*thrd_last_action)[tid] = act;
 
+	if (act->is_fence() && act->is_release()) {
+		if ((int)thrd_last_fence_release->size() <= tid)
+			thrd_last_fence_release->resize(get_num_threads());
+		(*thrd_last_fence_release)[tid] = act;
+	}
+
 	if (act->is_wait()) {
 		void *mutex_loc=(void *) act->get_value();
 		get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
@@ -2023,6 +2063,20 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
 		return NULL;
 }
 
+/**
+ * @brief Get the last fence release performed by a particular Thread
+ * @param tid The thread ID of the Thread in question
+ * @return The last fence release in the thread, if one exists; NULL otherwise
+ */
+ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
+{
+	int threadid = id_to_int(tid);
+	if (threadid < (int)thrd_last_fence_release->size())
+		return (*thrd_last_fence_release)[id_to_int(tid)];
+	else
+		return NULL;
+}
+
 /**
  * Gets the last memory_order_seq_cst write (in the total global sequence)
  * performed on a particular object (i.e., memory location), not including the
@@ -2128,7 +2182,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			if (read->is_rmw()) {
 				mo_graph->addRMWEdge(write, read);
 			}
-			read->read_from(write);
+			read_from(read, write);
 			//First fix up the modification order for actions that happened
 			//before the read
 			r_modification_order(read, write);