X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=9e611fae96367283e33d7b927224eb259b52a27e;hp=017455d24124c726ddd5164c508feaab3bd2b24f;hb=3b3533a76db06884f44b3e70ccdbad647275fcc4;hpb=a91144758ab80e865e5227c236e368fc0d3d77a9

diff --git a/model.cc b/model.cc
index 017455d2..9e611fae 100644
--- a/model.cc
+++ b/model.cc
@@ -721,7 +721,6 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 				r_status = r_modification_order(curr, reads_from);
 			}
 
-
 			if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
 				mo_graph->rollbackChanges();
 				priv->too_many_reads = false;
@@ -737,9 +736,9 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 			/* Read from future value */
 			struct future_value fv = curr->get_node()->get_future_value();
 			value = fv.value;
+			curr->set_value(fv.value);
 			curr->set_read_from(NULL);
-			Promise *valuepromise = new Promise(curr, value, fv.expiration);
-			promises->push_back(valuepromise);
+			promises->push_back(new Promise(curr, fv));
 		}
 		get_thread(curr)->set_return_value(value);
 		return updated;
@@ -856,10 +855,22 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 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);
+	if (mo_may_allow(writer, reader)) {
+		Node *node = reader->get_node();
+
+		/* Find an ancestor thread which exists at the time of the reader */
+		Thread *write_thread = get_thread(writer);
+		while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
+			write_thread = write_thread->get_parent();
+
+		struct future_value fv = {
+			writer->get_value(),
+			writer->get_seq_number() + params.maxfuturedelay,
+			write_thread->get_id(),
+		};
+		if (node->add_future_value(fv))
+			set_latest_backtrack(reader);
+	}
 }
 
 /**
@@ -956,6 +967,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 	case THREAD_CREATE: {
 		Thread *th = curr->get_thread_operand();
 		th->set_creation(curr);
+		/* Promises can be satisfied by children */
+		for (unsigned int i = 0; i < promises->size(); i++) {
+			Promise *promise = (*promises)[i];
+			if (promise->thread_is_available(curr->get_tid()))
+				promise->add_thread(th->get_id());
+		}
 		break;
 	}
 	case THREAD_JOIN: {
@@ -972,6 +989,13 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 			scheduler->wake(get_thread(act));
 		}
 		th->complete();
+		/* Completed thread can't satisfy promises */
+		for (unsigned int i = 0; i < promises->size(); i++) {
+			Promise *promise = (*promises)[i];
+			if (promise->thread_is_available(th->get_id()))
+				if (promise->eliminate_thread(th->get_id()))
+					priv->failed_promise = true;
+		}
 		updated = true; /* trigger rel-seq checks */
 		break;
 	}
@@ -1383,21 +1407,11 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-	return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
-}
-
-/**
- * Check If the current partial trace is infeasible, while ignoring
- * infeasibility related to 2 RMW's reading from the same store. It does not
- * check end-of-execution feasibility.
- * @see ModelChecker::is_infeasible
- * @return whether the current partial trace is infeasible, ignoring multiple
- * RMWs reading from the same store.
- * */
-bool ModelChecker::is_infeasible_ignoreRMW() const
-{
-	return mo_graph->checkForCycles() || priv->failed_promise ||
-		priv->too_many_reads || priv->bad_synchronization ||
+	return mo_graph->checkForRMWViolation() ||
+		mo_graph->checkForCycles() ||
+		priv->failed_promise ||
+		priv->too_many_reads ||
+		priv->bad_synchronization ||
 		promises_expired();
 }
 
@@ -1786,10 +1800,10 @@ 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())) {
+					if (!is_infeasible())
 						futurevalues->push_back(PendingFutureValue(curr, act));
-					}
+					else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
+						add_future_value(curr, act);
 				}
 			}
 		}
@@ -2379,7 +2393,7 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
 		const ModelAction *act = promise->get_action();
 		if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
 				merge_cv->synchronized_since(act)) {
-			if (promise->increment_threads(tid)) {
+			if (promise->eliminate_thread(tid)) {
 				//Promise has failed
 				priv->failed_promise = true;
 				return;
@@ -2388,29 +2402,34 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
 	}
 }
 
-void ModelChecker::check_promises_thread_disabled() {
+void ModelChecker::check_promises_thread_disabled()
+{
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		if (promise->check_promise()) {
+		if (promise->has_failed()) {
 			priv->failed_promise = true;
 			return;
 		}
 	}
 }
 
-/** Checks promises in response to addition to modification order for threads.
+/**
+ * @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 value read by the
- * first read to the same lcoation as pread by pthread that is
- * sequenced after pread..
+ * 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 mode order starting with pwrite.  Those threads cannot
+ * 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.
  *
@@ -2419,11 +2438,11 @@ void ModelChecker::check_promises_thread_disabled() {
  * 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 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 write The ModelAction representing the relevant write.
+ * @param read  The ModelAction that reads a promised write, or NULL otherwise.
  */
 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
 {
@@ -2432,24 +2451,24 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write,
 		Promise *promise = (*promises)[i];
 		const ModelAction *act = promise->get_action();
 
-		//Is this promise on the same location?
+		// Is this promise on the same location?
 		if (act->get_location() != location)
 			continue;
 
-		//same thread as the promise
+		// same thread as the promise
 		if (act->get_tid() == tid) {
-			//make sure that the reader of this write happens after the promise
-			if (( read == NULL ) || ( promise->get_action() -> happens_before(read))) {
-				//do we have a pwrite for the promise, if not, set it
+			// make sure that the reader of this write happens after the promise
+			if ((read == NULL) || (promise->get_action()->happens_before(read))) {
+				// 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 the promise
+					// The pwrite cannot happen before the promise
 					if (write->happens_before(act) && (write != act)) {
 						priv->failed_promise = true;
 						return;
 					}
 				}
-			
+
 				if (mo_graph->checkPromise(write, promise)) {
 					priv->failed_promise = true;
 					return;
@@ -2457,12 +2476,12 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write,
 			}
 		}
 
-		//Don't do any lookups twice for the same thread
-		if (promise->has_sync_thread(tid))
+		// Don't do any lookups twice for the same thread
+		if (!promise->thread_is_available(tid))
 			continue;
 
 		if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
-			if (promise->increment_threads(tid)) {
+			if (promise->eliminate_thread(tid)) {
 				priv->failed_promise = true;
 				return;
 			}
@@ -2683,7 +2702,7 @@ Thread * ModelChecker::get_thread(thread_id_t tid) const
  * @param act The ModelAction
  * @return A Thread reference
  */
-Thread * ModelChecker::get_thread(ModelAction *act) const
+Thread * ModelChecker::get_thread(const ModelAction *act) const
 {
 	return get_thread(act->get_tid());
 }