X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=400adc208047f8d2c7b4700c31bc20b650854e34;hb=82df62c2b0805848b87bb71df5b66a4a66f8e25d;hp=7c6b90d7093e88d0452c14f2ceaa2bab633a58c1;hpb=a11a861e697310b5fd8abe52dff49fc8a66eeb78;p=model-checker.git

diff --git a/model.cc b/model.cc
index 7c6b90d..400adc2 100644
--- a/model.cc
+++ b/model.cc
@@ -48,6 +48,7 @@ struct model_snapshot_members {
 		stats(),
 		failed_promise(false),
 		too_many_reads(false),
+		no_valid_reads(false),
 		bad_synchronization(false),
 		asserted(false)
 	{ }
@@ -66,6 +67,7 @@ struct model_snapshot_members {
 	struct execution_stats stats;
 	bool failed_promise;
 	bool too_many_reads;
+	bool no_valid_reads;
 	/** @brief Incorrectly-ordered synchronization was made */
 	bool bad_synchronization;
 	bool asserted;
@@ -294,7 +296,6 @@ void ModelChecker::execute_sleep_set()
 		thread_id_t tid = int_to_id(i);
 		Thread *thr = get_thread(tid);
 		if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
-			thr->set_state(THREAD_RUNNING);
 			scheduler->next_thread(thr);
 			Thread::swap(&system_context, thr);
 			priv->current_action->set_sleep_flag();
@@ -968,7 +969,10 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 
 	switch (curr->get_type()) {
 	case THREAD_CREATE: {
-		Thread *th = curr->get_thread_operand();
+		thrd_t *thrd = (thrd_t *)curr->get_location();
+		struct thread_params *params = (struct thread_params *)curr->get_value();
+		Thread *th = new Thread(thrd, params->func, params->arg);
+		add_thread(th);
 		th->set_creation(curr);
 		/* Promises can be satisfied by children */
 		for (unsigned int i = 0; i < promises->size(); i++) {
@@ -1387,6 +1391,8 @@ void ModelChecker::print_infeasibility(const char *prefix) const
 		ptr += sprintf(ptr, "[failed promise]");
 	if (priv->too_many_reads)
 		ptr += sprintf(ptr, "[too many reads]");
+	if (priv->no_valid_reads)
+		ptr += sprintf(ptr, "[no valid reads-from]");
 	if (priv->bad_synchronization)
 		ptr += sprintf(ptr, "[bad sw ordering]");
 	if (promises_expired())
@@ -1415,6 +1421,7 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
 bool ModelChecker::is_infeasible() const
 {
 	return mo_graph->checkForCycles() ||
+		priv->no_valid_reads ||
 		priv->failed_promise ||
 		priv->too_many_reads ||
 		priv->bad_synchronization ||
@@ -1494,13 +1501,9 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 				continue;
 
 			/* Test to see whether this is a feasible write to read from */
-			mo_graph->startChanges();
-			r_modification_order(curr, write);
-			bool feasiblereadfrom = !is_infeasible();
-			mo_graph->rollbackChanges();
+			/** NOTE: all members of read-from set should be
+			 *  feasible, so we no longer check it here **/
 
-			if (!feasiblereadfrom)
-				continue;
 			rit = ritcopy;
 
 			bool feasiblewrite = true;
@@ -2372,36 +2375,18 @@ void ModelChecker::check_promises_thread_disabled()
  * @brief Checks promises in response to addition to modification order for
  * threads.
  *
- * Definitions:
- *
- * pthread is the thread that performed the read that created the promise
- *
- * pread is the read that created the promise
- *
- * pwrite is either the first write to same location as pread by
- * pthread that is sequenced after pread or the write read by the
- * first read to the same location as pread by pthread that is
- * sequenced after pread.
- *
- * 1. If tid=pthread, then we check what other threads are reachable
- * through the mod order starting with pwrite.  Those threads cannot
- * perform a write that will resolve the promise due to modification
- * order constraints.
+ * We test whether threads are still available for satisfying promises after an
+ * addition to our modification order constraints. Those that are unavailable
+ * are "eliminated". Once all threads are eliminated from satisfying a promise,
+ * that promise has failed.
  *
- * 2. If the tid is not pthread, we check whether pwrite can reach the
- * action write through the modification order.  If so, that thread
- * cannot perform a future write that will resolve the promise due to
- * modificatin order constraints.
- *
- * @param tid The thread that either read from the model action write, or
- * actually did the model action write.
- *
- * @param write The ModelAction representing the relevant write.
- * @param read  The ModelAction that reads a promised write, or NULL otherwise.
+ * @param act The ModelAction which updated the modification order
+ * @param is_read_check Should be true if act is a read and we must check for
+ * updates to the store from which it read (there is a distinction here for
+ * RMW's, which are both a load and a store)
  */
 void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
 {
-	thread_id_t tid = act->get_tid();
 	const ModelAction *write = is_read_check ? act->get_reads_from() : act;
 
 	for (unsigned int i = 0; i < promises->size(); i++) {
@@ -2412,34 +2397,17 @@ void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
 		if (!pread->same_var(write))
 			continue;
 
-		// same thread as pread
-		if (pread->get_tid() == tid) {
-			// make sure that the reader of this write happens after the promise
-			if (!is_read_check || (pread->happens_before(act))) {
-				// do we have a pwrite for the promise, if not, set it
-				if (promise->get_write() == NULL) {
-					promise->set_write(write);
-					// The pwrite cannot happen before pread
-					if (write->happens_before(pread) && (write != pread)) {
-						priv->failed_promise = true;
-						return;
-					}
-				}
-
-				if (mo_graph->checkPromise(write, promise)) {
-					priv->failed_promise = true;
-					return;
-				}
-			}
+		if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
+			priv->failed_promise = true;
+			return;
 		}
 
 		// Don't do any lookups twice for the same thread
-		if (!promise->thread_is_available(tid))
+		if (!promise->thread_is_available(act->get_tid()))
 			continue;
 
-		const ModelAction *pwrite = promise->get_write();
-		if (pwrite && mo_graph->checkReachable(pwrite, write)) {
-			if (promise->eliminate_thread(tid)) {
+		if (mo_graph->checkReachable(promise, write)) {
+			if (mo_graph->checkPromise(write, promise)) {
 				priv->failed_promise = true;
 				return;
 			}
@@ -2508,14 +2476,25 @@ 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)
-				curr->get_node()->add_read_from(act);
+			if (allow_read) {
+				/* Only add feasible reads */
+				mo_graph->startChanges();
+				r_modification_order(curr, act);
+				if (!is_infeasible())
+					curr->get_node()->add_read_from(act);
+				mo_graph->rollbackChanges();
+			}
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr))
 				break;
 		}
 	}
+	/* We may find no valid may-read-from only if the execution is doomed */
+	if (!curr->get_node()->get_read_from_size()) {
+		priv->no_valid_reads = true;
+		set_assert();
+	}
 
 	if (DBG_ENABLED()) {
 		model_print("Reached read action:\n");
@@ -2700,7 +2679,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 	DBG();
 	Thread *old = thread_current();
 	set_current_action(act);
-	old->set_state(THREAD_READY);
 	if (Thread::swap(old, &system_context) < 0) {
 		perror("swap threads");
 		exit(EXIT_FAILURE);
@@ -2768,13 +2746,10 @@ bool ModelChecker::take_step(ModelAction *curr)
 	if (!next_thrd)
 		return false;
 
-	next_thrd->set_state(THREAD_RUNNING);
-
 	if (next_thrd->get_pending() != NULL) {
 		/* restart a pending action */
 		set_current_action(next_thrd->get_pending());
 		next_thrd->set_pending(NULL);
-		next_thrd->set_state(THREAD_READY);
 		return true;
 	}