From 663a0dcbf36fd68a8d5783fcf7b218d17e2f9aad Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 20 Sep 2012 10:47:31 -0700 Subject: [PATCH] model: release sequences: check last action in each thread Previously, release_seq_head would only examine actions on a particular, given object to determine a release sequence. However, we can get information regarding the possibility of future disruptive writes by checking the clock vector of the last action of each thread, regardless of object. --- model.cc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/model.cc b/model.cc index a7c99af..d2fc366 100644 --- a/model.cc +++ b/model.cc @@ -1118,6 +1118,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel * the release seq? */ bool future_ordered = false; + ModelAction *last = get_last_action(int_to_id(i)); + if (last && rf->happens_before(last)) + future_ordered = true; + for (rit = list->rbegin(); rit != list->rend(); rit++) { const ModelAction *act = *rit; if (!act->is_write()) -- 2.34.1