model: re-check release sequences after THREAD_JOIN

If a THREAD-specific operation (from process_thread_action()) added any
synchronization, we should re-check all release sequences.

diff --git a/model.cc b/model.cc
index 2b902ba809106795e77791bde5d500653934ed43..3593cef7b6be2c7373941bb6275cf510e9a67ecf 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -626,7 +626,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        bool update = false; /* update this location's release seq's */
                        bool update_all = false; /* update all release seq's */
 
-                       process_thread_action(curr);
+                       if (process_thread_action(curr))
+                               update_all = true;
 
                        if (act->is_read() && process_read(act, second_part_of_rmw))
                                update = true;