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

diff --git a/model.cc b/model.cc
index c9353db7..8267377f 100644
--- a/model.cc
+++ b/model.cc
@@ -12,6 +12,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "mutex.h"
+#include "threads.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -33,7 +34,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
 	promises(new std::vector<Promise *>()),
 	futurevalues(new std::vector<struct PendingFutureValue>()),
-	pending_acq_rel_seq(new std::vector<ModelAction *>()),
+	pending_rel_seqs(new std::vector<struct release_seq *>()),
 	thrd_last_action(new std::vector<ModelAction *>(1)),
 	node_stack(new NodeStack()),
 	mo_graph(new CycleGraph()),
@@ -46,12 +47,16 @@ 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 */
 ModelChecker::~ModelChecker()
 {
-	for (int i = 0; i < get_num_threads(); i++)
+	for (unsigned int i = 0; i < get_num_threads(); i++)
 		delete thread_map->get(i);
 	delete thread_map;
 
@@ -64,7 +69,7 @@ ModelChecker::~ModelChecker()
 		delete (*promises)[i];
 	delete promises;
 
-	delete pending_acq_rel_seq;
+	delete pending_rel_seqs;
 
 	delete thrd_last_action;
 	delete node_stack;
@@ -94,11 +99,17 @@ thread_id_t ModelChecker::get_next_id()
 }
 
 /** @return the number of user threads created during this execution */
-int ModelChecker::get_num_threads()
+unsigned int ModelChecker::get_num_threads()
 {
 	return priv->next_thread_id;
 }
 
+/** @return The currently executing Thread. */
+Thread * ModelChecker::get_current_thread()
+{
+	return scheduler->get_current_thread();
+}
+
 /** @return a sequence number for a new ModelAction */
 modelclock_t ModelChecker::get_next_seq_num()
 {
@@ -156,6 +167,10 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			/* The next node will try to read from a different future value. */
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
+		} else if (nextnode->increment_relseq_break()) {
+			/* The next node will try to resolve a release sequence differently */
+			tid = next->get_tid();
+			node_stack->pop_restofstack(2);
 		} else {
 			/* Make a different thread execute for next step */
 			Node *node = nextnode->get_parent();
@@ -171,7 +186,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 	} else {
 		tid = next->get_tid();
 	}
-	DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
+	DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
 	ASSERT(tid != THREAD_ID_T_NONE);
 	return thread_map->get(id_to_int(tid));
 }
@@ -192,7 +207,7 @@ bool ModelChecker::next_execution()
 	if (isfinalfeasible()) {
 		printf("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
-			earliest_diverge->print(false);
+			earliest_diverge->print();
 		else
 			printf("(Not set)\n");
 
@@ -200,8 +215,8 @@ bool ModelChecker::next_execution()
 		num_feasible_executions++;
 	}
 
-	DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
-			pending_acq_rel_seq->size());
+	DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
+			pending_rel_seqs->size());
 
 	if (isfinalfeasible() || DBG_ENABLED())
 		print_summary();
@@ -229,7 +244,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
-			if (act->is_synchronizing(prev))
+			if (prev->could_synchronize_with(act))
 				return prev;
 		}
 		break;
@@ -317,7 +332,8 @@ void ModelChecker::set_backtracking(ModelAction *act)
 		if (!node->set_backtrack(tid))
 			continue;
 		DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-					prev->get_tid(), t->get_id());
+					id_to_int(prev->get_tid()),
+					id_to_int(t->get_id()));
 		if (DBG_ENABLED()) {
 			prev->print();
 			act->print();
@@ -369,6 +385,8 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 
 			curr->read_from(reads_from);
 			mo_graph->commitChanges();
+			mo_check_promises(curr->get_tid(), reads_from);
+
 			updated |= r_status;
 		} else if (!second_part_of_rmw) {
 			/* Read from future value */
@@ -466,6 +484,8 @@ bool ModelChecker::process_write(ModelAction *curr)
 	}
 
 	mo_graph->commitChanges();
+	mo_check_promises(curr->get_tid(), curr);
+
 	get_thread(curr)->set_return_value(VALUE_NONE);
 	return updated_mod_order || updated_promises;
 }
@@ -518,7 +538,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		break;
 	}
 	case THREAD_START: {
-		check_promises(NULL, curr->get_cv());
+		check_promises(curr->get_tid(), NULL, curr->get_cv());
 		break;
 	}
 	default:
@@ -528,6 +548,76 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 	return updated;
 }
 
+/**
+ * @brief Process the current action for release sequence fixup activity
+ *
+ * Performs model-checker release sequence fixups for the current action,
+ * forcing a single pending release sequence to break (with a given, potential
+ * "loose" write) or to complete (i.e., synchronize). If a pending release
+ * sequence forms a complete release sequence, then we must perform the fixup
+ * synchronization, mo_graph additions, etc.
+ *
+ * @param curr The current action; must be a release sequence fixup action
+ * @param work_queue The work queue to which to add work items as they are
+ * generated
+ */
+void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
+{
+	const ModelAction *write = curr->get_node()->get_relseq_break();
+	struct release_seq *sequence = pending_rel_seqs->back();
+	pending_rel_seqs->pop_back();
+	ASSERT(sequence);
+	ModelAction *acquire = sequence->acquire;
+	const ModelAction *rf = sequence->rf;
+	const ModelAction *release = sequence->release;
+	ASSERT(acquire);
+	ASSERT(release);
+	ASSERT(rf);
+	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();
+			return;
+		}
+		/* Re-check all pending release sequences */
+		work_queue->push_back(CheckRelSeqWorkEntry(NULL));
+		/* Re-check act for mo_graph edges */
+		work_queue->push_back(MOEdgeWorkEntry(acquire));
+
+		/* propagate synchronization to later actions */
+		action_list_t::reverse_iterator rit = action_trace->rbegin();
+		for (; (*rit) != acquire; rit++) {
+			ModelAction *propagate = *rit;
+			if (acquire->happens_before(propagate)) {
+				propagate->synchronize_with(acquire);
+				/* Re-check 'propagate' for mo_graph edges */
+				work_queue->push_back(MOEdgeWorkEntry(propagate));
+			}
+		}
+	} else {
+		/* Break release sequence with new edges:
+		 *   release --mo--> write --mo--> rf */
+		mo_graph->addEdge(release, write);
+		mo_graph->addEdge(write, rf);
+	}
+
+	/* See if we have realized a data race */
+	if (checkDataRaces())
+		set_assert();
+}
+
 /**
  * Initialize the current action by performing one or more of the following
  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
@@ -579,6 +669,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		 */
 		if (newcurr->is_write())
 			compute_promises(newcurr);
+		else if (newcurr->is_relseq_fixup())
+			compute_relseq_breakwrites(newcurr);
 	}
 	return newcurr;
 }
@@ -666,6 +758,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			if (act->is_mutex_op() && process_mutex(act))
 				update_all = true;
 
+			if (act->is_relseq_fixup())
+				process_relseq_fixup(curr, &work_queue);
+
 			if (update_all)
 				work_queue.push_back(CheckRelSeqWorkEntry(NULL));
 			else if (update)
@@ -728,7 +823,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
 	if ((!parnode->backtrack_empty() ||
 			 !currnode->read_from_empty() ||
 			 !currnode->future_value_empty() ||
-			 !currnode->promise_empty())
+			 !currnode->promise_empty() ||
+			 !currnode->relseq_break_empty())
 			&& (!priv->next_backtrack ||
 					*curr > *priv->next_backtrack)) {
 		priv->next_backtrack = curr;
@@ -748,7 +844,7 @@ bool ModelChecker::promises_expired() {
 /** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
-	return promises->size() == 0 && pending_acq_rel_seq->size() == 0;
+	return promises->size() == 0 && pending_rel_seqs->size() == 0;
 }
 
 /** @return whether the current partial trace is feasible. */
@@ -787,8 +883,7 @@ bool ModelChecker::isfinalfeasible() {
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
-	int tid = id_to_int(act->get_tid());
-	ModelAction *lastread = get_last_action(tid);
+	ModelAction *lastread = get_last_action(act->get_tid());
 	lastread->process_rmw(act);
 	if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
 		mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
@@ -1103,7 +1198,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				}
 				added = true;
 				break;
-			} else if (act->is_read() && !act->is_synchronizing(curr) &&
+			} else if (act->is_read() && !act->could_synchronize_with(curr) &&
 			                             !act->same_thread(curr)) {
 				/* We have an action that:
 				   (1) did not happen before us
@@ -1163,13 +1258,19 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * @todo Finish lazy updating, when promises are fulfilled in the future
  * @param rf The action that might be part of a release sequence. Must be a
  * write.
- * @param release_heads A pass-by-reference style return parameter.  After
+ * @param release_heads A pass-by-reference style return parameter. After
  * execution of this function, release_heads will contain the heads of all the
- * relevant release sequences, if any exists
+ * relevant release sequences, if any exists with certainty
+ * @param pending A pass-by-reference style return parameter which is only used
+ * when returning false (i.e., uncertain). Returns most information regarding
+ * an uncertain release sequence, including any write operations that might
+ * break the sequence.
  * @return true, if the ModelChecker is certain that release_heads is complete;
  * false otherwise
  */
-bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
+bool ModelChecker::release_seq_heads(const ModelAction *rf,
+		rel_heads_list_t *release_heads,
+		struct release_seq *pending) const
 {
 	/* Only check for release sequences if there are no cycles */
 	if (mo_graph->checkForCycles())
@@ -1198,6 +1299,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 	};
 	if (!rf) {
 		/* read from future: need to settle this later */
+		pending->rf = NULL;
 		return false; /* incomplete */
 	}
 
@@ -1227,6 +1329,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 
 	ASSERT(rf->same_thread(release));
 
+	pending->writes.clear();
+
 	bool certain = true;
 	for (unsigned int i = 0; i < thrd_lists->size(); i++) {
 		if (id_to_int(rf->get_tid()) == (int)i)
@@ -1238,10 +1342,14 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 		bool future_ordered = false;
 
 		ModelAction *last = get_last_action(int_to_id(i));
-		if (last && (rf->happens_before(last) ||
-				last->get_type() == THREAD_FINISH))
+		Thread *th = get_thread(int_to_id(i));
+		if ((last && rf->happens_before(last)) ||
+				!scheduler->is_enabled(th) ||
+				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 */
@@ -1270,14 +1378,21 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 				/* release --mo-> act --mo--> rf */
 				return true; /* complete */
 			}
+			/* act may break release sequence */
+			pending->writes.push_back(act);
 			certain = false;
 		}
 		if (!future_ordered)
-			return false; /* This thread is uncertain */
+			certain = false; /* This thread is uncertain */
 	}
 
-	if (certain)
+	if (certain) {
 		release_heads->push_back(release);
+		pending->writes.clear();
+	} else {
+		pending->release = release;
+		pending->rf = rf;
+	}
 	return certain;
 }
 
@@ -1291,16 +1406,19 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
  * @param act The 'acquire' action that may read from a release sequence
  * @param release_heads A pass-by-reference return parameter. Will be filled
  * with the head(s) of the release sequence(s), if they exists with certainty.
- * @see ModelChecker::release_seq_head
+ * @see ModelChecker::release_seq_heads
  */
 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
 {
 	const ModelAction *rf = act->get_reads_from();
-	bool complete;
-	complete = release_seq_head(rf, release_heads);
-	if (!complete) {
+	struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
+	sequence->acquire = act;
+
+	if (!release_seq_heads(rf, release_heads, sequence)) {
 		/* add act to 'lazy checking' list */
-		pending_acq_rel_seq->push_back(act);
+		pending_rel_seqs->push_back(sequence);
+	} else {
+		snapshot_free(sequence);
 	}
 }
 
@@ -1320,9 +1438,10 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
 {
 	bool updated = false;
-	std::vector<ModelAction *>::iterator it = pending_acq_rel_seq->begin();
-	while (it != pending_acq_rel_seq->end()) {
-		ModelAction *act = *it;
+	std::vector<struct release_seq *>::iterator it = pending_rel_seqs->begin();
+	while (it != pending_rel_seqs->end()) {
+		struct release_seq *pending = *it;
+		ModelAction *act = pending->acquire;
 
 		/* Only resolve sequences on the given location, if provided */
 		if (location && act->get_location() != location) {
@@ -1333,7 +1452,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 		const ModelAction *rf = act->get_reads_from();
 		rel_heads_list_t release_heads;
 		bool complete;
-		complete = release_seq_head(rf, &release_heads);
+		complete = release_seq_heads(rf, &release_heads, pending);
 		for (unsigned int i = 0; i < release_heads.size(); i++) {
 			if (!act->has_synchronized_with(release_heads[i])) {
 				if (act->synchronize_with(release_heads[i]))
@@ -1360,10 +1479,12 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 				}
 			}
 		}
-		if (complete)
-			it = pending_acq_rel_seq->erase(it);
-		else
+		if (complete) {
+			it = pending_rel_seqs->erase(it);
+			snapshot_free(pending);
+		} else {
 			it++;
+		}
 	}
 
 	// If we resolved promises or data races, see if we have realized a data race.
@@ -1479,6 +1600,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid)
 bool ModelChecker::resolve_promises(ModelAction *write)
 {
 	bool resolved = false;
+  std::vector<thread_id_t> threads_to_check;
 
 	for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
 		Promise *promise = (*promises)[promise_index];
@@ -1496,13 +1618,22 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			post_r_modification_order(read, write);
 			//Make sure the promise's value matches the write's value
 			ASSERT(promise->get_value() == write->get_value());
-
 			delete(promise);
+			
 			promises->erase(promises->begin() + promise_index);
+			threads_to_check.push_back(read->get_tid());
+
 			resolved = true;
 		} else
 			promise_index++;
 	}
+
+	//Check whether reading these writes has made threads unable to
+	//resolve promises
+
+	for(unsigned int i=0;i<threads_to_check.size();i++)
+		mo_check_promises(threads_to_check[i], write);
+
 	return resolved;
 }
 
@@ -1519,7 +1650,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
 		const ModelAction *act = promise->get_action();
 		if (!act->happens_before(curr) &&
 				act->is_read() &&
-				!act->is_synchronizing(curr) &&
+				!act->could_synchronize_with(curr) &&
 				!act->same_thread(curr) &&
 				promise->get_value() == curr->get_value()) {
 			curr->get_node()->set_promise(i);
@@ -1528,16 +1659,14 @@ void ModelChecker::compute_promises(ModelAction *curr)
 }
 
 /** Checks promises in response to change in ClockVector Threads. */
-void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
+void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
 {
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
 		const ModelAction *act = promise->get_action();
 		if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
 				merge_cv->synchronized_since(act)) {
-			//This thread is no longer able to send values back to satisfy the promise
-			int num_synchronized_threads = promise->increment_threads();
-			if (num_synchronized_threads == get_num_threads()) {
+			if (promise->increment_threads(tid)) {
 				//Promise has failed
 				failed_promise = true;
 				return;
@@ -1546,6 +1675,92 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
 	}
 }
 
+/** Checks promises in response to addition to modification order for threads.
+ * Definitions:
+ * pthread is the thread that performed the read that created the promise
+ * 
+ * pread is the read that created the promise
+ *
+ * pwrite is either the first write to same location as pread by
+ * pthread that is sequenced after pread or the value read by the
+ * first read to the same lcoation as pread by pthread that is
+ * sequenced after pread..
+ *
+ *	1. If tid=pthread, then we check what other threads are reachable
+ * through the mode order starting with pwrite.  Those threads cannot
+ * perform a write that will resolve the promise due to modification
+ * order constraints.
+ *
+ * 2. If the tid is not pthread, we check whether pwrite can reach the
+ * action write through the modification order.  If so, that thread
+ * cannot perform a future write that will resolve the promise due to
+ * modificatin order constraints.
+ *
+ *	@parem tid The thread that either read from the model action
+ *	write, or actually did the model action write.
+ *
+ *	@parem write The ModelAction representing the relevant write.
+ */
+
+void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
+	void * location = write->get_location();
+	for (unsigned int i = 0; i < promises->size(); i++) {
+		Promise *promise = (*promises)[i];
+		const ModelAction *act = promise->get_action();
+		
+		//Is this promise on the same location?
+		if ( act->get_location() != location )
+			continue;
+
+		//same thread as the promise
+		if ( act->get_tid()==tid ) {
+
+			//do we have a pwrite for the promise, if not, set it
+			if (promise->get_write() == NULL ) {
+				promise->set_write(write);
+			}
+			if (mo_graph->checkPromise(write, promise)) {
+				failed_promise = true;
+				return;
+			}
+		}
+		
+		//Don't do any lookups twice for the same thread
+		if (promise->has_sync_thread(tid))
+			continue;
+		
+		if (mo_graph->checkReachable(promise->get_write(), write)) {
+			if (promise->increment_threads(tid)) {
+				failed_promise = true;
+				return;
+			}
+		}
+	}
+}
+
+/**
+ * Compute the set of writes that may break the current pending release
+ * sequence. This information is extracted from previou release sequence
+ * calculations.
+ *
+ * @param curr The current ModelAction. Must be a release sequence fixup
+ * action.
+ */
+void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
+{
+	if (pending_rel_seqs->empty())
+		return;
+
+	struct release_seq *pending = pending_rel_seqs->back();
+	for (unsigned int i = 0; i < pending->writes.size(); i++) {
+		const ModelAction *write = pending->writes[i];
+		curr->get_node()->add_relseq_break(write);
+	}
+
+	/* NULL means don't break the sequence; just synchronize */
+	curr->get_node()->add_relseq_break(NULL);
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from. This set is determined by the clock vector's "happens before"
@@ -1701,12 +1916,35 @@ void ModelChecker::remove_thread(Thread *t)
 	scheduler->remove_thread(t);
 }
 
+/**
+ * @brief Get a Thread reference by its ID
+ * @param tid The Thread's ID
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(thread_id_t tid) const
+{
+	return thread_map->get(id_to_int(tid));
+}
+
+/**
+ * @brief Get a reference to the Thread in which a ModelAction was executed
+ * @param act The ModelAction
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(ModelAction *act) const
+{
+	return get_thread(act->get_tid());
+}
+
 /**
  * Switch from a user-context to the "master thread" context (a.k.a. system
  * context). This switch is made with the intention of exploring a particular
  * model-checking action (described by a ModelAction object). Must be called
  * from a user-thread context.
- * @param act The current action that will be explored. Must not be NULL.
+ *
+ * @param act The current action that will be explored. May be NULL only if
+ * trace is exiting via an assertion (see ModelChecker::set_assert and
+ * ModelChecker::has_asserted).
  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
  */
 int ModelChecker::switch_to_master(ModelAction *act)
@@ -1726,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);
@@ -1740,22 +1978,43 @@ bool ModelChecker::take_step() {
 			ASSERT(false);
 		}
 	}
-	Thread * next = scheduler->next_thread(priv->nextThread);
+	Thread *next = scheduler->next_thread(priv->nextThread);
 
 	/* Infeasible -> don't take any more steps */
 	if (!isfeasible())
 		return false;
 
-	if (next)
-		next->set_state(THREAD_RUNNING);
-	DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+	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;
 
-	if ( next->get_pending() != NULL ) {
-		//restart a pending action
+	next->set_state(THREAD_RUNNING);
+
+	if (next->get_pending() != NULL) {
+		/* restart a pending action */
 		set_current_action(next->get_pending());
 		next->set_pending(NULL);
 		next->set_state(THREAD_READY);