nodestack: add release sequence breakage backtracking

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index bcc4298b6180618259f08b241c0ba0445fbd6532..6eaf65606b6fbfb96f79946836bfae5da2db7b2c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -207,7 +207,7 @@ bool ModelChecker::next_execution()
                num_feasible_executions++;
        }
 
-       DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+       DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
                        pending_rel_seqs->size());
 
        if (isfinalfeasible() || DBG_ENABLED())
@@ -236,7 +236,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
-                       if (act->is_synchronizing(prev))
+                       if (prev->could_synchronize_with(act))
                                return prev;
                }
                break;
@@ -1114,7 +1114,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                }
                                added = true;
                                break;
-                       } else if (act->is_read() && !act->is_synchronizing(curr) &&
+                       } else if (act->is_read() && !act->could_synchronize_with(curr) &&
                                                     !act->same_thread(curr)) {
                                /* We have an action that:
                                   (1) did not happen before us
@@ -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++) {
@@ -1562,7 +1564,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
                const ModelAction *act = promise->get_action();
                if (!act->happens_before(curr) &&
                                act->is_read() &&
-                               !act->is_synchronizing(curr) &&
+                               !act->could_synchronize_with(curr) &&
                                !act->same_thread(curr) &&
                                promise->get_value() == curr->get_value()) {
                        curr->get_node()->set_promise(i);