X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=cd703edf329ef3245b8bcded411c540b3ac3ab22;hp=9e476a95f76a68d1f3395b271c83b0b70c0cc387;hb=ff3ab0abac18649da161a495781c3925cbcd62a4;hpb=4e4fa53414eb5f0a78e05478127b375d5f0aba73

diff --git a/model.cc b/model.cc
index 9e476a95..cd703edf 100644
--- a/model.cc
+++ b/model.cc
@@ -204,34 +204,43 @@ Node * ModelChecker::get_curr_node() const
 	return node_stack->get_head();
 }
 
+/**
+ * @brief Select the next thread to execute based on the curren action
+ *
+ * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
+ * actions should be followed by the execution of their child thread. In either
+ * case, the current action should determine the next thread schedule.
+ *
+ * @param curr The current action
+ * @return The next thread to run, if the current action will determine this
+ * selection; otherwise NULL
+ */
+Thread * ModelChecker::action_select_next_thread(const ModelAction *curr) const
+{
+	/* Do not split atomic RMW */
+	if (curr->is_rmwr())
+		return get_thread(curr);
+	/* Follow CREATE with the created thread */
+	if (curr->get_type() == THREAD_CREATE)
+		return curr->get_thread_operand();
+	return NULL;
+}
+
 /**
  * @brief Choose the next thread to execute.
  *
- * This function chooses the next thread that should execute. It can force the
- * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
- * followed by a THREAD_START, or it can enforce execution replay/backtracking.
- * The model-checker may have no preference regarding the next thread (i.e.,
- * when exploring a new execution ordering), in which case we defer to the
- * scheduler.
+ * This function chooses the next thread that should execute. It can enforce
+ * execution replay/backtracking or, if the model-checker has no preference
+ * regarding the next thread (i.e., when exploring a new execution ordering),
+ * we defer to the scheduler.
  *
- * @param curr Optional: The current ModelAction. Only used if non-NULL and it
- * might guide the choice of next thread (i.e., THREAD_CREATE should be
- * followed by THREAD_START, or ATOMIC_RMWR followed by ATOMIC_{RMW,RMWC})
- * @return The next chosen thread to run, if any exist. Or else if no threads
- * remain to be executed, return NULL.
+ * @return The next chosen thread to run, if any exist. Or else if the current
+ * execution should terminate, return NULL.
  */
-Thread * ModelChecker::get_next_thread(ModelAction *curr)
+Thread * ModelChecker::get_next_thread()
 {
 	thread_id_t tid;
 
-	if (curr != NULL) {
-		/* Do not split atomic actions. */
-		if (curr->is_rmwr())
-			return get_thread(curr);
-		else if (curr->get_type() == THREAD_CREATE)
-			return curr->get_thread_operand();
-	}
-
 	/*
 	 * Have we completed exploring the preselected path? Then let the
 	 * scheduler decide
@@ -400,6 +409,22 @@ bool ModelChecker::is_deadlocked() const
 	return blocking_threads;
 }
 
+/**
+ * Check if a Thread has entered a circular wait deadlock situation. This will
+ * not check other threads for potential deadlock situations, and may miss
+ * deadlocks involving WAIT.
+ *
+ * @param t The thread which may have entered a deadlock
+ * @return True if this Thread entered a deadlock; false otherwise
+ */
+bool ModelChecker::is_circular_wait(const Thread *t) const
+{
+	for (Thread *waiting = t->waiting_on() ; waiting != NULL; waiting = waiting->waiting_on())
+		if (waiting == t)
+			return true;
+	return false;
+}
+
 /**
  * Check if this is a complete execution. That is, have all thread completed
  * execution (rather than exiting because sleep sets have forced a redundant
@@ -514,7 +539,7 @@ void ModelChecker::print_execution(bool printbugs) const
 {
 	print_program_output();
 
-	if (DBG_ENABLED() || params.verbose) {
+	if (params.verbose) {
 		model_print("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
 			earliest_diverge->print();
@@ -558,7 +583,7 @@ bool ModelChecker::next_execution()
 	record_stats();
 
 	/* Output */
-	if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
+	if (params.verbose || (complete && have_bug_reports()))
 		print_execution(complete);
 	else
 		clear_program_output();
@@ -853,7 +878,6 @@ ModelAction * ModelChecker::get_next_backtrack()
 bool ModelChecker::process_read(ModelAction *curr)
 {
 	Node *node = curr->get_node();
-	uint64_t value = VALUE_NONE;
 	while (true) {
 		bool updated = false;
 		switch (node->get_read_from_status()) {
@@ -864,27 +888,25 @@ bool ModelChecker::process_read(ModelAction *curr)
 			mo_graph->startChanges();
 
 			ASSERT(!is_infeasible());
-			if (!check_recency(curr, rf))
-				priv->too_many_reads = true;
-			updated = r_modification_order(curr, rf);
-
-			if (is_infeasible() && node->increment_read_from()) {
-				mo_graph->rollbackChanges();
-				priv->too_many_reads = false;
-				continue;
+			if (!check_recency(curr, rf)) {
+				if (node->increment_read_from()) {
+					mo_graph->rollbackChanges();
+					continue;
+				} else {
+					priv->too_many_reads = true;
+				}
 			}
 
-			value = rf->get_value();
+			updated = r_modification_order(curr, rf);
 			read_from(curr, rf);
 			mo_graph->commitChanges();
 			mo_check_promises(curr, true);
-
 			break;
 		}
 		case READ_FROM_PROMISE: {
 			Promise *promise = curr->get_node()->get_read_from_promise();
-			promise->add_reader(curr);
-			value = promise->get_value();
+			if (promise->add_reader(curr))
+				priv->failed_promise = true;
 			curr->set_read_from_promise(promise);
 			mo_graph->startChanges();
 			if (!check_recency(curr, promise))
@@ -897,7 +919,6 @@ bool ModelChecker::process_read(ModelAction *curr)
 			/* Read from future value */
 			struct future_value fv = node->get_future_value();
 			Promise *promise = new Promise(curr, fv);
-			value = fv.value;
 			curr->set_read_from_promise(promise);
 			promises->push_back(promise);
 			mo_graph->startChanges();
@@ -908,7 +929,7 @@ bool ModelChecker::process_read(ModelAction *curr)
 		default:
 			ASSERT(false);
 		}
-		get_thread(curr)->set_return_value(value);
+		get_thread(curr)->set_return_value(curr->get_return_value());
 		return updated;
 	}
 }
@@ -931,20 +952,15 @@ bool ModelChecker::process_read(ModelAction *curr)
  */
 bool ModelChecker::process_mutex(ModelAction *curr)
 {
-	std::mutex *mutex = NULL;
+	std::mutex *mutex = curr->get_mutex();
 	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()) {
-		mutex = (std::mutex *)curr->get_value();
+	if (mutex)
 		state = mutex->get_state();
-	}
 
 	switch (curr->get_type()) {
 	case ATOMIC_TRYLOCK: {
-		bool success = !state->islocked;
+		bool success = !state->locked;
 		curr->set_try_lock(success);
 		if (!success) {
 			get_thread(curr)->set_return_value(0);
@@ -956,7 +972,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 	case ATOMIC_LOCK: {
 		if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
 			assert_bug("Lock access before initialization");
-		state->islocked = true;
+		state->locked = get_thread(curr);
 		ModelAction *unlock = get_last_unlock(curr);
 		//synchronize with the previous unlock statement
 		if (unlock != NULL) {
@@ -967,7 +983,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 	}
 	case ATOMIC_UNLOCK: {
 		//unlock the lock
-		state->islocked = false;
+		state->locked = NULL;
 		//wake up the other threads
 		action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
 		//activate all the waiting threads
@@ -979,7 +995,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 	}
 	case ATOMIC_WAIT: {
 		//unlock the lock
-		state->islocked = false;
+		state->locked = NULL;
 		//wake up the other threads
 		action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
 		//activate all the waiting threads
@@ -1411,7 +1427,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 	if (curr->is_lock()) {
 		std::mutex *lock = (std::mutex *)curr->get_location();
 		struct std::mutex_state *state = lock->get_state();
-		if (state->islocked) {
+		if (state->locked) {
 			//Stick the action in the appropriate waiting queue
 			get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
 			return false;
@@ -2512,7 +2528,6 @@ int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
 bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
 {
 	std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
-	promise_list_t mustResolve;
 	Promise *promise = (*promises)[promise_idx];
 
 	for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
@@ -2522,20 +2537,23 @@ bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
 	}
 	/* Make sure the promise's value matches the write's value */
 	ASSERT(promise->is_compatible(write) && promise->same_value(write));
-	mo_graph->resolvePromise(promise, write, &mustResolve);
+	if (!mo_graph->resolvePromise(promise, write))
+		priv->failed_promise = true;
 
 	promises->erase(promises->begin() + promise_idx);
-
-	/** @todo simplify the 'mustResolve' stuff */
-	ASSERT(mustResolve.size() <= 1);
-
-	if (!mustResolve.empty() && mustResolve[0] != promise)
-		priv->failed_promise = true;
-	delete promise;
+	/**
+	 * @todo  It is possible to end up in an inconsistent state, where a
+	 * "resolved" promise may still be referenced if
+	 * CycleGraph::resolvePromise() failed, so don't delete 'promise'.
+	 *
+	 * Note that the inconsistency only matters when dumping mo_graph to
+	 * file.
+	 *
+	 * delete promise;
+	 */
 
 	//Check whether reading these writes has made threads unable to
 	//resolve promises
-
 	for (unsigned int i = 0; i < actions_to_check.size(); i++) {
 		ModelAction *read = actions_to_check[i];
 		mo_check_promises(read, true);
@@ -2796,7 +2814,9 @@ static void print_list(action_list_t *list)
 	unsigned int hash = 0;
 
 	for (it = list->begin(); it != list->end(); it++) {
-		(*it)->print();
+		const ModelAction *act = *it;
+		if (act->get_seq_number() > 0)
+			act->print();
 		hash = hash^(hash<<3)^((*it)->hash());
 	}
 	model_print("HASH %u\n", hash);
@@ -2863,6 +2883,14 @@ void ModelChecker::print_summary() const
 		print_infeasibility(" INFEASIBLE");
 	print_list(action_trace);
 	model_print("\n");
+	if (!promises->empty()) {
+		model_print("Pending promises:\n");
+		for (unsigned int i = 0; i < promises->size(); i++) {
+			model_print(" [P%u] ", i);
+			(*promises)[i]->print();
+		}
+		model_print("\n");
+	}
 }
 
 /**
@@ -3009,7 +3037,11 @@ Thread * ModelChecker::take_step(ModelAction *curr)
 	if (curr_thrd->is_blocked() || curr_thrd->is_complete())
 		scheduler->remove_thread(curr_thrd);
 
-	Thread *next_thrd = get_next_thread(curr);
+	Thread *next_thrd = NULL;
+	if (curr)
+		next_thrd = action_select_next_thread(curr);
+	if (!next_thrd)
+		next_thrd = get_next_thread();
 
 	DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
 			next_thrd ? id_to_int(next_thrd->get_id()) : -1);
@@ -3043,6 +3075,8 @@ void ModelChecker::run()
 				Thread *thr = get_thread(tid);
 				if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
 					switch_from_master(thr);
+					if (is_circular_wait(thr))
+						assert_bug("Deadlock detected");
 				}
 			}