toward building a naive predicate tree

diff --git a/funcinst.cc b/funcinst.cc
index 8d9c23ba9c81d48b0c1856c53b89f05eb636c3e0..3216baee3d1e79c4f029d629d64ab781331b8bb6 100644 (file)
--- a/funcinst.cc
+++ b/funcinst.cc
@@ -8,6 +8,7 @@ FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) :
        this->position = act->get_position();
        this->location = act->get_location();
        this->type = act->get_type();
        this->position = act->get_position();
        this->location = act->get_location();
        this->type = act->get_type();

+       this->order = act->get_mo();

        this->func_node = func_node;
 }
 
        this->func_node = func_node;
 }
 


@@ -47,10 +48,10 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act)
 {
        action_type type = act->get_type();
 
 {
        action_type type = act->get_type();
 

-       mllnode<FuncInst*>* it;
-       for (it = collisions.begin();it != NULL;it=it->getNext()) {
+       mllnode<FuncInst*> * it;
+       for (it = collisions.begin(); it != NULL; it = it->getNext()) {

                FuncInst * inst = it->getVal();
                FuncInst * inst = it->getVal();

-               if ( inst->get_type() == type )
+               if (inst->get_type() == type)

                        return inst;
        }
        return NULL;
                        return inst;
        }
        return NULL;


@@ -58,7 +59,7 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act)
 
 bool FuncInst::is_read() const
 {
 
 bool FuncInst::is_read() const
 {

-       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS;    /* type == ATOMIC_RMW ? */
+       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS || type == ATOMIC_RMW;

 }
 
 bool FuncInst::is_write() const
 }
 
 bool FuncInst::is_write() const


@@ -66,3 +67,7 @@ bool FuncInst::is_write() const
        return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE;
 }
 
        return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE;
 }
 

+void FuncInst::print()
+{
+       model_print("func inst - position: %s, location: %p, type: %d, order: %d\n", position, location, type, order);
+}

diff --git a/funcinst.h b/funcinst.h
index bc56e2772544869097979b42bee45e7f44b1b675..654ba653edce66af902541dc9198703176d5ed04 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -17,6 +17,7 @@ public:
        const char * get_position() const { return position; }
        void * get_location() const { return location; }
        action_type get_type() const { return type; }
        const char * get_position() const { return position; }
        void * get_location() const { return location; }
        action_type get_type() const { return type; }

+       memory_order get_mo() const { return order; }

        FuncNode * get_func_node() const { return func_node; }
 
        bool add_pred(FuncInst * other);
        FuncNode * get_func_node() const { return func_node; }
 
        bool add_pred(FuncInst * other);


@@ -31,12 +32,15 @@ public:
        bool is_read() const;
        bool is_write() const;
 
        bool is_read() const;
        bool is_write() const;
 

+       void print();
+

        MEMALLOC
 private:
        //ModelAction * const action;
        const char * position;
        void * location;
        action_type type;
        MEMALLOC
 private:
        //ModelAction * const action;
        const char * position;
        void * location;
        action_type type;

+       memory_order order;

        FuncNode * func_node;
 
        /* collisions store a list of FuncInsts with the same position
        FuncNode * func_node;
 
        /* collisions store a list of FuncInsts with the same position

diff --git a/funcnode.cc b/funcnode.cc
index 6233d3f3fc882db027f8c0eee6cbbfb8fbcb39b9..190dce8eb1951f02ca1b17a1a63fae9da5f0b2df 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -5,7 +5,8 @@ FuncNode::FuncNode() :
        func_inst_map(),
        inst_list(),
        entry_insts(),
        func_inst_map(),
        inst_list(),
        entry_insts(),

-       thrd_read_map()
+       thrd_read_map(),
+       predicate_tree_entry()

 {}
 
 /* Check whether FuncInst with the same type, position, and location
 {}
 
 /* Check whether FuncInst with the same type, position, and location


@@ -18,10 +19,8 @@ FuncInst * FuncNode::get_or_add_inst(ModelAction *act)
        ASSERT(act);
        const char * position = act->get_position();
 
        ASSERT(act);
        const char * position = act->get_position();
 

-       /* Actions THREAD_CREATE, THREAD_START, THREAD_YIELD, THREAD_JOIN,
-        * THREAD_FINISH, PTHREAD_CREATE, PTHREAD_JOIN,
-        * ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK are not tagged with their
-        * source line numbers
+       /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
+        * actions are not tagged with their source line numbers

         */
        if (position == NULL)
                return NULL;
         */
        if (position == NULL)
                return NULL;


@@ -61,7 +60,7 @@ void FuncNode::add_entry_inst(FuncInst * inst)
        if (inst == NULL)
                return;
 
        if (inst == NULL)
                return;
 

-       mllnode<FuncInst*>* it;
+       mllnode<FuncInst *> * it;

        for (it = entry_insts.begin(); it != NULL; it = it->getNext()) {
                if (inst == it->getVal())
                        return;
        for (it = entry_insts.begin(); it != NULL; it = it->getNext()) {
                if (inst == it->getVal())
                        return;


@@ -70,10 +69,11 @@ void FuncNode::add_entry_inst(FuncInst * inst)
        entry_insts.push_back(inst);
 }
 
        entry_insts.push_back(inst);
 }
 

-/* @param act_list a list of ModelActions; this argument comes from ModelExecution
- * convert act_inst to inst_list do linking - add one FuncInst to another's predecessors and successors
+/**
+ * @brief Convert ModelAdtion list to FuncInst list 
+ * @param act_list A list of ModelActions

  */
  */

-void FuncNode::update_inst_tree(action_list_t * act_list)
+void FuncNode::update_tree(action_list_t * act_list)

 {
        if (act_list == NULL)
                return;
 {
        if (act_list == NULL)
                return;


@@ -82,16 +82,47 @@ void FuncNode::update_inst_tree(action_list_t * act_list)
 
        /* build inst_list from act_list for later processing */
        func_inst_list_t inst_list;
 
        /* build inst_list from act_list for later processing */
        func_inst_list_t inst_list;

+       func_inst_list_t read_inst_list;
+       HashTable<FuncInst *, uint64_t, uintptr_t, 4> read_val_map;
+

        for (sllnode<ModelAction *> * it = act_list->begin(); it != NULL; it = it->getNext()) {
                ModelAction * act = it->getVal();
                FuncInst * func_inst = get_or_add_inst(act);
 
        for (sllnode<ModelAction *> * it = act_list->begin(); it != NULL; it = it->getNext()) {
                ModelAction * act = it->getVal();
                FuncInst * func_inst = get_or_add_inst(act);
 

-               if (func_inst != NULL)
-                       inst_list.push_back(func_inst);
+               if (func_inst == NULL)
+                       continue;
+
+               inst_list.push_back(func_inst);
+
+               if (!predicate_tree_initialized) {
+                       model_print("position: %s ", act->get_position());
+                       act->print();
+               }
+
+               if (func_inst->is_read()) {
+                       read_inst_list.push_back(func_inst);
+                       read_val_map.put(func_inst, act->get_reads_from_value());
+               }

        }
 
        }
 

+       update_inst_tree(&inst_list);
+       model_print("line break\n");
+       init_predicate_tree(&read_inst_list, &read_val_map);
+}
+
+/** 
+ * @brief Link FuncInsts in inst_list  - add one FuncInst to another's predecessors and successors
+ * @param inst_list A list of FuncInsts
+ */
+void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
+{
+       if (inst_list == NULL)
+               return;
+       else if (inst_list->size() == 0)
+               return;
+

        /* start linking */
        /* start linking */

-       sllnode<FuncInst *>* it = inst_list.begin();
+       sllnode<FuncInst *>* it = inst_list->begin();

        sllnode<FuncInst *>* prev;
 
        /* add the first instruction to the list of entry insts */
        sllnode<FuncInst *>* prev;
 
        /* add the first instruction to the list of entry insts */


@@ -163,13 +194,16 @@ void FuncNode::clear_read_map(uint32_t tid)
        thrd_read_map[tid]->reset();
 }
 
        thrd_read_map[tid]->reset();
 }
 

-void FuncNode::init_predicate_tree(func_inst_list_t * inst_list)
+void FuncNode::init_predicate_tree(func_inst_list_t * inst_list, HashTable<FuncInst *, uint64_t, uintptr_t, 4> * read_val_map)

 {
        if (inst_list == NULL || inst_list->size() == 0)
                return;
 
 {
        if (inst_list == NULL || inst_list->size() == 0)
                return;
 

-       if (predicate_tree_initialized)
+       if (predicate_tree_initialized) {
+               model_print("function %s\n", func_name);
+               print_predicate_tree();

                return;
                return;

+       }

 
        predicate_tree_initialized = true;
 
 
        predicate_tree_initialized = true;
 


@@ -182,7 +216,8 @@ void FuncNode::init_predicate_tree(func_inst_list_t * inst_list)
        FuncInst * entry_inst = it->getVal();
 
        /* entry instruction has no predicate expression */
        FuncInst * entry_inst = it->getVal();
 
        /* entry instruction has no predicate expression */

-       Predicate * pred_entry = new Predicate(entry_inst);
+       Predicate * curr_pred = new Predicate(entry_inst);
+       predicate_tree_entry.add(curr_pred);

        loc_inst_map.put(entry_inst->get_location(), entry_inst);
 
        it = it->getNext();
        loc_inst_map.put(entry_inst->get_location(), entry_inst);
 
        it = it->getNext();


@@ -193,11 +228,25 @@ void FuncNode::init_predicate_tree(func_inst_list_t * inst_list)
                FuncInst * prev_inst = prev->getVal();
 
                if ( loc_inst_map.contains(curr_inst->get_location()) ) {
                FuncInst * prev_inst = prev->getVal();
 
                if ( loc_inst_map.contains(curr_inst->get_location()) ) {

-                       Predicate * pred1 = new Predicate(curr_inst);
-                       pred1->add_predicate(EQUALITY, curr_inst->get_location(), 0);
-
-                       Predicate * pred2 = new Predicate(curr_inst);
-                       pred2->add_predicate(EQUALITY, curr_inst->get_location(), 1);
+//                     model_print("new predicate created at location: %p\n", curr_inst->get_location());
+                       Predicate * new_pred1 = new Predicate(curr_inst);
+                       new_pred1->add_predicate(EQUALITY, curr_inst->get_location(), true);
+
+                       Predicate * new_pred2 = new Predicate(curr_inst);
+                       new_pred2->add_predicate(EQUALITY, curr_inst->get_location(), false);
+
+                       curr_pred->add_child(new_pred1);
+                       curr_pred->add_child(new_pred2);
+
+                       uint64_t last_read = read_val_map->get(prev_inst);
+                       if ( last_read == read_val_map->get(curr_inst) )
+                               curr_pred = new_pred1;
+                       else
+                               curr_pred = new_pred2;
+               } else {
+                       Predicate * new_pred = new Predicate(curr_inst);
+                       curr_pred->add_child(new_pred);
+                       curr_pred = new_pred;

                }
 
                loc_inst_map.put(curr_inst->get_location(), curr_inst);
                }
 
                loc_inst_map.put(curr_inst->get_location(), curr_inst);


@@ -207,19 +256,26 @@ void FuncNode::init_predicate_tree(func_inst_list_t * inst_list)
 }
 
 
 }
 
 

-void FuncNode::generate_predicate(FuncInst *func_inst)
+void FuncNode::print_predicate_tree()

 {
 {

+       HSIterator<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> * it;
+       it = predicate_tree_entry.iterator();

 
 

+       while (it->hasNext()) {
+               Predicate * p = it->next();
+               p->print_pred_subtree();
+       }

 }
 
 /* @param tid thread id
  * Print the values read by the last read actions for each memory location
  */
 }
 
 /* @param tid thread id
  * Print the values read by the last read actions for each memory location
  */

+/*

 void FuncNode::print_last_read(uint32_t tid)
 {
        ASSERT(thrd_read_map.size() > tid);
        read_map_t * read_map = thrd_read_map[tid];
 void FuncNode::print_last_read(uint32_t tid)
 {
        ASSERT(thrd_read_map.size() > tid);
        read_map_t * read_map = thrd_read_map[tid];

-/*
+

        mllnode<void *> * it;
        for (it = read_locations.begin();it != NULL;it=it->getNext()) {
                if ( !read_map->contains(it->getVal()) )
        mllnode<void *> * it;
        for (it = read_locations.begin();it != NULL;it=it->getNext()) {
                if ( !read_map->contains(it->getVal()) )


@@ -228,5 +284,5 @@ void FuncNode::print_last_read(uint32_t tid)
                uint64_t read_val = read_map->get(it->getVal());
                model_print("last read of thread %d at %p: 0x%x\n", tid, it->getVal(), read_val);
        }
                uint64_t read_val = read_map->get(it->getVal());
                model_print("last read of thread %d at %p: 0x%x\n", tid, it->getVal(), read_val);
        }

-*/

 }
 }

+*/

diff --git a/funcnode.h b/funcnode.h
index 367297462ed0c30edd9d493c8152a3e50618916f..61ab0593b7ed9a88465ae3fbc04eec7c8fc1fa3b 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -26,15 +26,17 @@ public:
        func_inst_list_mt * get_inst_list() { return &inst_list; }
        func_inst_list_mt * get_entry_insts() { return &entry_insts; }
        void add_entry_inst(FuncInst * inst);
        func_inst_list_mt * get_inst_list() { return &inst_list; }
        func_inst_list_mt * get_entry_insts() { return &entry_insts; }
        void add_entry_inst(FuncInst * inst);

-       void update_inst_tree(action_list_t * act_list);
+
+       void update_tree(action_list_t * act_list);
+       void update_inst_tree(func_inst_list_t * inst_list);

 
        void store_read(ModelAction * act, uint32_t tid);
        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 store_read(ModelAction * act, uint32_t tid);
        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 init_predicate_tree(func_inst_list_t * inst_list);
-       void generate_predicate(FuncInst * func_inst);
+       void init_predicate_tree(func_inst_list_t * inst_list, HashTable<FuncInst *, uint64_t, uintptr_t, 4> * read_val_map);
+       void print_predicate_tree();

 
        void print_last_read(uint32_t tid);
 
 
        void print_last_read(uint32_t tid);
 


@@ -58,7 +60,6 @@ private:
        /* Store the values read by atomic read actions per memory location for each thread */
        ModelVector<read_map_t *> thrd_read_map;
 
        /* Store the values read by atomic read actions per memory location for each thread */
        ModelVector<read_map_t *> thrd_read_map;
 

-       /* TODO: how to guarantee unique predicate? Or add an equal function */

        HashSet<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> predicate_tree_entry;
 };
 
        HashSet<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> predicate_tree_entry;
 };
 

diff --git a/history.cc b/history.cc
index a6d0c96f03168438b123364ed4da30c814945d1f..283c248f90cf0238e4d728e7c305c2ad2235aed4 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -67,8 +67,9 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
                FuncNode * func_node = func_nodes[func_id];
                func_node->clear_read_map(tid);
 
                FuncNode * func_node = func_nodes[func_id];
                func_node->clear_read_map(tid);
 

+               // model_print("hello function %s and thread %d\n", func_node->get_func_name(), tid);

                action_list_t * curr_act_list = func_act_lists->back();
                action_list_t * curr_act_list = func_act_lists->back();

-               func_node->update_inst_tree(curr_act_list);
+               func_node->update_tree(curr_act_list);

 
                (*thrd_func_list)[id].pop_back();
                func_act_lists->pop_back();
 
                (*thrd_func_list)[id].pop_back();
                func_act_lists->pop_back();