ichange

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 954c07dd6dacdfc9473a4aa3f5e0a2f8db38bcbf..7c0575fe198f055f38849889df7c38b10cdc46f2 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -197,21 +197,33 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
        action_type type = act->get_type();
 
-       switch (type) {
-               case ATOMIC_READ:
-               case ATOMIC_WRITE:
-               case ATOMIC_RMW:
-                       break;
-               default:
-                       return NULL;
-       }
-       /* linear search: from most recent to oldest */
-       action_list_t *list = obj_map->get_safe_ptr(act->get_location());
-       action_list_t::reverse_iterator rit;
-       for (rit = list->rbegin(); rit != list->rend(); rit++) {
-               ModelAction *prev = *rit;
-               if (act->is_synchronizing(prev))
-                       return prev;
+       if (type==ATOMIC_READ||type==ATOMIC_WRITE||type==ATOMIC_RMW) {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (act->is_synchronizing(prev))
+                               return prev;
+               }
+       } else if (type==ATOMIC_LOCK||type==ATOMIC_TRYLOCK) {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (prev->is_success_lock())
+                               return prev;
+               }
+       } else if (type==ATOMIC_UNLOCK) {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (prev->is_failed_trylock())
+                               return prev;
+               }
        }
        return NULL;
 }
@@ -358,16 +370,18 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                curr = tmp;
                compute_promises(curr);
        } else {
-               ModelAction *tmp = node_stack->explore_action(curr);
+               ModelAction *tmp = node_stack->explore_action(curr, scheduler->get_enabled());
                if (tmp) {
                        /* Discard duplicate ModelAction; use action from NodeStack */
                        /* First restore type and order in case of RMW operation */
                        if (curr->is_rmwr())
                                tmp->copy_typeandorder(curr);
-
+                       
                        /* If we have diverged, we need to reset the clock vector. */
                        if (diverge == NULL)
                                tmp->create_cv(get_parent_action(tmp->get_tid()));
+                       
+                       ASSERT(curr->get_location()==tmp->get_location());
 
                        delete curr;
                        curr = tmp;
@@ -1321,25 +1335,23 @@ int ModelChecker::switch_to_master(ModelAction *act)
  * @return Returns true (success) if a step was taken and false otherwise.
  */
 bool ModelChecker::take_step() {
-       Thread *curr, *next;
-
        if (has_asserted())
                return false;
 
-       curr = thread_current();
+       Thread * curr = thread_current();
        if (curr) {
                if (curr->get_state() == THREAD_READY) {
                        ASSERT(priv->current_action);
 
                        priv->nextThread = check_current_action(priv->current_action);
                        priv->current_action = NULL;
-                       if (!curr->is_blocked() && !curr->is_complete())
-                               scheduler->add_thread(curr);
+                       if (curr->is_blocked() || curr->is_complete())
+                               scheduler->remove_thread(curr);
                } else {
                        ASSERT(false);
                }
        }
-       next = scheduler->next_thread(priv->nextThread);
+       Thread * next = scheduler->next_thread(priv->nextThread);
 
        /* Infeasible -> don't take any more steps */
        if (!isfeasible())