From a7472bf7d514d8c53b22eb64bc552f593c79d506 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 2 Oct 2012 18:09:40 -0700 Subject: [PATCH] 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. --- model.cc | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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; } /** -- 2.34.1