planning to build a predicate generator based on values that have been written to...

diff --git a/funcinst.cc b/funcinst.cc
index 7e0446ffec149e9c778345c6ca2790ca48916cec..92890d58ce07b296daa0b7bb1c0c17e717d4bb78 100644 (file)
--- a/funcinst.cc
+++ b/funcinst.cc
@@ -58,5 +58,11 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act)
 
 bool FuncInst::is_read() const
 {
-       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS;
+       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS; /* type == ATOMIC_RMW ? */
 }
+
+bool FuncInst::is_write() const
+{
+        return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE;
+}
+

diff --git a/funcinst.h b/funcinst.h
index 85b9c20ecce2d9b07d8b85168fc3f1bbe39701b4..efdb43b4dbe88c9250cb62ecaca8848bbfce1f95 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -1,3 +1,6 @@
+#ifndef __FUNCINST_H__
+#define __FUNCINST_H__
+
 #include "action.h"
 #include "hashtable.h"
 
@@ -26,6 +29,7 @@ public:
        func_inst_list_mt * get_succs() { return &successors; }
 
        bool is_read() const;
+       bool is_write() const;
 
        MEMALLOC
 private:
@@ -43,3 +47,6 @@ private:
        func_inst_list_mt predecessors;
        func_inst_list_mt successors;
 };
+
+#endif /* __FUNCINST_H__ */
+

diff --git a/funcnode.cc b/funcnode.cc
index 281e0f0559486a1ae64dad4480232a4f1b773b06..208bc3beb2666520d20ac30f873234b1e9775e00 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -1,4 +1,5 @@
 #include "funcnode.h"
+#include "predicate.h"
 
 FuncNode::FuncNode() :
        func_inst_map(),
@@ -164,6 +165,11 @@ void FuncNode::clear_read_map(uint32_t tid)
        thrd_read_map[tid]->reset();
 }
 
+void FuncNode::generate_predicate(FuncInst *func_inst)
+{
+       
+}
+
 /* @param tid thread id
  * Print the values read by the last read actions for each memory location
  */

diff --git a/funcnode.h b/funcnode.h
index f80e9266087e4bc448554ea6bb00a98d7c5f7c02..08e07fb188ffcbd009f2ee6b160f0b674fd97935 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -1,9 +1,10 @@
+#ifndef __FUNCNODE_H__
+#define __FUNCNODE_H__
+
 #include "action.h"
 #include "funcinst.h"
 #include "hashtable.h"
 
-class ModelAction;
-
 typedef ModelList<FuncInst *> func_inst_list_mt;
 typedef HashTable<void *, uint64_t, uintptr_t, 4, model_malloc, model_calloc, model_free> read_map_t;
 
@@ -29,6 +30,9 @@ public:
        uint64_t query_last_read(void * location, uint32_t tid);
        void clear_read_map(uint32_t tid);
 
+       /* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */
+       void generate_predicate(FuncInst * func_inst);
+
        void print_last_read(uint32_t tid);
 
        MEMALLOC
@@ -51,3 +55,5 @@ private:
        ModelVector<read_map_t *> thrd_read_map;
        ModelList<void *> read_locations;
 };
+
+#endif /* __FUNCNODE_H__ */

diff --git a/history.cc b/history.cc
index 267205db559ebba3a06b109ca897b09d5a08d31a..7b6e3c87fe6adfca4e5bbcd54e99203b8ec35234 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -13,7 +13,8 @@ ModelHistory::ModelHistory() :
        func_counter(1),        /* function id starts with 1 */
        func_map(),
        func_map_rev(),
-       func_nodes()
+       func_nodes(),
+       write_history()
 {}
 
 void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
@@ -118,6 +119,9 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
        if (inst->is_read())
                func_node->store_read(act, tid);
 
+       if (inst->is_write())
+               add_to_write_history(act->get_location(), act->get_write_value());
+
        /* add to curr_inst_list */
        func_inst_list_t * curr_inst_list = func_inst_lists->back();
        ASSERT(curr_inst_list != NULL);
@@ -150,6 +154,15 @@ uint64_t ModelHistory::query_last_read(void * location, thread_id_t tid)
        return last_read_val;
 }
 
+void ModelHistory::add_to_write_history(void * location, uint64_t write_val)
+{
+       if ( !write_history.contains(location) )
+               write_history.put(location, new write_set_t() );
+
+       write_set_t * write_set = write_history.get(location);
+       write_set->add(write_val);
+}
+
 void ModelHistory::print()
 {
        /* function id starts with 1 */

diff --git a/history.h b/history.h
index 184646c64a8eaf30eb436b97a5a71ae6391d926f..5709ab6cc9baa405dc2f5febc00b3910b639c4bf 100644 (file)
--- a/history.h
+++ b/history.h
@@ -1,8 +1,14 @@
+#ifndef __HISTORY_H__
+#define __HISTORY_H__
+
 #include "stl-model.h"
 #include "common.h"
 #include "hashtable.h"
+#include "hashset.h"
 #include "threads-model.h"
 
+typedef HashSet<uint64_t, uint64_t, 4, model_malloc, model_calloc, model_free> write_set_t;
+
 class ModelHistory {
 public:
        ModelHistory();
@@ -24,6 +30,8 @@ public:
        FuncNode * get_func_node(uint32_t func_id);
        uint64_t query_last_read(void * location, thread_id_t tid);
 
+       void add_to_write_history(void * location, uint64_t write_val);
+
        void print();
 
        MEMALLOC
@@ -36,4 +44,7 @@ private:
        ModelVector<const char *> func_map_rev;
 
        ModelVector<FuncNode *> func_nodes;
+       HashTable<void *, write_set_t *, uintptr_t, 4, model_malloc, model_calloc, model_free> write_history;
 };
+
+#endif /* __HISTORY_H__ */

diff --git a/predicate.cc b/predicate.cc
new file mode 100644 (file)
index 0000000..9f4246e
--- /dev/null
+++ b/predicate.cc
@@ -0,0 +1,26 @@
+#include "predicate.h"
+
+inline bool operator==(const predicate_expr& expr_A, const predicate_expr& expr_B)
+{
+       if (expr_A.token != expr_B.token)
+               return false;
+
+       if (expr_A.token == EQUALITY && expr_A.location != expr_B.location)
+               return false;
+
+       if (expr_A.value != expr_B.value)
+               return false;
+
+       return true;
+}
+
+void Predicate::add_predicate(predicate_expr predicate)
+{
+       ModelList<predicate_expr>::iterator it;
+       for (it = predicates.begin(); it != predicates.end(); it++) {
+               if (predicate == *it)
+                       return;
+       }
+
+       predicates.push_back(predicate);
+}

diff --git a/predicate.h b/predicate.h
new file mode 100644 (file)
index 0000000..e2412d1
--- /dev/null
+++ b/predicate.h
@@ -0,0 +1,31 @@
+#include "funcinst.h"
+
+typedef enum predicate_token {
+       EQUALITY, NULLITY
+} token_t;
+
+/* If token is EQUALITY, then the predicate asserts whether
+ * this load should read the same value as the last value 
+ * read at memory location specified in predicate_expr.
+ */
+struct predicate_expr {
+       token_t token;
+       void * location;
+       bool value;
+};
+
+class Predicate {
+public:
+       Predicate();
+       ~Predicate();
+
+       FuncInst * get_func_inst() { return func_inst; }
+       ModelList<predicate_expr> * get_predicates() { return &predicates; }
+       void add_predicate(predicate_expr predicate);
+
+       MEMALLOC
+private:
+       FuncInst * func_inst;
+       /* may have multiple precicates */
+       ModelList<predicate_expr> predicates;
+};