model: wrap some ModelAction helper functions
authorBrian Norris <banorris@uci.edu>
Sun, 29 Apr 2012 06:41:41 +0000 (23:41 -0700)
committerBrian Norris <banorris@uci.edu>
Sun, 29 Apr 2012 19:29:06 +0000 (12:29 -0700)
model.cc
model.h

index d878abbc002124d4dcacd2651af3c1990f6c19b9..f0709103f10c0ecafea972e08c78a6716a109136 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -119,9 +119,7 @@ bool ModelChecker::next_execution()
 
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
-       void *loc = act->get_location();
        action_type type = act->get_type();
-       thread_id_t id = act->get_tid();
 
        switch (type) {
                case THREAD_CREATE:
@@ -137,14 +135,8 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
        action_list_t::reverse_iterator rit;
        for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
                ModelAction *prev = *rit;
-               if (prev->get_location() != loc)
-                       continue;
-               if (type == ATOMIC_READ && prev->get_type() != ATOMIC_WRITE)
-                       continue;
-               /* Conflict from the same thread is not really a conflict */
-               if (id == prev->get_tid())
-                       continue;
-               return prev;
+               if (act->is_dependent(prev))
+                       return prev;
        }
        return NULL;
 }
@@ -259,6 +251,38 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int
        act->value = value;
 }
 
+bool ModelAction::is_read()
+{
+       return type == ATOMIC_READ;
+}
+
+bool ModelAction::is_write()
+{
+       return type == ATOMIC_WRITE;
+}
+
+bool ModelAction::same_var(ModelAction *act)
+{
+       return location == act->location;
+}
+
+bool ModelAction::same_thread(ModelAction *act)
+{
+       return tid == act->tid;
+}
+
+bool ModelAction::is_dependent(ModelAction *act)
+{
+       if (!is_read() && !is_write())
+               return false;
+       if (!act->is_read() && !act->is_write())
+               return false;
+       if (same_var(act) && !same_thread(act) &&
+                       (is_write() || act->is_write()))
+               return true;
+       return false;
+}
+
 void ModelAction::print(void)
 {
        const char *type_str;
diff --git a/model.h b/model.h
index ad8760a28576aafecc17d05d9cb01b92e7df259d..4472c5b2b0c7499373e226e0aee40a7cfe432ae8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -36,6 +36,12 @@ public:
 
        TreeNode * get_node() { return node; }
        void set_node(TreeNode *n) { node = n; }
+
+       bool is_read();
+       bool is_write();
+       bool same_var(ModelAction *act);
+       bool same_thread(ModelAction *act);
+       bool is_dependent(ModelAction *act);
 private:
        action_type type;
        memory_order order;