bug fixes for lock support...think it works now...
authorBrian Demsky <bdemsky@uci.edu>
Thu, 20 Sep 2012 08:20:34 +0000 (01:20 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Thu, 20 Sep 2012 08:20:34 +0000 (01:20 -0700)
action.cc
action.h
model.cc
nodestack.cc
nodestack.h

index e5c9afe..3fda30d 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";
        }
index c5179bc..f83aec9 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);
index 4f2d9e0..02518ee 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;
index b79863e..715dbb2 100644 (file)
@@ -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
index 3262a56..a06bef4 100644 (file)
@@ -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