From 5236350c6c02c09a167a461fce69c581768f9c03 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 25 Sep 2012 16:56:02 -0700 Subject: [PATCH] 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. --- model.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index 2b902ba8..3593cef7 100644 --- 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; -- 2.34.1