X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=execution.cc;h=f2c50c4321c67cd83da4c905ac1bcd652307b4a0;hp=66418a4abb630a5b234b035342f4179435c52363;hb=4a0000d96b695d084ffa930564a267d15abd91af;hpb=c5703c61b49d29d3f56fdcb06847f2aa811eeb4e

diff --git a/execution.cc b/execution.cc
index 66418a4..f2c50c4 100644
--- a/execution.cc
+++ b/execution.cc
@@ -58,7 +58,7 @@ struct model_snapshot_members {
 
 /** @brief Constructor */
 ModelExecution::ModelExecution(ModelChecker *m,
-		struct model_params *params,
+		const struct model_params *params,
 		Scheduler *scheduler,
 		NodeStack *node_stack) :
 	model(m),
@@ -82,6 +82,7 @@ ModelExecution::ModelExecution(ModelChecker *m,
 	model_thread = new Thread(get_next_id());
 	add_thread(model_thread);
 	scheduler->register_engine(this);
+	node_stack->register_engine(this);
 }
 
 /** @brief Destructor */
@@ -263,6 +264,28 @@ bool ModelExecution::is_deadlocked() const
 	return blocking_threads;
 }
 
+/**
+ * @brief Check if we are yield-blocked
+ *
+ * A program can be "yield-blocked" if all threads are ready to execute a
+ * yield.
+ *
+ * @return True if the program is yield-blocked; false otherwise
+ */
+bool ModelExecution::is_yieldblocked() const
+{
+	if (!params->yieldblock)
+		return false;
+
+	for (unsigned int i = 0; i < get_num_threads(); i++) {
+		thread_id_t tid = int_to_id(i);
+		Thread *t = get_thread(tid);
+		if (t->get_pending() && t->get_pending()->is_yield())
+			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
@@ -272,6 +295,8 @@ bool ModelExecution::is_deadlocked() const
  */
 bool ModelExecution::is_complete_execution() const
 {
+	if (is_yieldblocked())
+		return false;
 	for (unsigned int i = 0; i < get_num_threads(); i++)
 		if (is_enabled(int_to_id(i)))
 			return false;
@@ -365,7 +390,10 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
 ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 {
 	switch (act->get_type()) {
-	/* case ATOMIC_FENCE: fences don't directly cause backtracking */
+	case ATOMIC_FENCE:
+		/* Only seq-cst fences can (directly) cause backtracking */
+		if (!act->is_seqcst())
+			break;
 	case ATOMIC_READ:
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {
@@ -376,6 +404,8 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
+			if (prev == act)
+				continue;
 			if (prev->could_synchronize_with(act)) {
 				ret = prev;
 				break;
@@ -1175,9 +1205,10 @@ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *wai
 /**
  * @brief Check whether a model action is enabled.
  *
- * Checks whether a lock or join operation would be successful (i.e., is the
- * lock already locked, or is the joined thread already complete). If not, put
- * the action in a waiter list.
+ * Checks whether an operation would be successful (i.e., is a lock already
+ * locked, or is the joined thread already complete).
+ *
+ * For yield-blocking, yields are never enabled.
  *
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
@@ -1194,6 +1225,8 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
 			thread_blocking_check_promises(blocking, get_thread(curr));
 			return false;
 		}
+	} else if (params->yieldblock && curr->is_yield()) {
+		return false;
 	}
 
 	return true;
@@ -1208,7 +1241,7 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
  *
  * @param curr The current action to process
  * @return The ModelAction that is actually executed; may be different than
- * curr; may be NULL, if the current action is not enabled to run
+ * curr
  */
 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 {
@@ -2610,7 +2643,7 @@ void ModelExecution::dumpGraph(char *filename) const
 	mo_graph->dumpNodes(file);
 	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++) {
+	for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) {
 		ModelAction *act = *it;
 		if (act->is_read()) {
 			mo_graph->dot_print_node(file, act);
@@ -2653,6 +2686,8 @@ void ModelExecution::print_summary() const
 
 	model_print("Execution %d:", get_execution_number());
 	if (isfeasibleprefix()) {
+		if (is_yieldblocked())
+			model_print(" YIELD BLOCKED");
 		if (scheduler->all_threads_sleeping())
 			model_print(" SLEEP-SET REDUNDANT");
 		model_print("\n");
@@ -2810,7 +2845,7 @@ void ModelExecution::fixup_release_sequences()
 {
 	while (!pending_rel_seqs.empty() &&
 			is_feasible_prefix_ignore_relseq() &&
-			!unrealizedraces.empty()) {
+			haveUnrealizedRaces()) {
 		model_print("*** WARNING: release sequence fixup action "
 				"(%zu pending release seuqence(s)) ***\n",
 				pending_rel_seqs.size());