From 8669bd6f88178382893b48223498611f2200714a Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sun, 7 Oct 2012 15:04:08 -0700 Subject: [PATCH] model: disabled threads are "future ordered" If a Thread is not currently enabled, then it will synchronize with another (currently-enabled) Thread if/when it wakes up. Thus, it qualifies as "future ordered" within the release sequence code: it cannot contribute future writes that will break current pending release sequences. --- model.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/model.cc b/model.cc index 2260431..6eaf656 100644 --- a/model.cc +++ b/model.cc @@ -1258,8 +1258,10 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, bool future_ordered = false; ModelAction *last = get_last_action(int_to_id(i)); - if (last && (rf->happens_before(last) || - get_thread(int_to_id(i))->is_complete())) + Thread *th = get_thread(int_to_id(i)); + if ((last && rf->happens_before(last)) || + !scheduler->is_enabled(th) || + th->is_complete()) future_ordered = true; for (rit = list->rbegin(); rit != list->rend(); rit++) { -- 2.34.1