model: bugfix - correct the "equality" check for RR coherence

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index ae3788945c7756881178b1657bb215cf5a71901a..152e36ec2f296fc9f467b890e2e89d6ada3504ee 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -282,6 +282,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                                earliest_diverge = prevnode->get_action();
                        }
                }
+               /* Start the round robin scheduler from this thread id */
+               scheduler->set_scheduler_thread(tid);
                /* The correct sleep set is in the parent node. */
                execute_sleep_set();
 
@@ -1111,7 +1113,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
        case THREAD_CREATE: {
                thrd_t *thrd = (thrd_t *)curr->get_location();
                struct thread_params *params = (struct thread_params *)curr->get_value();
-               Thread *th = new Thread(thrd, params->func, params->arg);
+               Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr));
                add_thread(th);
                th->set_creation(curr);
                /* Promises can be satisfied by children */
@@ -1325,6 +1327,30 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
        return false;
 }
 
+/**
+ * Check promises and eliminate potentially-satisfying threads when a thread is
+ * blocked (e.g., join, lock). A thread which is waiting on another thread can
+ * no longer satisfy a promise generated from that thread.
+ *
+ * @param blocker The thread on which a thread is waiting
+ * @param waiting The waiting thread
+ */
+void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
+{
+       for (unsigned int i = 0; i < promises->size(); i++) {
+               Promise *promise = (*promises)[i];
+               ModelAction *reader = promise->get_action();
+               if (reader->get_tid() != blocker->get_id())
+                       continue;
+               if (!promise->thread_is_available(waiting->get_id()))
+                       continue;
+               if (promise->eliminate_thread(waiting->get_id())) {
+                       /* Promise has failed */
+                       priv->failed_promise = true;
+               }
+       }
+}
+
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -1348,6 +1374,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
                Thread *blocking = (Thread *)curr->get_location();
                if (!blocking->is_complete()) {
                        blocking->push_wait_list(curr);
+                       thread_blocking_check_promises(blocking, get_thread(curr));
                        return false;
                }
        }
@@ -1738,13 +1765,13 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                                                added = mo_graph->addEdge(act, rf) || added;
                                        }
                                } else {
-                                       const ModelAction *prevreadfrom = act->get_reads_from();
-                                       //if the previous read is unresolved, keep going...
-                                       if (prevreadfrom == NULL)
-                                               continue;
-
-                                       if (!prevreadfrom->equals(rf)) {
-                                               added = mo_graph->addEdge(prevreadfrom, rf) || added;
+                                       const ModelAction *prevrf = act->get_reads_from();
+                                       const Promise *prevrf_promise = act->get_reads_from_promise();
+                                       if (prevrf) {
+                                               if (!prevrf->equals(rf))
+                                                       added = mo_graph->addEdge(prevrf, rf) || added;
+                                       } else if (!prevrf_promise->equals(rf)) {
+                                               added = mo_graph->addEdge(prevrf_promise, rf) || added;
                                        }
                                }
                                break;
@@ -2420,7 +2447,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        read_from(read, write);
                        //Make sure the promise's value matches the write's value
                        ASSERT(promise->is_compatible(write));
-                       mo_graph->resolvePromise(read, write, &mustResolve);
+                       mo_graph->resolvePromise(promise, write, &mustResolve);
 
                        resolved.push_back(promise);
                        promises->erase(promises->begin() + promise_index);
@@ -2460,11 +2487,10 @@ void ModelChecker::compute_promises(ModelAction *curr)
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
                const ModelAction *act = promise->get_action();
+               ASSERT(act->is_read());
                if (!act->happens_before(curr) &&
-                               act->is_read() &&
                                !act->could_synchronize_with(curr) &&
-                               !act->same_thread(curr) &&
-                               act->get_location() == curr->get_location() &&
+                               promise->is_compatible(curr) &&
                                promise->get_value() == curr->get_value()) {
                        curr->get_node()->set_promise(i, act->is_rmw());
                }
@@ -2888,7 +2914,7 @@ void ModelChecker::run()
 {
        do {
                thrd_t user_thread;
-               Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
+               Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL, NULL);
                add_thread(t);
 
                do {