X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=model.cc;h=8267377faa791a2cfbc85f9027949c7338186635;hb=9b894e117ad1090ad6f54753cde7fd9b6ea60ab7;hp=c5e41ab74c4be12cc8605860548abee71192a532;hpb=10536d9feee27d20b8022ff4fde8000a2cbb3a38;p=c11tester.git

diff --git a/model.cc b/model.cc
index c5e41ab7..8267377f 100644
--- a/model.cc
+++ b/model.cc
@@ -47,6 +47,10 @@ ModelChecker::ModelChecker(struct model_params params) :
 	priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
 	/* First thread created will have id INITIAL_THREAD_ID */
 	priv->next_thread_id = INITIAL_THREAD_ID;
+
+	/* Initialize a model-checker thread, for special ModelActions */
+	model_thread = new Thread(get_next_id());
+	thread_map->put(id_to_int(model_thread->get_id()), model_thread);
 }
 
 /** @brief Destructor */
@@ -572,6 +576,16 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 	ASSERT(release->same_thread(rf));
 
 	if (write == NULL) {
+		/**
+		 * @todo Forcing a synchronization requires that we set
+		 * modification order constraints. For instance, we can't allow
+		 * a fixup sequence in which two separate read-acquire
+		 * operations read from the same sequence, where the first one
+		 * synchronizes and the other doesn't. Essentially, we can't
+		 * allow any writes to insert themselves between 'release' and
+		 * 'rf'
+		 */
+
 		/* Must synchronize */
 		if (!acquire->synchronize_with(release)) {
 			set_bad_synchronization();
@@ -598,6 +612,10 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 		mo_graph->addEdge(release, write);
 		mo_graph->addEdge(write, rf);
 	}
+
+	/* See if we have realized a data race */
+	if (checkDataRaces())
+		set_assert();
 }
 
 /**
@@ -1330,6 +1348,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 				th->is_complete())
 			future_ordered = true;
 
+		ASSERT(!th->is_model_thread() || future_ordered);
+
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			const ModelAction *act = *rit;
 			/* Reach synchronization -> this thread is complete */
@@ -1944,7 +1964,7 @@ bool ModelChecker::take_step() {
 	if (has_asserted())
 		return false;
 
-	Thread *curr = thread_current();
+	Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
 	if (curr) {
 		if (curr->get_state() == THREAD_READY) {
 			ASSERT(priv->current_action);
@@ -1967,6 +1987,26 @@ bool ModelChecker::take_step() {
 	DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
 			next ? id_to_int(next->get_id()) : -1);
 
+	/*
+	 * Launch end-of-execution release sequence fixups only when there are:
+	 *
+	 * (1) no more user threads to run (or when execution replay chooses
+	 *     the 'model_thread')
+	 * (2) pending release sequences
+	 * (3) pending assertions (i.e., data races)
+	 * (4) no pending promises
+	 */
+	if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
+			isfinalfeasible() && !unrealizedraces.empty()) {
+		printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+				pending_rel_seqs->size());
+		ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
+				std::memory_order_seq_cst, NULL, VALUE_NONE,
+				model_thread);
+		set_current_action(fixup);
+		return true;
+	}
+
 	/* next == NULL -> don't take any more steps */
 	if (!next)
 		return false;