model: remove unnecessary boolean variable

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 824e1e430c7e29c983a380a92ae821ddc425c721..b916d8cf3e2c3d169c11e361715c46407ace3cd5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1307,9 +1307,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re
 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
 {
        const ModelAction *rf = act->get_reads_from();
-       bool complete;
-       complete = release_seq_heads(rf, release_heads);
-       if (!complete) {
+
+       if (!release_seq_heads(rf, release_heads)) {
                /* add act to 'lazy checking' list */
                pending_acq_rel_seq->push_back(act);
        }
@@ -1490,6 +1489,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid)
 bool ModelChecker::resolve_promises(ModelAction *write)
 {
        bool resolved = false;
+  std::vector<thread_id_t> threads_to_check;
 
        for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
                Promise *promise = (*promises)[promise_index];
@@ -1507,14 +1507,18 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        post_r_modification_order(read, write);
                        //Make sure the promise's value matches the write's value
                        ASSERT(promise->get_value() == write->get_value());
-                       mo_check_promises(read->get_tid(), write);
-
                        delete(promise);
+                       
                        promises->erase(promises->begin() + promise_index);
+                       threads_to_check.push_back(read->get_tid());
+
                        resolved = true;
                } else
                        promise_index++;
        }
+       for(unsigned int i=0;i<threads_to_check.size();i++)
+               mo_check_promises(threads_to_check[i], write);
+
        return resolved;
 }