model: use get_thread() helper

[cdsspec-compiler.git] / model.cc

diff --git a/model.cc b/model.cc
index 879f1dea17d162b38ca240e4c628043ed00001c3..6a79ad4a90f80ff1ee3177511683cd96c67ebb54 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -83,7 +83,6 @@ ModelChecker::ModelChecker(struct model_params params) :
        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),
        obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
-       lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
        condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
        obj_thrd_map(new HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4 >()),
        promises(new SnapVector<Promise *>()),
@@ -109,7 +108,6 @@ ModelChecker::~ModelChecker()
 
        delete obj_thrd_map;
        delete obj_map;
-       delete lock_waiters_map;
        delete condvar_waiters_map;
        delete action_trace;
 
@@ -260,20 +258,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 {
@@ -300,7 +286,7 @@ Thread * ModelChecker::get_next_thread()
        }
        DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
        ASSERT(tid != THREAD_ID_T_NONE);
-       return thread_map->get(id_to_int(tid));
+       return get_thread(id_to_int(tid));
 }
 
 /**
@@ -980,32 +966,26 @@ 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));
+               /* wake up the other threads */
+               for (unsigned int i = 0; i < get_num_threads(); i++) {
+                       Thread *t = get_thread(int_to_id(i));
+                       Thread *curr_thrd = get_thread(curr);
+                       if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+                               scheduler->wake(t);
                }
-               waiters->clear();
-               break;
-       }
-       case ATOMIC_WAIT: {
-               //unlock the lock
+
+               /* unlock the lock - after checking who was waiting on it */
                state->locked = NULL;
-               //wake up the other threads
-               action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
-               //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;
@@ -1239,9 +1219,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
        }
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
-               while (!th->wait_list_empty()) {
-                       ModelAction *act = th->pop_wait_list();
-                       scheduler->wake(get_thread(act));
+               /* Wake up any joining threads */
+               for (unsigned int i = 0; i < get_num_threads(); i++) {
+                       Thread *waiting = get_thread(int_to_id(i));
+                       if (waiting->waiting_on() == th &&
+                                       waiting->get_pending()->is_thread_join())
+                               scheduler->wake(waiting);
                }
                th->complete();
                /* Completed thread can't satisfy promises */
@@ -1477,17 +1460,13 @@ void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiti
  */
 bool ModelChecker::check_action_enabled(ModelAction *curr) {
        if (curr->is_lock()) {
-               std::mutex *lock = (std::mutex *)curr->get_location();
+               std::mutex *lock = curr->get_mutex();
                struct std::mutex_state *state = lock->get_state();
-               if (state->locked) {
-                       //Stick the action in the appropriate waiting queue
-                       get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
+               if (state->locked)
                        return false;
-               }
-       } else if (curr->get_type() == THREAD_JOIN) {
-               Thread *blocking = (Thread *)curr->get_location();
+       } else if (curr->is_thread_join()) {
+               Thread *blocking = curr->get_thread_operand();
                if (!blocking->is_complete()) {
-                       blocking->push_wait_list(curr);
                        thread_blocking_check_promises(blocking, get_thread(curr));
                        return false;
                }