X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=9611f2f615845c926485dd732ce26b026585c085;hp=00982130b042f16add374761d180f717a51900a7;hb=1bc8782b55cab0503f1b64529f993f0b9e3a1846;hpb=0c61161a061c85189d4d1531a9ad00caf2f2588d

diff --git a/model.cc b/model.cc
index 00982130..9611f2f6 100644
--- a/model.cc
+++ b/model.cc
@@ -292,8 +292,9 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
 		} else {
 			/* Read from future value */
 			value = curr->get_node()->get_future_value();
+			modelclock_t expiration = curr->get_node()->get_future_value_expiration();
 			curr->read_from(NULL);
-			Promise *valuepromise = new Promise(curr, value);
+			Promise *valuepromise = new Promise(curr, value, expiration);
 			promises->push_back(valuepromise);
 		}
 		th->set_return_value(value);
@@ -428,6 +429,16 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	return get_next_thread(curr);
 }
 
+bool ModelChecker::promises_expired() {
+	for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
+		Promise *promise = (*promises)[promise_index];
+		if (promise->get_expiration()<priv->used_sequence_numbers) {
+			return true;
+		}
+	}
+	return false;
+}
+
 /** @returns whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
@@ -436,7 +447,7 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
-	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads;
+	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -685,7 +696,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				   =>
 				   that read could potentially read from our write.
 				 */
-				if (isfeasible() && act->get_node()->add_future_value(curr->get_value()) &&
+				if (isfeasible() && act->get_node()->add_future_value(curr->get_value(), curr->get_seq_number()+params.maxfuturedelay) &&
 						(!priv->next_backtrack || *act > *priv->next_backtrack))
 					priv->next_backtrack = act;
 			}