model: merge duplicated code for WAIT and UNLOCK

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 167ea947a79a020964ec13fc67d67077aae961f7..4a35fcd51ac965993c4194734107ddccbdae084b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -260,20 +260,8 @@ Thread * ModelChecker::get_next_thread()
                scheduler->update_sleep_set(prevnode);
 
                /* Reached divergence point */
-               if (nextnode->increment_misc()) {
-                       /* The next node will try to satisfy a different misc_index values. */
-                       tid = next->get_tid();
-                       node_stack->pop_restofstack(2);
-               } else if (nextnode->increment_promise()) {
-                       /* The next node will try to satisfy a different set of promises. */
-                       tid = next->get_tid();
-                       node_stack->pop_restofstack(2);
-               } else if (nextnode->increment_read_from()) {
-                       /* The next node will read from a different value. */
-                       tid = next->get_tid();
-                       node_stack->pop_restofstack(2);
-               } else if (nextnode->increment_relseq_break()) {
-                       /* The next node will try to resolve a release sequence differently */
+               if (nextnode->increment_behaviors()) {
+                       /* Execute the same thread with a new behavior */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
                } else {
@@ -409,22 +397,6 @@ bool ModelChecker::is_deadlocked() const
        return blocking_threads;
 }
 
-/**
- * Check if a Thread has entered a circular wait deadlock situation. This will
- * not check other threads for potential deadlock situations, and may miss
- * deadlocks involving WAIT.
- *
- * @param t The thread which may have entered a deadlock
- * @return True if this Thread entered a deadlock; false otherwise
- */
-bool ModelChecker::is_circular_wait(const Thread *t) const
-{
-       for (Thread *waiting = t->waiting_on() ; waiting != NULL; waiting = waiting->waiting_on())
-               if (waiting == t)
-                       return true;
-       return false;
-}
-
 /**
  * Check if this is a complete execution. That is, have all thread completed
  * execution (rather than exiting because sleep sets have forced a redundant
@@ -996,32 +968,25 @@ bool ModelChecker::process_mutex(ModelAction *curr)
                }
                break;
        }
+       case ATOMIC_WAIT:
        case ATOMIC_UNLOCK: {
                //unlock the lock
                state->locked = NULL;
                //wake up the other threads
-               action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
-               //activate all the waiting threads
-               for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
-                       scheduler->wake(get_thread(*rit));
-               }
-               waiters->clear();
-               break;
-       }
-       case ATOMIC_WAIT: {
-               //unlock the lock
-               state->locked = NULL;
-               //wake up the other threads
-               action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
+               action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, mutex);
                //activate all the waiting threads
                for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
                        scheduler->wake(get_thread(*rit));
                }
                waiters->clear();
-               //check whether we should go to sleep or not...simulate spurious failures
+
+               if (!curr->is_wait())
+                       break; /* The rest is only for ATOMIC_WAIT */
+
+               /* Should we go to sleep? (simulate spurious failures) */
                if (curr->get_node()->get_misc() == 0) {
                        get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
-                       //disable us
+                       /* disable us */
                        scheduler->sleep(get_thread(curr));
                }
                break;
@@ -1056,7 +1021,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
  *
  * If one of the following is true:
  *  (a) there are no pending promises
- *  (b) the reader is ordered after the latest Promise creation
+ *  (b) the reader and writer do not cross any promises
  * Then, it is safe to pass a future value back now.
  *
  * Otherwise, we must save the pending future value until (a) or (b) is true
@@ -1068,8 +1033,18 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 bool ModelChecker::promises_may_allow(const ModelAction *writer,
                const ModelAction *reader) const
 {
-       return promises->empty() ||
-               *(promises->back()->get_reader(0)) < *reader;
+       if (promises->empty())
+               return true;
+       for(int i=promises->size()-1;i>=0;i--) {
+               ModelAction *pr=(*promises)[i]->get_reader(0);
+               //reader is after promise...doesn't cross any promise
+               if (*reader > *pr)
+                       return true;
+               //writer is after promise, reader before...bad...
+               if (*writer > *pr)
+                       return false;
+       }
+       return true;
 }
 
 /**
@@ -1490,7 +1465,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
                        get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
                        return false;
                }
-       } else if (curr->get_type() == THREAD_JOIN) {
+       } else if (curr->is_thread_join()) {
                Thread *blocking = (Thread *)curr->get_location();
                if (!blocking->is_complete()) {
                        blocking->push_wait_list(curr);
@@ -3159,7 +3134,7 @@ void ModelChecker::run()
                                Thread *thr = get_thread(tid);
                                if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
                                        switch_from_master(thr);
-                                       if (is_circular_wait(thr))
+                                       if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected");
                                }
                        }