experiment with adding NULLITY predicate

diff --git a/funcinst.cc b/funcinst.cc
index cecaca7ba86d473a3192bca9a5bd1f1bbfd77192..a3a2874ec7ce2c0044956803b03caefacf23ba62 100644 (file)
--- a/funcinst.cc
+++ b/funcinst.cc
@@ -1,7 +1,7 @@
 #include "funcinst.h"
 
 FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) :
-       collisions()
+       single_location(true)
 {
        ASSERT(act);
        ASSERT(func_node);
@@ -44,6 +44,7 @@ bool FuncInst::add_succ(FuncInst * other)
        return true;
 }
 
+/*
 FuncInst * FuncInst::search_in_collision(ModelAction *act)
 {
        action_type type = act->get_type();
@@ -56,6 +57,7 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act)
        }
        return NULL;
 }
+*/
 
 bool FuncInst::is_read() const
 {

diff --git a/funcinst.h b/funcinst.h
index 654ba653edce66af902541dc9198703176d5ed04..3b2890f0bdafa33ea9e041b23ddfa47987eb3fac 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -13,7 +13,6 @@ public:
        FuncInst(ModelAction *act, FuncNode *func_node);
        ~FuncInst();
 
-       //ModelAction * get_action() const { return action; }
        const char * get_position() const { return position; }
        void * get_location() const { return location; }
        action_type get_type() const { return type; }
@@ -23,30 +22,40 @@ public:
        bool add_pred(FuncInst * other);
        bool add_succ(FuncInst * other);
 
-       FuncInst * search_in_collision(ModelAction *act);
+       //FuncInst * search_in_collision(ModelAction *act);
+       //func_inst_list_mt * get_collisions() { return &collisions; }
 
-       func_inst_list_mt * get_collisions() { return &collisions; }
        func_inst_list_mt * get_preds() { return &predecessors; }
        func_inst_list_mt * get_succs() { return &successors; }
 
        bool is_read() const;
        bool is_write() const;
+       bool is_single_location() { return single_location; }
+       void not_single_location() { single_location = false; }
 
        void print();
 
        MEMALLOC
 private:
-       //ModelAction * const action;
        const char * position;
+
+       /* Atomic operations with the same source line number may act at different
+        * memory locations, such as the next field of the head pointer in ms-queue. 
+        * location only stores the memory location when this FuncInst was constructed.
+        */
        void * location;
        action_type type;
        memory_order order;
        FuncNode * func_node;
 
-       /* collisions store a list of FuncInsts with the same position
+       bool single_location;
+
+       /* Currently not in use. May remove this field later
+        *
+        * collisions store a list of FuncInsts with the same position
         * but different action types. For example, CAS is broken down
         * as three different atomic operations in cmodelint.cc */
-       func_inst_list_mt collisions;
+       // func_inst_list_mt collisions;
 
        func_inst_list_mt predecessors;
        func_inst_list_mt successors;

diff --git a/funcnode.cc b/funcnode.cc
index 188ed173c3c0bfda3bc60fad06c7d781fc4f5fbc..5b6fb355a5e92b422be0157bec6b4e97398460e2 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -29,17 +29,9 @@ void FuncNode::add_inst(ModelAction *act)
        if ( func_inst_map.contains(position) ) {
                FuncInst * inst = func_inst_map.get(position);
 
-               if (inst->get_type() != act->get_type() ) {
-                       // model_print("action with a different type occurs at line number %s\n", position);
-                       FuncInst * func_inst = inst->search_in_collision(act);
-
-                       if (func_inst != NULL)
-                               return;
-
-                       func_inst = new FuncInst(act, this);
-                       inst->get_collisions()->push_back(func_inst);
-                       inst_list.push_back(func_inst); // delete?
-               }
+               ASSERT(inst->get_type() == act->get_type());
+               if (inst->get_location() != act->get_location())
+                       inst->not_single_location();
 
                return;
        }
@@ -69,8 +61,6 @@ FuncInst * FuncNode::get_inst(ModelAction *act)
        if (inst == NULL)
                return NULL;
 
-//     ASSERT(inst->get_location() == act->get_location());
-
        action_type inst_type = inst->get_type();
        action_type act_type = act->get_type();
 
@@ -130,8 +120,12 @@ void FuncNode::update_tree(action_list_t * act_list)
                        read_act_list.push_back(act);
        }
 
+       model_print("function %s\n", func_name);
        update_inst_tree(&inst_list);
        update_predicate_tree(&read_act_list);
+       deep_update(predicate_tree_entry);
+
+       print_predicate_tree();
 }
 
 /** 
@@ -271,8 +265,8 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 
                                curr_pred->add_child(new_pred1);
                                curr_pred->add_child(new_pred2);
-                               //new_pred1->add_parent(curr_pred);
-                               //new_pred2->add_parent(curr_pred);
+                               new_pred1->set_parent(curr_pred);
+                               new_pred2->set_parent(curr_pred);
 
                                ModelAction * last_act = loc_act_map.get(next_act->get_location());
                                uint64_t last_read = last_act->get_reads_from_value();
@@ -285,7 +279,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                        } else {
                                Predicate * new_pred = new Predicate(next_inst);
                                curr_pred->add_child(new_pred);
-                               //new_pred->add_parent(curr_pred);
+                               new_pred->set_parent(curr_pred);
 
                                curr_pred = new_pred;
                        }
@@ -294,9 +288,40 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                loc_act_map.put(next_act->get_location(), next_act);
                it = it->getNext();
        }
+}
+
+void FuncNode::deep_update(Predicate * curr_pred)
+{
+       FuncInst * func_inst = curr_pred->get_func_inst();
+       if (func_inst != NULL && !func_inst->is_single_location()) {
+               bool has_null_pred = false;
+               PredExprSet * pred_expressions = curr_pred->get_pred_expressions();
+               PredExprSetIter * pred_expr_it = pred_expressions->iterator();
+               while (pred_expr_it->hasNext()) {
+                       pred_expr * pred_expression = pred_expr_it->next();
+                       if (pred_expression->token == NULLITY) {
+                               has_null_pred = true;
+                               break;
+                       }
+               }
+
+               if (!has_null_pred) {
+//                     func_inst->print();
+                       Predicate * parent = curr_pred->get_parent();
+                       curr_pred->add_predicate(NULLITY, NULL, 0);
+
+                       Predicate * another_branch = new Predicate(func_inst);
+                       another_branch->add_predicate(NULLITY, NULL, 1);
+                       parent->add_child(another_branch);
+//                     another_branch.add_children(i);
+               }
+       }
 
-//     model_print("function %s\n", func_name);
-//     print_predicate_tree();
+       ModelVector<Predicate *> * branches = curr_pred->get_children();
+       for (uint i = 0; i < branches->size(); i++) {
+               Predicate * branch = (*branches)[i];
+               deep_update(branch);
+       }
 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that contains next_inst and the correct predicate
@@ -317,7 +342,6 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
 
                /* no predicate, follow the only branch */
                if (pred_expressions->getSize() == 0) {
-//                     model_print("no predicate exists: "); next_inst->print();
                        *curr_pred = branch;
                        branch_found = true;
                        break;
@@ -337,7 +361,6 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                                        next_read = next_act->get_reads_from_value();
 
                                        equality = (last_read == next_read);
-
                                        if (equality == pred_expression->value) {
                                                *curr_pred = branch;
 //                                             model_print("predicate: token: %d, location: %p, value: %d - ", pred_expression->token, pred_expression->location, pred_expression->value); next_inst->print();
@@ -345,6 +368,13 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                                        }
                                        break;
                                case NULLITY:
+                                       next_read = next_act->get_reads_from_value();
+                                       equality = ((void*)next_read == NULL);
+                                       //model_print("%s ", next_act->get_position()); next_act->print();
+                                       if (equality == pred_expression->value) {
+                                               *curr_pred = branch;
+                                               branch_found = true;
+                                       }
                                        break;
                                default:
                                        model_print("unkown predicate token\n");

diff --git a/funcnode.h b/funcnode.h
index 4ba239856df8e468a7bf4f6b7518a7a95381bed7..730a7b7cc22a50767d1df5d4563b90d84ec46973 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -37,6 +37,7 @@ public:
 
        /* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */
        void update_predicate_tree(action_list_t * act_list);
+       void deep_update(Predicate * pred);
        bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable<void *, ModelAction *, uintptr_t, 0>* loc_act_map);
        void print_predicate_tree();
 

diff --git a/predicate.cc b/predicate.cc
index 77f362dafd9c4f8ea29e465a3c01f5f99ea9172c..128ac3dc4155ddcec0a8cbda9143b9d0e4fa5089 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -5,7 +5,7 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry) :
        entry_predicate(is_entry),
        pred_expressions(),
        children(),
-       parents(),
+       parent(NULL),
        backedge(NULL)
 {}
 
@@ -37,12 +37,6 @@ void Predicate::add_child(Predicate * child)
        children.push_back(child);
 }
 
-void Predicate::add_parent(Predicate * parent)
-{
-       /* check duplication? */
-       parents.push_back(parent);
-}
-
 void Predicate::print_predicate()
 {
        model_print("\"%p\" [shape=box, label=\"\n", this);

diff --git a/predicate.h b/predicate.h
index 2f15a126653f724e510c3c7a1fb0145fe781a1cd..dbb959ea4b0cb84cee1bcbc198f71bf741547654 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -41,11 +41,11 @@ public:
        PredExprSet * get_pred_expressions() { return &pred_expressions; }
        void add_predicate(token_t token, void * location, bool value);
        void add_child(Predicate * child);
-       void add_parent(Predicate * parent);
+       void set_parent(Predicate * parent_pred) { parent = parent_pred; }
        void set_backedge(Predicate * back_pred) { backedge = back_pred; }
 
        ModelVector<Predicate *> * get_children() { return &children; }
-       ModelVector<Predicate *> * get_parents() { return &parents; }
+       Predicate * get_parent() { return parent; }
        Predicate * get_backedge() { return backedge; }
 
        bool is_entry_predicate() { return entry_predicate; }
@@ -62,7 +62,9 @@ private:
        /* may have multiple predicates */
        PredExprSet pred_expressions;
        ModelVector<Predicate *> children;
-       ModelVector<Predicate *> parents;
+
+       /* only a single parent may exist */
+       Predicate * parent;
 
        /* assume almost one back edge exists */
        Predicate * backedge;