model: debug print - pending release sequences

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 097da8ae9b7c66fae010db5c95d3a6245622f3cc..4d6d7634bf26c58eb83e2070b99df902c05b41ba 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -139,6 +139,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
        ModelAction *next = node_stack->get_next()->get_action();
 
        if (next == diverge) {
+               if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+                       earliest_diverge=diverge;
+
                Node *nextnode = next->get_node();
                /* Reached divergence point */
                if (nextnode->increment_promise()) {
@@ -158,8 +161,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        Node *node = nextnode->get_parent();
                        tid = node->get_next_backtrack();
                        node_stack->pop_restofstack(1);
+                       if (diverge==earliest_diverge) {
+                               earliest_diverge=node->get_action();
+                       }
                }
                DEBUG("*** Divergence point ***\n");
+
                diverge = NULL;
        } else {
                tid = next->get_tid();
@@ -181,6 +188,7 @@ bool ModelChecker::next_execution()
        DBG();
 
        num_executions++;
+
        if (isfinalfeasible()) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
@@ -192,15 +200,15 @@ bool ModelChecker::next_execution()
                num_feasible_executions++;
        }
 
+       DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+                       pending_acq_rel_seq->size());
+
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
 
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
-       if (earliest_diverge == NULL || *diverge < *earliest_diverge)
-               earliest_diverge=diverge;
-
        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
                diverge->print();
@@ -471,11 +479,11 @@ bool ModelChecker::process_write(ModelAction *curr)
  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
  *
  * @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated or a thread completed
  */
 bool ModelChecker::process_thread_action(ModelAction *curr)
 {
-       bool synchronized = false;
+       bool updated = false;
 
        switch (curr->get_type()) {
        case THREAD_CREATE: {
@@ -484,19 +492,29 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                break;
        }
        case THREAD_JOIN: {
-               Thread *blocking = (Thread *)curr->get_location();
-               ModelAction *act = get_last_action(blocking->get_id());
-               curr->synchronize_with(act);
-               synchronized = true;
+               Thread *waiting, *blocking;
+               waiting = get_thread(curr);
+               blocking = (Thread *)curr->get_location();
+               if (!blocking->is_complete()) {
+                       blocking->push_wait_list(curr);
+                       scheduler->sleep(waiting);
+               } else {
+                       do_complete_join(curr);
+                       updated = true; /* trigger rel-seq checks */
+               }
                break;
        }
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
                while (!th->wait_list_empty()) {
                        ModelAction *act = th->pop_wait_list();
-                       scheduler->wake(get_thread(act));
+                       Thread *wake = get_thread(act);
+                       scheduler->wake(wake);
+                       do_complete_join(act);
+                       updated = true; /* trigger rel-seq checks */
                }
                th->complete();
+               updated = true; /* trigger rel-seq checks */
                break;
        }
        case THREAD_START: {
@@ -507,7 +525,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                break;
        }
 
-       return synchronized;
+       return updated;
 }
 
 /**
@@ -534,6 +552,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                return newcurr;
        }
 
+       curr->set_seq_number(get_next_seq_num());
+
        newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
        if (newcurr) {
                /* First restore type and order in case of RMW operation */
@@ -564,12 +584,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 }
 
 /**
- * @brief Check whether a model action is enabled.
- *
- * Checks whether a lock or join operation would be successful (i.e., is the
- * lock already locked, or is the joined thread already complete). If not, put
- * the action in a waiter list.
- *
+ * This method checks whether a model action is enabled at the given point.
+ * At this point, it checks whether a lock operation would be successful at this point.
+ * If not, it puts the thread in a waiter list.
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
  */
@@ -582,12 +599,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
                        lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
                        return false;
                }
-       } else if (curr->get_type() == THREAD_JOIN) {
-               Thread *blocking = (Thread *)curr->get_location();
-               if (!blocking->is_complete()) {
-                       blocking->push_wait_list(curr);
-                       return false;
-               }
        }
 
        return true;
@@ -613,7 +624,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
        if (!check_action_enabled(curr)) {
                /* Make the execution look like we chose to run this action
-                * much later, when a lock/join can succeed */
+                * much later, when a lock is actually available to release */
                get_current_thread()->set_pending(curr);
                scheduler->sleep(get_current_thread());
                return get_next_thread(NULL);
@@ -697,6 +708,19 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        return get_next_thread(curr);
 }
 
+/**
+ * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
+ * operation from the Thread it is joining with. Must be called after the
+ * completion of the Thread in question.
+ * @param join The THREAD_JOIN action
+ */
+void ModelChecker::do_complete_join(ModelAction *join)
+{
+       Thread *blocking = (Thread *)join->get_location();
+       ModelAction *act = get_last_action(blocking->get_id());
+       join->synchronize_with(act);
+}
+
 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
@@ -1304,6 +1328,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                }
 
                if (updated) {
+                       /* Re-check all pending release sequences */
+                       work_queue->push_back(CheckRelSeqWorkEntry(NULL));
                        /* Re-check act for mo_graph edges */
                        work_queue->push_back(MOEdgeWorkEntry(act));