From: Brian Norris <banorris@uci.edu>
Date: Thu, 24 Jan 2013 02:47:53 +0000 (-0800)
Subject: model: modify promises on THREAD_{CREATE,FINISH}
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d2985e8129a69c7fb28c080272988485830c2bd9;p=cdsspec-compiler.git

model: modify promises on THREAD_{CREATE,FINISH}

When a thread is created it *must* pass its promise satisfiability to
its children.

When a thread finishes, we should remove it from all promises. This can
help prune a search early, if some read was depending only on the
finishing thread: we can then declare an unresolved promise.
---

diff --git a/model.cc b/model.cc
index 9aaab91..6453d53 100644
--- a/model.cc
+++ b/model.cc
@@ -968,6 +968,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: {
@@ -984,6 +990,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;
 	}