model: one release sequence may help resolve another

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 744fec5e17a27ef75b07a2bca068ff344e951ee8..38f40e5cd1ee55b47103883fa9677b6ad7ea7e6d 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();
@@ -198,9 +205,6 @@ bool ModelChecker::next_execution()
        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 +475,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: {
@@ -487,7 +491,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                Thread *blocking = (Thread *)curr->get_location();
                ModelAction *act = get_last_action(blocking->get_id());
                curr->synchronize_with(act);
-               synchronized = true;
+               updated = true; /* trigger rel-seq checks */
                break;
        }
        case THREAD_FINISH: {
@@ -497,6 +501,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                        scheduler->wake(get_thread(act));
                }
                th->complete();
+               updated = true; /* trigger rel-seq checks */
                break;
        }
        case THREAD_START: {
@@ -507,7 +512,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                break;
        }
 
-       return synchronized;
+       return updated;
 }
 
 /**
@@ -1306,6 +1311,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));