From 802e014ba228bb6bc689ff1d31e8423097be9826 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 23 Aug 2012 17:54:39 -0700 Subject: [PATCH] model: re-check release sequences lazily For now, I write this "lazy check" as follows: Whenever one of the following occurs: * a Promise is fulfilled * a mo_graph edge is added Then I recheck all the actions (for the relevant object location) that are waiting in the lazy release head queue. --- model.cc | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/model.cc b/model.cc index 69cffcdb..6ded3f5d 100644 --- a/model.cc +++ b/model.cc @@ -320,13 +320,15 @@ void ModelChecker::check_current_action(void) /* Assign reads_from values */ Thread *th = get_thread(curr->get_tid()); uint64_t value = VALUE_NONE; + bool updated = false; if (curr->is_read()) { const ModelAction *reads_from = curr->get_node()->get_read_from(); if (reads_from != NULL) { value = reads_from->get_value(); /* Assign reads_from, perform release/acquire synchronization */ curr->read_from(reads_from); - r_modification_order(curr,reads_from); + if (r_modification_order(curr,reads_from)) + updated = true; } else { /* Read from future value */ value = curr->get_node()->get_future_value(); @@ -335,10 +337,15 @@ void ModelChecker::check_current_action(void) promises->push_back(valuepromise); } } else if (curr->is_write()) { - w_modification_order(curr); - resolve_promises(curr); + if (w_modification_order(curr)) + updated = true;; + if (resolve_promises(curr)) + updated = true; } + if (updated) + resolve_release_sequences(curr->get_location()); + th->set_return_value(value); /* Add action to list. */ -- 2.34.1