X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=e6df37f8372949f610057599181402ddf673ce84;hb=ceac3a2484741a39bcb00f8593514f65be8bbe85;hp=e36426721ca44b53b7029cedb7de53ee79b22634;hpb=b35625b0499717b3caab5344d7278a31fbee9cb6;p=model-checker.git

diff --git a/model.cc b/model.cc
index e364267..e6df37f 100644
--- a/model.cc
+++ b/model.cc
@@ -43,7 +43,6 @@ struct model_snapshot_members {
 		/* First thread created will have id INITIAL_THREAD_ID */
 		next_thread_id(INITIAL_THREAD_ID),
 		used_sequence_numbers(0),
-		nextThread(NULL),
 		next_backtrack(NULL),
 		bugs(),
 		stats(),
@@ -62,7 +61,6 @@ struct model_snapshot_members {
 	ModelAction *current_action;
 	unsigned int next_thread_id;
 	modelclock_t used_sequence_numbers;
-	Thread *nextThread;
 	ModelAction *next_backtrack;
 	std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
 	struct execution_stats stats;
@@ -161,7 +159,7 @@ void ModelChecker::reset_to_initial_state()
 	/* Print all model-checker output before rollback */
 	fflush(model_out);
 
-	snapshotObject->backTrackBeforeStep(0);
+	snapshot_backtrack_before(0);
 }
 
 /** @return a thread ID for a new Thread */
@@ -176,7 +174,12 @@ unsigned int ModelChecker::get_num_threads() const
 	return priv->next_thread_id;
 }
 
-/** @return The currently executing Thread. */
+/**
+ * Must be called from user-thread context (e.g., through the global
+ * thread_current() interface)
+ *
+ * @return The currently executing Thread.
+ */
 Thread * ModelChecker::get_current_thread() const
 {
 	return scheduler->get_current_thread();
@@ -214,9 +217,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 		/* Do not split atomic actions. */
 		if (curr->is_rmwr())
 			return thread_current();
-		/* The THREAD_CREATE action points to the created Thread */
 		else if (curr->get_type() == THREAD_CREATE)
-			return (Thread *)curr->get_location();
+			return curr->get_thread_operand();
 	}
 
 	/* Have we completed exploring the preselected path? */
@@ -228,7 +230,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 
 	if (next == diverge) {
 		if (earliest_diverge == NULL || *diverge < *earliest_diverge)
-			earliest_diverge=diverge;
+			earliest_diverge = diverge;
 
 		Node *nextnode = next->get_node();
 		Node *prevnode = nextnode->get_parent();
@@ -256,13 +258,14 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
 		} else {
+			ASSERT(prevnode);
 			/* Make a different thread execute for next step */
-			scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
+			scheduler->add_sleep(get_thread(next->get_tid()));
 			tid = prevnode->get_next_backtrack();
 			/* Make sure the backtracked thread isn't sleeping. */
 			node_stack->pop_restofstack(1);
-			if (diverge==earliest_diverge) {
-				earliest_diverge=prevnode->get_action();
+			if (diverge == earliest_diverge) {
+				earliest_diverge = prevnode->get_action();
 			}
 		}
 		/* The correct sleep set is in the parent node. */
@@ -298,7 +301,6 @@ void ModelChecker::execute_sleep_set()
 			thr->set_pending(priv->current_action);
 		}
 	}
-	priv->current_action = NULL;
 }
 
 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
@@ -502,7 +504,7 @@ bool ModelChecker::next_execution()
 	record_stats();
 
 	/* Output */
-	if (DBG_ENABLED() || params.verbose || have_bug_reports())
+	if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
 		print_execution(complete);
 	else
 		clear_program_output();
@@ -560,7 +562,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->same_thread(prev)&&prev->is_failed_trylock())
+			if (!act->same_thread(prev) && prev->is_failed_trylock())
 				return prev;
 		}
 		break;
@@ -571,9 +573,9 @@ 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->same_thread(prev)&&prev->is_failed_trylock())
+			if (!act->same_thread(prev) && prev->is_failed_trylock())
 				return prev;
-			if (!act->same_thread(prev)&&prev->is_notify())
+			if (!act->same_thread(prev) && prev->is_notify())
 				return prev;
 		}
 		break;
@@ -586,7 +588,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->same_thread(prev)&&prev->is_wait())
+			if (!act->same_thread(prev) && prev->is_wait())
 				return prev;
 		}
 		break;
@@ -612,15 +614,15 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	Node *node = prev->get_node()->get_parent();
 
 	int low_tid, high_tid;
-	if (node->is_enabled(t)) {
+	if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
 		low_tid = id_to_int(act->get_tid());
-		high_tid = low_tid+1;
+		high_tid = low_tid + 1;
 	} else {
 		low_tid = 0;
 		high_tid = get_num_threads();
 	}
 
-	for(int i = low_tid; i < high_tid; i++) {
+	for (int i = low_tid; i < high_tid; i++) {
 		thread_id_t tid = int_to_id(i);
 
 		/* Make sure this thread can be enabled here. */
@@ -628,7 +630,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 			break;
 
 		/* Don't backtrack into a point where the thread is disabled or sleeping. */
-		if (node->enabled_status(tid)!=THREAD_ENABLED)
+		if (node->enabled_status(tid) != THREAD_ENABLED)
 			continue;
 
 		/* Check if this has been explored already */
@@ -637,11 +639,11 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
 		/* See if fairness allows */
 		if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
-			bool unfair=false;
-			for(int t=0;t<node->get_num_threads();t++) {
-				thread_id_t tother=int_to_id(t);
+			bool unfair = false;
+			for (int t = 0; t < node->get_num_threads(); t++) {
+				thread_id_t tother = int_to_id(t);
 				if (node->is_enabled(tother) && node->has_priority(tother)) {
-					unfair=true;
+					unfair = true;
 					break;
 				}
 			}
@@ -649,8 +651,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 				continue;
 		}
 		/* Cache the latest backtracking point */
-		if (!priv->next_backtrack || *prev > *priv->next_backtrack)
-			priv->next_backtrack = prev;
+		set_latest_backtrack(prev);
 
 		/* If this is a new backtracking point, mark the tree */
 		if (!node->set_backtrack(tid))
@@ -665,6 +666,26 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	}
 }
 
+/**
+ * @brief Cache the a backtracking point as the "most recent", if eligible
+ *
+ * Note that this does not prepare the NodeStack for this backtracking
+ * operation, it only caches the action on a per-execution basis
+ *
+ * @param act The operation at which we should explore a different next action
+ * (i.e., backtracking point)
+ * @return True, if this action is now the most recent backtracking point;
+ * false otherwise
+ */
+bool ModelChecker::set_latest_backtrack(ModelAction *act)
+{
+	if (!priv->next_backtrack || *act > *priv->next_backtrack) {
+		priv->next_backtrack = act;
+		return true;
+	}
+	return false;
+}
+
 /**
  * Returns last backtracking point. The model checker will explore a different
  * path for this point in the next execution.
@@ -701,7 +722,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 			}
 
 
-			if (!second_part_of_rmw&&is_infeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
+			if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
 				mo_graph->rollbackChanges();
 				priv->too_many_reads = false;
 				continue;
@@ -741,14 +762,15 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
  *
  * @return True if synchronization was updated; false otherwise
  */
-bool ModelChecker::process_mutex(ModelAction *curr) {
-	std::mutex *mutex=NULL;
-	struct std::mutex_state *state=NULL;
+bool ModelChecker::process_mutex(ModelAction *curr)
+{
+	std::mutex *mutex = NULL;
+	struct std::mutex_state *state = NULL;
 
 	if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
 		mutex = (std::mutex *)curr->get_location();
 		state = mutex->get_state();
-	} else if(curr->is_wait()) {
+	} else if (curr->is_wait()) {
 		mutex = (std::mutex *)curr->get_value();
 		state = mutex->get_state();
 	}
@@ -799,10 +821,10 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 		}
 		waiters->clear();
 		//check whether we should go to sleep or not...simulate spurious failures
-		if (curr->get_node()->get_misc()==0) {
+		if (curr->get_node()->get_misc() == 0) {
 			get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
 			//disable us
-			scheduler->sleep(get_current_thread());
+			scheduler->sleep(get_thread(curr));
 		}
 		break;
 	}
@@ -817,7 +839,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 	}
 	case ATOMIC_NOTIFY_ONE: {
 		action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
-		int wakeupthread=curr->get_node()->get_misc();
+		int wakeupthread = curr->get_node()->get_misc();
 		action_list_t::iterator it = waiters->begin();
 		advance(it, wakeupthread);
 		scheduler->wake(get_thread(*it));
@@ -831,6 +853,15 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 	return false;
 }
 
+void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
+{
+	/* Do more ambitious checks now that mo is more complete */
+	if (mo_may_allow(writer, reader) &&
+			reader->get_node()->add_future_value(writer->get_value(),
+				writer->get_seq_number() + params.maxfuturedelay))
+		set_latest_backtrack(reader);
+}
+
 /**
  * Process a write ModelAction
  * @param curr The ModelAction to process
@@ -844,13 +875,9 @@ bool ModelChecker::process_write(ModelAction *curr)
 	if (promises->size() == 0) {
 		for (unsigned int i = 0; i < futurevalues->size(); i++) {
 			struct PendingFutureValue pfv = (*futurevalues)[i];
-			//Do more ambitious checks now that mo is more complete
-			if (mo_may_allow(pfv.writer, pfv.act)&&
-					pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
-					(!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
-				priv->next_backtrack = pfv.act;
+			add_future_value(pfv.writer, pfv.act);
 		}
-		futurevalues->resize(0);
+		futurevalues->clear();
 	}
 
 	mo_graph->commitChanges();
@@ -927,12 +954,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 
 	switch (curr->get_type()) {
 	case THREAD_CREATE: {
-		Thread *th = (Thread *)curr->get_location();
+		Thread *th = curr->get_thread_operand();
 		th->set_creation(curr);
 		break;
 	}
 	case THREAD_JOIN: {
-		Thread *blocking = (Thread *)curr->get_location();
+		Thread *blocking = curr->get_thread_operand();
 		ModelAction *act = get_last_action(blocking->get_id());
 		curr->synchronize_with(act);
 		updated = true; /* trigger rel-seq checks */
@@ -1175,11 +1202,10 @@ void ModelChecker::set_current_action(ModelAction *act) {
  * execution when running permutations of previously-observed executions.
  *
  * @param curr The current action to process
- * @return The next Thread that must be executed. May be NULL if ModelChecker
- * makes no choice (e.g., according to replay execution, combining RMW actions,
- * etc.)
+ * @return The ModelAction that is actually executed; may be different than
+ * curr; may be NULL, if the current action is not enabled to run
  */
-Thread * ModelChecker::check_current_action(ModelAction *curr)
+ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 {
 	ASSERT(curr);
 	bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
@@ -1187,13 +1213,17 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	if (!check_action_enabled(curr)) {
 		/* Make the execution look like we chose to run this action
 		 * much later, when a lock/join can succeed */
-		get_current_thread()->set_pending(curr);
-		scheduler->sleep(get_current_thread());
-		return get_next_thread(NULL);
+		get_thread(curr)->set_pending(curr);
+		scheduler->sleep(get_thread(curr));
+		return NULL;
 	}
 
 	bool newly_explored = initialize_curr_action(&curr);
 
+	DBG();
+	if (DBG_ENABLED())
+		curr->print();
+
 	wake_up_sleeping_actions(curr);
 
 	/* Add the action to lists before any other model-checking tasks */
@@ -1271,7 +1301,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	check_curr_backtracking(curr);
 	set_backtracking(curr);
-	return get_next_thread(curr);
+	return curr;
 }
 
 void ModelChecker::check_curr_backtracking(ModelAction *curr)
@@ -1279,25 +1309,22 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
 
-	if ((!parnode->backtrack_empty() ||
+	if ((parnode && !parnode->backtrack_empty()) ||
 			 !currnode->misc_empty() ||
 			 !currnode->read_from_empty() ||
 			 !currnode->future_value_empty() ||
 			 !currnode->promise_empty() ||
-			 !currnode->relseq_break_empty())
-			&& (!priv->next_backtrack ||
-					*curr > *priv->next_backtrack)) {
-		priv->next_backtrack = curr;
+			 !currnode->relseq_break_empty()) {
+		set_latest_backtrack(curr);
 	}
 }
 
 bool ModelChecker::promises_expired() const
 {
-	for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
-		Promise *promise = (*promises)[promise_index];
-		if (promise->get_expiration()<priv->used_sequence_numbers) {
+	for (unsigned int i = 0; i < promises->size(); i++) {
+		Promise *promise = (*promises)[i];
+		if (promise->get_expiration() < priv->used_sequence_numbers)
 			return true;
-		}
 	}
 	return false;
 }
@@ -1312,15 +1339,39 @@ bool ModelChecker::isfeasibleprefix() const
 	return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
 }
 
+/**
+ * Print disagnostic information about an infeasible execution
+ * @param prefix A string to prefix the output with; if NULL, then a default
+ * message prefix will be provided
+ */
+void ModelChecker::print_infeasibility(const char *prefix) const
+{
+	char buf[100];
+	char *ptr = buf;
+	if (mo_graph->checkForRMWViolation())
+		ptr += sprintf(ptr, "[RMW atomicity]");
+	if (mo_graph->checkForCycles())
+		ptr += sprintf(ptr, "[mo cycle]");
+	if (priv->failed_promise)
+		ptr += sprintf(ptr, "[failed promise]");
+	if (priv->too_many_reads)
+		ptr += sprintf(ptr, "[too many reads]");
+	if (priv->bad_synchronization)
+		ptr += sprintf(ptr, "[bad sw ordering]");
+	if (promises_expired())
+		ptr += sprintf(ptr, "[promise expired]");
+	if (promises->size() != 0)
+		ptr += sprintf(ptr, "[unresolved promise]");
+	if (ptr != buf)
+		model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
+}
+
 /**
  * Returns whether the current completed trace is feasible, except for pending
  * release sequences.
  */
 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
 {
-	if (DBG_ENABLED() && promises->size() != 0)
-		DEBUG("Infeasible: unrevolved promises\n");
-
 	return !is_infeasible() && promises->size() == 0;
 }
 
@@ -1332,9 +1383,6 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-	if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
-		DEBUG("Infeasible: RMW violation\n");
-
 	return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
 }
 
@@ -1348,18 +1396,6 @@ bool ModelChecker::is_infeasible() const
  * */
 bool ModelChecker::is_infeasible_ignoreRMW() const
 {
-	if (DBG_ENABLED()) {
-		if (mo_graph->checkForCycles())
-			DEBUG("Infeasible: modification order cycles\n");
-		if (priv->failed_promise)
-			DEBUG("Infeasible: failed promise\n");
-		if (priv->too_many_reads)
-			DEBUG("Infeasible: too many reads\n");
-		if (priv->bad_synchronization)
-			DEBUG("Infeasible: bad synchronization ordering\n");
-		if (promises_expired())
-			DEBUG("Infeasible: promises expired\n");
-	}
 	return mo_graph->checkForCycles() || priv->failed_promise ||
 		priv->too_many_reads || priv->bad_synchronization ||
 		promises_expired();
@@ -1369,7 +1405,7 @@ bool ModelChecker::is_infeasible_ignoreRMW() const
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 	ModelAction *lastread = get_last_action(act->get_tid());
 	lastread->process_rmw(act);
-	if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
+	if (act->is_rmw() && lastread->get_reads_from() != NULL) {
 		mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
 		mo_graph->commitChanges();
 	}
@@ -1414,7 +1450,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 		action_list_t::reverse_iterator ritcopy = rit;
 		//See if we have enough reads from the same value
 		int count = 0;
-		for (; count < params.maxreads; rit++,count++) {
+		for (; count < params.maxreads; rit++, count++) {
 			if (rit == list->rend())
 				return;
 			ModelAction *act = *rit;
@@ -1434,7 +1470,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 			if (write == rf)
 				continue;
 
-			/* Test to see whether this is a feasible write to read from*/
+			/* Test to see whether this is a feasible write to read from */
 			mo_graph->startChanges();
 			r_modification_order(curr, write);
 			bool feasiblereadfrom = !is_infeasible();
@@ -1447,11 +1483,11 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 			bool feasiblewrite = true;
 			//new we need to see if this write works for everyone
 
-			for (int loop = count; loop>0; loop--,rit++) {
+			for (int loop = count; loop > 0; loop--, rit++) {
 				ModelAction *act = *rit;
 				bool foundvalue = false;
-				for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
-					if (act->get_node()->get_read_from_at(j)==write) {
+				for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
+					if (act->get_node()->get_read_from_at(j) == write) {
 						foundvalue = true;
 						break;
 					}
@@ -1606,7 +1642,7 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
 
 			/* Include at most one act per-thread that "happens before" curr */
 		if (lastact != NULL) {
-			if (lastact==curr) {
+			if (lastact == curr) {
 				//Case 1: The resolved read is a RMW, and we need to make sure
 				//that the write portion of the RMW mod order after rf
 
@@ -1617,13 +1653,13 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
 				//is mod ordered after rf
 
 				const ModelAction *postreadfrom = lastact->get_reads_from();
-				if (postreadfrom != NULL&&rf != postreadfrom)
+				if (postreadfrom != NULL && rf != postreadfrom)
 					mo_graph->addEdge(rf, postreadfrom);
 			} else {
 				//Case 3: The resolved read is a normal read and the next
 				//operation is a write, and we need to make sure that the
 				//write is mod ordered after rf
-				if (lastact!=rf)
+				if (lastact != rf)
 					mo_graph->addEdge(rf, lastact);
 			}
 			break;
@@ -1698,7 +1734,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				 * continue processing list.
 				 */
 				if (curr->is_rmw()) {
-					if (curr->get_reads_from()!=NULL)
+					if (curr->get_reads_from() != NULL)
 						break;
 					else
 						continue;
@@ -1752,8 +1788,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				if (thin_air_constraint_may_allow(curr, act)) {
 					if (!is_infeasible() ||
 							(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
-						struct PendingFutureValue pfv = {curr,act};
-						futurevalues->push_back(pfv);
+						futurevalues->push_back(PendingFutureValue(curr, act));
 					}
 				}
 			}
@@ -1806,16 +1841,16 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *act = *rit;
 
-			if (!reader->happens_before(act))
+			/* Don't disallow due to act == reader */
+			if (!reader->happens_before(act) || reader == act)
 				break;
 			else if (act->is_write())
 				write_after_read = act;
-			else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
+			else if (act->is_read() && act->get_reads_from() != NULL)
 				write_after_read = act->get_reads_from();
-			}
 		}
 
-		if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
+		if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
 			return false;
 	}
 	return true;
@@ -2141,7 +2176,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 	}
 
 	if (act->is_wait()) {
-		void *mutex_loc=(void *) act->get_value();
+		void *mutex_loc = (void *) act->get_value();
 		get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
 
 		std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
@@ -2306,7 +2341,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 	//Check whether reading these writes has made threads unable to
 	//resolve promises
 
-	for(unsigned int i=0;i<threads_to_check.size();i++)
+	for (unsigned int i = 0; i < threads_to_check.size(); i++)
 		mo_check_promises(threads_to_check[i], write);
 
 	return resolved;
@@ -2395,14 +2430,14 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
 		const ModelAction *act = promise->get_action();
 
 		//Is this promise on the same location?
-		if ( act->get_location() != location )
+		if (act->get_location() != location)
 			continue;
 
 		//same thread as the promise
-		if ( act->get_tid()==tid ) {
+		if (act->get_tid() == tid) {
 
 			//do we have a pwrite for the promise, if not, set it
-			if (promise->get_write() == NULL ) {
+			if (promise->get_write() == NULL) {
 				promise->set_write(write);
 				//The pwrite cannot happen before the promise
 				if (write->happens_before(act) && (write != act)) {
@@ -2420,7 +2455,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
 		if (promise->has_sync_thread(tid))
 			continue;
 
-		if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
+		if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
 			if (promise->increment_threads(tid)) {
 				priv->failed_promise = true;
 				return;
@@ -2490,14 +2525,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 			else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
 				allow_read = false;
 
-			if (allow_read) {
-				DEBUG("Adding action to may_read_from:\n");
-				if (DBG_ENABLED()) {
-					act->print();
-					curr->print();
-				}
+			if (allow_read)
 				curr->get_node()->add_read_from(act);
-			}
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr))
@@ -2530,7 +2559,7 @@ bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *wri
 		}
 		if (write->get_reads_from() == NULL)
 			return true;
-		write=write->get_reads_from();
+		write = write->get_reads_from();
 	}
 }
 
@@ -2547,47 +2576,46 @@ ModelAction * ModelChecker::new_uninitialized_action(void *location) const
 	return act;
 }
 
-static void print_list(action_list_t *list, int exec_num = -1)
+static void print_list(action_list_t *list)
 {
 	action_list_t::iterator it;
 
 	model_print("---------------------------------------------------------------------\n");
-	if (exec_num >= 0)
-		model_print("Execution %d:\n", exec_num);
 
-	unsigned int hash=0;
+	unsigned int hash = 0;
 
 	for (it = list->begin(); it != list->end(); it++) {
 		(*it)->print();
-		hash=hash^(hash<<3)^((*it)->hash());
+		hash = hash^(hash<<3)^((*it)->hash());
 	}
 	model_print("HASH %u\n", hash);
 	model_print("---------------------------------------------------------------------\n");
 }
 
 #if SUPPORT_MOD_ORDER_DUMP
-void ModelChecker::dumpGraph(char *filename) {
+void ModelChecker::dumpGraph(char *filename) const
+{
 	char buffer[200];
-	sprintf(buffer, "%s.dot",filename);
-	FILE *file=fopen(buffer, "w");
-	fprintf(file, "digraph %s {\n",filename);
+	sprintf(buffer, "%s.dot", filename);
+	FILE *file = fopen(buffer, "w");
+	fprintf(file, "digraph %s {\n", filename);
 	mo_graph->dumpNodes(file);
-	ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
+	ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
 
 	for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
-		ModelAction *action=*it;
+		ModelAction *action = *it;
 		if (action->is_read()) {
-			fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
-			if (action->get_reads_from()!=NULL)
+			fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
+			if (action->get_reads_from() != NULL)
 				fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
 		}
 		if (thread_array[action->get_tid()] != NULL) {
 			fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
 		}
 
-		thread_array[action->get_tid()]=action;
+		thread_array[action->get_tid()] = action;
 	}
-	fprintf(file,"}\n");
+	fprintf(file, "}\n");
 	model_free(thread_array);
 	fclose(file);
 }
@@ -2605,9 +2633,12 @@ void ModelChecker::print_summary() const
 	dumpGraph(buffername);
 #endif
 
-	if (!isfeasibleprefix())
-		model_print("INFEASIBLE EXECUTION!\n");
-	print_list(action_trace, stats.num_total);
+	model_print("Execution %d:", stats.num_total);
+	if (isfeasibleprefix())
+		model_print("\n");
+	else
+		print_infeasibility(" INFEASIBLE");
+	print_list(action_trace);
 	model_print("\n");
 }
 
@@ -2697,27 +2728,18 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 
 /**
  * Takes the next step in the execution, if possible.
+ * @param curr The current step to take
  * @return Returns true (success) if a step was taken and false otherwise.
  */
-bool ModelChecker::take_step() {
+bool ModelChecker::take_step(ModelAction *curr)
+{
 	if (has_asserted())
 		return false;
 
-	Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
-	if (curr) {
-		if (curr->get_state() == THREAD_READY) {
-			ASSERT(priv->current_action);
+	Thread *curr_thrd = get_thread(curr);
+	ASSERT(curr_thrd->get_state() == THREAD_READY);
 
-			priv->nextThread = check_current_action(priv->current_action);
-			priv->current_action = NULL;
-
-			if (curr->is_blocked() || curr->is_complete())
-				scheduler->remove_thread(curr);
-		} else {
-			ASSERT(false);
-		}
-	}
-	Thread *next = scheduler->next_thread(priv->nextThread);
+	curr = check_current_action(curr);
 
 	/* Infeasible -> don't take any more steps */
 	if (is_infeasible())
@@ -2727,14 +2749,18 @@ bool ModelChecker::take_step() {
 		return false;
 	}
 
-	if (params.bound != 0) {
-		if (priv->used_sequence_numbers > params.bound) {
+	if (params.bound != 0)
+		if (priv->used_sequence_numbers > params.bound)
 			return false;
-		}
-	}
 
-	DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
-			next ? id_to_int(next->get_id()) : -1);
+	if (curr_thrd->is_blocked() || curr_thrd->is_complete())
+		scheduler->remove_thread(curr_thrd);
+
+	Thread *next_thrd = get_next_thread(curr);
+	next_thrd = scheduler->next_thread(next_thrd);
+
+	DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
+			next_thrd ? id_to_int(next_thrd->get_id()) : -1);
 
 	/*
 	 * Launch end-of-execution release sequence fixups only when there are:
@@ -2745,7 +2771,7 @@ bool ModelChecker::take_step() {
 	 * (3) pending assertions (i.e., data races)
 	 * (4) no pending promises
 	 */
-	if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
+	if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
 			is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
 		model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
 				pending_rel_seqs->size());
@@ -2756,22 +2782,22 @@ bool ModelChecker::take_step() {
 		return true;
 	}
 
-	/* next == NULL -> don't take any more steps */
-	if (!next)
+	/* next_thrd == NULL -> don't take any more steps */
+	if (!next_thrd)
 		return false;
 
-	next->set_state(THREAD_RUNNING);
+	next_thrd->set_state(THREAD_RUNNING);
 
-	if (next->get_pending() != NULL) {
+	if (next_thrd->get_pending() != NULL) {
 		/* restart a pending action */
-		set_current_action(next->get_pending());
-		next->set_pending(NULL);
-		next->set_state(THREAD_READY);
+		set_current_action(next_thrd->get_pending());
+		next_thrd->set_pending(NULL);
+		next_thrd->set_state(THREAD_READY);
 		return true;
 	}
 
 	/* Return false only if swap fails with an error */
-	return (Thread::swap(&system_context, next) == 0);
+	return (Thread::swap(&system_context, next_thrd) == 0);
 }
 
 /** Wrapper to run the user's main function, with appropriate arguments */
@@ -2785,12 +2811,16 @@ void ModelChecker::run()
 {
 	do {
 		thrd_t user_thread;
+		Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
+
+		add_thread(t);
 
-		/* Start user program */
-		add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
+		/* Run user thread up to its first action */
+		scheduler->next_thread(t);
+		Thread::swap(&system_context, t);
 
 		/* Wait for all threads to complete */
-		while (take_step());
+		while (take_step(priv->current_action));
 	} while (next_execution());
 
 	print_stats();