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

diff --git a/model.cc b/model.cc
index c9bb868..e6df37f 100644
--- a/model.cc
+++ b/model.cc
@@ -159,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 */
@@ -174,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();
@@ -212,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? */
@@ -610,7 +614,7 @@ 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;
 	} else {
@@ -820,7 +824,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 		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;
 	}
@@ -849,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
@@ -862,12 +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))
-				set_latest_backtrack(pfv.act);
+			add_future_value(pfv.writer, pfv.act);
 		}
-		futurevalues->resize(0);
+		futurevalues->clear();
 	}
 
 	mo_graph->commitChanges();
@@ -944,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 */
@@ -1203,8 +1213,8 @@ ModelAction * 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());
+		get_thread(curr)->set_pending(curr);
+		scheduler->sleep(get_thread(curr));
 		return NULL;
 	}
 
@@ -1329,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;
 }
 
@@ -1349,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();
 }
 
@@ -1365,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();
@@ -1769,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));
 					}
 				}
 			}
@@ -2558,13 +2576,11 @@ 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;
 
@@ -2617,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");
 }