X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=217d6421ac403e60108ec074c900168bbce67888;hp=0e2b818cd26487df48b0968484e9533c984a8443;hb=c5b57f3d98d1d14b4546995a0882753cf71a1c4b;hpb=7c003db5218470054490a6777c97c6611b933a12

diff --git a/model.cc b/model.cc
index 0e2b818c..217d6421 100644
--- a/model.cc
+++ b/model.cc
@@ -9,6 +9,7 @@
 #include "clockvector.h"
 #include "cyclegraph.h"
 #include "promise.h"
+#include "datarace.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -36,7 +37,8 @@ ModelChecker::ModelChecker(struct model_params params) :
 	node_stack(new NodeStack()),
 	next_backtrack(NULL),
 	mo_graph(new CycleGraph()),
-	failed_promise(false)
+	failed_promise(false),
+	asserted(false)
 {
 }
 
@@ -77,6 +79,7 @@ void ModelChecker::reset_to_initial_state()
 	nextThread = NULL;
 	next_backtrack = NULL;
 	failed_promise = false;
+	reset_asserted();
 	snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -299,6 +302,19 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	if (curr->get_type() == THREAD_CREATE) {
 		Thread *th = (Thread *)curr->get_location();
 		th->set_creation(curr);
+	} else if (curr->get_type() == THREAD_JOIN) {
+		Thread *wait, *join;
+		wait = get_thread(curr->get_tid());
+		join = (Thread *)curr->get_location();
+		if (!join->is_complete())
+			scheduler->wait(wait, join);
+	} else if (curr->get_type() == THREAD_FINISH) {
+		Thread *th = get_thread(curr->get_tid());
+		while (!th->wait_list_empty()) {
+			Thread *wake = th->pop_wait_list();
+			scheduler->wake(wake);
+		}
+		th->complete();
 	}
 
 	/* Deal with new thread */
@@ -326,7 +342,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		}
 	} else if (curr->is_write()) {
 		if (w_modification_order(curr))
-			updated = true;;
+			updated = true;
 		if (resolve_promises(curr))
 			updated = true;
 	}
@@ -361,6 +377,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
  * feasible trace. */
 
 bool ModelChecker::isfeasibleprefix() {
+	return promises->size()==0;
 }
 
 /** @returns whether the current partial trace is feasible. */
@@ -693,6 +710,11 @@ bool ModelChecker::resolve_release_sequences(void *location)
 			it++;
 	}
 
+	// If we resolved promises or data races, see if we have realized a data race.
+	if (checkDataRaces()) {
+		model->set_assert();
+	}
+
 	return updated;
 }
 
@@ -784,6 +806,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 		} else
 			promise_index++;
 	}
+
 	return resolved;
 }
 
@@ -947,10 +970,7 @@ void ModelChecker::remove_thread(Thread *t)
  * 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. May be NULL, although
- * there is little reason to switch to the model-checker without an action to
- * explore (note: act == NULL is sometimes used as a hack to allow a thread to
- * yield control without performing any progress; see thrd_join()).
+ * @param act The current action that will be explored. Must not be NULL.
  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
  */
 int ModelChecker::switch_to_master(ModelAction *act)
@@ -962,14 +982,6 @@ int ModelChecker::switch_to_master(ModelAction *act)
 	return Thread::swap(old, &system_context);
 }
 
-void ModelChecker::assert_thread() {
-	DBG();
-	Thread *old = thread_current();
-	set_current_action(NULL);
-	old->set_state(THREAD_ASSERTED);
-	return Thread::swap(old, &system_context);
-}
-
 /**
  * Takes the next step in the execution, if possible.
  * @return Returns true (success) if a step was taken and false otherwise.
@@ -977,20 +989,17 @@ void ModelChecker::assert_thread() {
 bool ModelChecker::take_step() {
 	Thread *curr, *next;
 
+	if (has_asserted())
+		return false;
+
 	curr = thread_current();
 	if (curr) {
 		if (curr->get_state() == THREAD_READY) {
-			if (current_action) {
-				nextThread = check_current_action(current_action);
-				current_action = NULL;
-			}
-			scheduler->add_thread(curr);
-		} else if (curr->get_state() == THREAD_RUNNING) {
-			/* Stopped while running; i.e., completed */
-			curr->complete();
-		} else if (curr->get_state()==THREAD_ASSERTED) {
-			/* Something bad happened.  Stop taking steps. */
-			return false;
+			ASSERT(current_action);
+			nextThread = check_current_action(current_action);
+			current_action = NULL;
+			if (!curr->is_blocked() && !curr->is_complete())
+				scheduler->add_thread(curr);
 		} else {
 			ASSERT(false);
 		}