From: Brian Norris <banorris@uci.edu>
Date: Wed, 3 Oct 2012 01:09:40 +0000 (-0700)
Subject: model: THREAD_FINISH triggers release sequence check
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=a7472bf7d514d8c53b22eb64bc552f593c79d506

model: THREAD_FINISH triggers release sequence check

A THREAD_FINISH action may ensure that a Thread is no longer able to
break release sequences, so all pending release sequences should be
checked.
---

diff --git a/model.cc b/model.cc
index 4f600a91..e3d26d32 100644
--- a/model.cc
+++ b/model.cc
@@ -475,11 +475,11 @@ bool ModelChecker::process_write(ModelAction *curr)
  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
  *
  * @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated or a thread completed
  */
 bool ModelChecker::process_thread_action(ModelAction *curr)
 {
-	bool synchronized = false;
+	bool updated = false;
 
 	switch (curr->get_type()) {
 	case THREAD_CREATE: {
@@ -491,7 +491,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		Thread *blocking = (Thread *)curr->get_location();
 		ModelAction *act = get_last_action(blocking->get_id());
 		curr->synchronize_with(act);
-		synchronized = true;
+		updated = true; /* trigger rel-seq checks */
 		break;
 	}
 	case THREAD_FINISH: {
@@ -501,6 +501,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 			scheduler->wake(get_thread(act));
 		}
 		th->complete();
+		updated = true; /* trigger rel-seq checks */
 		break;
 	}
 	case THREAD_START: {
@@ -511,7 +512,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		break;
 	}
 
-	return synchronized;
+	return updated;
 }
 
 /**