bug fixes for lock support...think it works now...

diff --git a/action.cc b/action.cc
index e5c9afe46f4cd81fff20555344b669c23c9b4bb1..3fda30de4bf7e425ac99fe95d5c30aca198965d5 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -27,6 +27,10 @@ ModelAction::~ModelAction()
                delete cv;
 }
 
+void ModelAction::copy_from_new(ModelAction *newaction) {
+       seq_number=newaction->seq_number;
+}
+
 bool ModelAction::is_mutex_op() const {
        return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
 }
@@ -180,6 +184,23 @@ bool ModelAction::is_synchronizing(const ModelAction *act) const
        return false;
 }
 
+bool ModelAction::is_conflicting_lock(const ModelAction *act) const
+{
+       //Must be different threads to reorder
+       if (same_thread(act))
+               return false;
+       
+       //Try to reorder a lock past a successful lock
+       if (act->is_success_lock())
+               return true;
+       
+       //Try to push a successful trylock past an unlock
+       if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS)
+               return true;
+
+       return false;
+}
+
 void ModelAction::create_cv(const ModelAction *parent)
 {
        if (cv)
@@ -278,6 +299,15 @@ void ModelAction::print(void) const
        case ATOMIC_INIT:
                type_str = "init atomic";
                break;
+       case ATOMIC_LOCK:
+               type_str = "lock";
+               break;
+       case ATOMIC_UNLOCK:
+               type_str = "unlock";
+               break;
+       case ATOMIC_TRYLOCK:
+               type_str = "trylock";
+               break;
        default:
                type_str = "unknown type";
        }

diff --git a/action.h b/action.h
index c5179bcfa81a77de58b79b5c57077a28d32cfb24..f83aec9583e230fd9fddbf10676b7b73113faa8e 100644 (file)
--- a/action.h
+++ b/action.h
@@ -72,6 +72,7 @@ public:
        Node * get_node() const { return node; }
        void set_node(Node *n) { node = n; }
 
+       void copy_from_new(ModelAction *newaction);
        void set_try_lock(bool obtainedlock);
        bool is_mutex_op() const;
        bool is_lock() const;
@@ -91,6 +92,7 @@ public:
        bool is_seqcst() const;
        bool same_var(const ModelAction *act) const;
        bool same_thread(const ModelAction *act) const;
+       bool is_conflicting_lock(const ModelAction *act) const;
        bool is_synchronizing(const ModelAction *act) const;
 
        void create_cv(const ModelAction *parent = NULL);

diff --git a/model.cc b/model.cc
index 4f2d9e0f314b8fbc451867ee5676f81292ab6353..02518eef53078cc2618a56e0f75d4c00a2a27ccc 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -217,7 +217,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
-                       if (prev->is_success_lock())
+                       if (act->is_conflicting_lock(prev))
                                return prev;
                }
        } else if (type==ATOMIC_UNLOCK) {
@@ -226,7 +226,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
-                       if (prev->is_failed_trylock())
+                       if (!act->same_thread(prev)&&prev->is_failed_trylock())
                                return prev;
                }
        }
@@ -235,35 +235,44 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 
 void ModelChecker::set_backtracking(ModelAction *act)
 {
-       ModelAction *prev;
-       Node *node;
        Thread *t = get_thread(act);
-
-       prev = get_last_conflict(act);
+       ModelAction * prev = get_last_conflict(act);
        if (prev == NULL)
                return;
 
-       node = prev->get_node()->get_parent();
-
-       while (!node->is_enabled(t))
-               t = t->get_parent();
-
-       /* Check if this has been explored already */
-       if (node->has_been_explored(t->get_id()))
-               return;
+       Node * node = prev->get_node()->get_parent();
 
-       /* Cache the latest backtracking point */
-       if (!priv->next_backtrack || *prev > *priv->next_backtrack)
-               priv->next_backtrack = prev;
+       int low_tid, high_tid;
+       if (node->is_enabled(t)) {
+               low_tid=id_to_int(act->get_tid());
+               high_tid=low_tid+1;
+       } else {
+               low_tid=0;
+               high_tid=get_num_threads();
+       }
+       
+       for(int i=low_tid;i<high_tid;i++) {
+               thread_id_t tid=int_to_id(i);
+               if (!node->is_enabled(tid))
+                       continue;
 
-       /* If this is a new backtracking point, mark the tree */
-       if (!node->set_backtrack(t->get_id()))
-               return;
-       DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-                       prev->get_tid(), t->get_id());
-       if (DBG_ENABLED()) {
-               prev->print();
-               act->print();
+               /* Check if this has been explored already */
+               if (node->has_been_explored(tid))
+                       continue;
+               
+               /* Cache the latest backtracking point */
+               if (!priv->next_backtrack || *prev > *priv->next_backtrack)
+                       priv->next_backtrack = prev;
+               
+               /* If this is a new backtracking point, mark the tree */
+               if (!node->set_backtrack(tid))
+                       continue;
+               DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
+                                       prev->get_tid(), t->get_id());
+               if (DBG_ENABLED()) {
+                       prev->print();
+                       act->print();
+               }
        }
 }
 
@@ -423,6 +432,7 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                        newcurr->copy_typeandorder(curr);
 
                ASSERT(curr->get_location()==newcurr->get_location());
+               newcurr->copy_from_new(curr);
 
                /* Discard duplicate ModelAction; use action from NodeStack */
                delete curr;

diff --git a/nodestack.cc b/nodestack.cc
index b79863e2abbcc443e76721360724cc1c800d9b61..715dbb23d051badd48b84b31218c95c97a213425 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -224,6 +224,12 @@ bool Node::is_enabled(Thread *t)
        return thread_id < num_threads && enabled_array[thread_id];
 }
 
+bool Node::is_enabled(thread_id_t tid)
+{
+       int thread_id=id_to_int(tid);
+       return thread_id < num_threads && enabled_array[thread_id];
+}
+
 /**
  * Add an action to the may_read_from set.
  * @param act is the action to add

diff --git a/nodestack.h b/nodestack.h
index 3262a569d0e5da24689c46c706752a3b718c9a69..a06bef40570556ddbf52bff19959423aaca159a6 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -56,6 +56,7 @@ public:
        bool set_backtrack(thread_id_t id);
        thread_id_t get_next_backtrack();
        bool is_enabled(Thread *t);
+       bool is_enabled(thread_id_t tid);
        ModelAction * get_action() { return action; }
 
        /** @return the parent Node to this Node; that is, the action that