error

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 0006fd63d66e172336df1296c417a787fe559d2a..c01122191d0e712750b382f87b9c0edbfecf9aa2 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -188,10 +188,11 @@ bool ModelChecker::next_execution()
        DBG();
 
        num_executions++;
+
        if (isfinalfeasible()) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
-                       earliest_diverge->print();
+                       earliest_diverge->print(false);
                else
                        printf("(Not set)\n");
 
@@ -199,6 +200,9 @@ 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();
 
@@ -430,7 +434,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
                action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
                //activate all the waiting threads
                for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
-                       scheduler->add_thread(get_thread((*rit)->get_tid()));
+                       scheduler->wake(get_thread(*rit));
                }
                waiters->clear();
                break;
@@ -475,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: {
@@ -496,7 +500,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                        scheduler->sleep(waiting);
                } else {
                        do_complete_join(curr);
-                       synchronized = true;
+                       updated = true; /* trigger rel-seq checks */
                }
                break;
        }
@@ -507,9 +511,10 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                        Thread *wake = get_thread(act);
                        scheduler->wake(wake);
                        do_complete_join(act);
-                       synchronized = true;
+                       updated = true; /* trigger rel-seq checks */
                }
                th->complete();
+               updated = true; /* trigger rel-seq checks */
                break;
        }
        case THREAD_START: {
@@ -520,7 +525,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                break;
        }
 
-       return synchronized;
+       return updated;
 }
 
 /**
@@ -547,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 */
@@ -619,7 +626,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                /* Make the execution look like we chose to run this action
                 * much later, when a lock is actually available to release */
                get_current_thread()->set_pending(curr);
-               remove_thread(get_current_thread());
+               scheduler->sleep(get_current_thread());
                return get_next_thread(NULL);
        }
 
@@ -1321,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));
 
@@ -1472,6 +1481,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        //Make sure the promise's value matches the write's value
                        ASSERT(promise->get_value() == write->get_value());
 
+                       delete(promise);
                        promises->erase(promises->begin() + promise_index);
                        resolved = true;
                } else