nodestack: add release sequence breakage backtracking

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index e8b860c2c5058a0daf3f42ada4ba42d470a80b0e..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++) {
@@ -1539,6 +1541,10 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                } else
                        promise_index++;
        }
+
+       //Check whether reading these writes has made threads unable to
+       //resolve promises
+
        for(unsigned int i=0;i<threads_to_check.size();i++)
                mo_check_promises(threads_to_check[i], write);
 
@@ -1558,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);
@@ -1583,7 +1589,33 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
        }
 }
 
-/** Checks promises in response to change in ClockVector Threads. */
+/** Checks promises in response to addition to modification order for threads.
+ * Definitions:
+ * pthread is the thread that performed the read that created the promise
+ * 
+ * pread is the read that created the promise
+ *
+ * pwrite is either the first write to same location as pread by
+ * pthread that is sequenced after pread or the value read by the
+ * first read to the same lcoation as pread by pthread that is
+ * sequenced after pread..
+ *
+ *     1. If tid=pthread, then we check what other threads are reachable
+ * through the mode order starting with pwrite.  Those threads cannot
+ * perform a write that will resolve the promise due to modification
+ * order constraints.
+ *
+ * 2. If the tid is not pthread, we check whether pwrite can reach the
+ * action write through the modification order.  If so, that thread
+ * cannot perform a future write that will resolve the promise due to
+ * modificatin order constraints.
+ *
+ *     @parem tid The thread that either read from the model action
+ *     write, or actually did the model action write.
+ *
+ *     @parem write The ModelAction representing the relevant write.
+ */
+
 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
        void * location = write->get_location();
        for (unsigned int i = 0; i < promises->size(); i++) {
@@ -1594,7 +1626,10 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
                if ( act->get_location() != location )
                        continue;
 
-               if ( act->get_tid()==tid) {
+               //same thread as the promise
+               if ( act->get_tid()==tid ) {
+
+                       //do we have a pwrite for the promise, if not, set it
                        if (promise->get_write() == NULL ) {
                                promise->set_write(write);
                        }