From ce35fd211d8af2b55dfa6fffc9c09036f3313dcf Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 5 Oct 2012 19:20:21 -0700 Subject: [PATCH] model: launch release sequence fixup actions when necessary This should complete the "release sequence fixup" step. The ModelChecker will launch new fixup actions, associating them with the special 'model_thread'. --- model.cc | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/model.cc b/model.cc index c1818ad..1fcb8fc 100644 --- a/model.cc +++ b/model.cc @@ -1971,6 +1971,18 @@ bool ModelChecker::take_step() { DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, next ? id_to_int(next->get_id()) : -1); + /* When no more threads, or when execution replay chooses the + * 'model_thread': launch end-of-execution release sequence fixups */ + if (!pending_rel_seqs->empty() && (!next || next->is_model_thread())) { + printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n", + pending_rel_seqs->size()); + ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, + std::memory_order_seq_cst, NULL, VALUE_NONE, + model_thread); + set_current_action(fixup); + return true; + } + /* next == NULL -> don't take any more steps */ if (!next) return false; -- 2.34.1