more changes towards locks

diff --git a/action.cc b/action.cc
index 1e28264fbcedf171c673bace33be6f41c3aa3f35..2d9186d2f812bdbbe0e7eab770e1e813b79386fe 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -27,6 +27,14 @@ ModelAction::~ModelAction()
                delete cv;
 }
 
+bool ModelAction::is_success_lock() const {
+       return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
+}
+
+bool ModelAction::is_failed_trylock() const {
+       return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
+}
+
 bool ModelAction::is_read() const
 {
        return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW;

diff --git a/action.h b/action.h
index 0e3f3d572792303444c2e4efa3cce73326135039..753860984a2f2df79869deb11bb0053fdb05d7a5 100644 (file)
--- a/action.h
+++ b/action.h
@@ -24,6 +24,8 @@ using std::memory_order_seq_cst;
                hence by iteself does not indicate no value. */
 
 #define VALUE_NONE 1234567890
+#define VALUE_TRYSUCCESS 1
+#define VALUE_TRYFAILED 0
 
 /** @brief Represents an action type, identifying one of several types of
  * ModelAction */
@@ -70,6 +72,8 @@ public:
        Node * get_node() const { return node; }
        void set_node(Node *n) { node = n; }
 
+       bool is_success_lock() const;
+       bool is_failed_trylock() const;
        bool is_read() const;
        bool is_write() const;
        bool is_rmwr() const;

diff --git a/model.cc b/model.cc
index ede3797b7f4933f1c16f0a054d8b558ef63baff1..007492286587d6a3ea9c619c191b30a3644b1007 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -33,6 +33,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        lazy_sync_with_release(new HashTable<void *, std::list<ModelAction *>, uintptr_t, 4>()),
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
+       is_enabled(NULL),
        mo_graph(new CycleGraph()),
        failed_promise(false),
        too_many_reads(false),
@@ -52,6 +53,8 @@ ModelChecker::~ModelChecker()
        for (int i = 0; i < get_num_threads(); i++)
                delete thread_map->get(i);
        delete thread_map;
+       if (is_enabled)
+               free(is_enabled);
 
        delete obj_thrd_map;
        delete obj_map;
@@ -86,7 +89,13 @@ void ModelChecker::reset_to_initial_state()
 /** @returns a thread ID for a new Thread */
 thread_id_t ModelChecker::get_next_id()
 {
-       return priv->next_thread_id++;
+       thread_id_t newid=priv->next_thread_id++;
+       bool * tmp=(bool *) malloc((newid+1)*sizeof(bool));
+       memcpy(tmp, is_enabled, newid*sizeof(bool));
+       tmp[newid]=true;
+       free(is_enabled);
+       is_enabled=tmp;
+       return newid;
 }
 
 /** @returns the number of user threads created during this execution */
@@ -197,21 +206,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;
 }

diff --git a/model.h b/model.h
index 4fc32c6db6c2800d2bdf705d7a8b256683968bab..54f302684fc092b7226fa5a1d0988b536962d236 100644 (file)
--- a/model.h
+++ b/model.h
@@ -177,6 +177,8 @@ private:
         * together for efficiency and maintainability. */
        struct model_snapshot_members *priv;
 
+       bool * is_enabled;
+
        /**
         * @brief The modification order graph
         *