Make sure that actions that do writes are labeled correctly in predicate trees

diff --git a/funcnode.cc b/funcnode.cc
index 3f238fc1fdaf53f9559fbf47aa86cfbcff3efe32..64972b4d4d1555a441bc30b7a3306314da9c9fce 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -147,16 +147,23 @@ void FuncNode::update_tree(action_list_t * act_list)
 
                inst_list.push_back(func_inst);
 
-               if (func_inst->is_write())
+               /* NOTE: for rmw actions, func_inst and act may have different
+                * action types because of action type conversion in ModelExecution
+                * func_inst->is_write() <==> pure writes (excluding rmw) */
+               if (func_inst->is_write()) {
+                       // model_print("write detected\n");
                        rw_act_list.push_back(act);
+               }
 
+               /* func_inst->is_read() <==> read + rmw */
                if (func_inst->is_read()) {
                        rw_act_list.push_back(act);
                        /* If func_inst may only read_from a single location, then:
                         *
-                        * The first time an action reads from some location, import all the values that have
-                        * been written to this location from ModelHistory and notify ModelHistory that this
-                        * FuncNode may read from this location.
+                        * The first time an action reads from some location,
+                        * import all the values that have been written to this
+                        * location from ModelHistory and notify ModelHistory
+                        * that this FuncNode may read from this location.
                         */
                        void * loc = act->get_location();
                        if (!read_locations->contains(loc) && func_inst->is_single_location()) {
@@ -273,6 +280,9 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                        continue;
                }
 
+               if (next_act->is_write())
+                       curr_pred->set_write(true);
+
                inst_pred_map.put(next_inst, curr_pred);
                if (!inst_id_map.contains(next_inst))
                        inst_id_map.put(next_inst, inst_counter++);
@@ -304,6 +314,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                PredExprSet * pred_expressions = branch->get_pred_expressions();
                PredExprSetIter * pred_expr_it = pred_expressions->iterator();
 
+               /* Only read and rmw actions my have unset predicate expressions */
                if (pred_expressions->getSize() == 0) {
                        predicate_correct = false;
                        unset_predicates->push_back(branch);
@@ -355,6 +366,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
        return branch_found;
 }
 
+/* Infer predicate expressions, which are generated in FuncNode::generate_predicates */
 void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
        HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map,
        SnapVector<struct half_pred_expr *> * half_pred_expressions)
@@ -362,6 +374,7 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
        void * loc = next_act->get_location();
 
        if (next_inst->is_read()) {
+               /* read + rmw */
                if ( loc_act_map->contains(loc) ) {
                        ModelAction * last_act = loc_act_map->get(loc);
                        FuncInst * last_inst = get_inst(last_act);
@@ -394,7 +407,8 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
                        }
                }
        } else {
-               // TODO: when next_act is a write action, do anything?
+               /* Pure writes */
+               // TODO: do anything here?
        }
 }
 
@@ -407,12 +421,14 @@ void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst,
                (*curr_pred)->add_child(new_pred);
                new_pred->set_parent(*curr_pred);
 
-               /* entry predicates and predicates containing write actions 
+               /* entry predicates and predicates containing pure write actions
                 * have no predicate expressions */
                if ( (*curr_pred)->is_entry_predicate() )
                        new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
-               else if (next_inst->is_write())
+               else if (next_inst->is_write()) {
+                       /* next_inst->is_write() <==> pure writes */
                        new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
+               }
 
                return;
        }
@@ -526,6 +542,7 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location
        }
 }
 
+/* Every time a thread enters a function, set its position to the predicate tree entry */
 void FuncNode::init_predicate_tree_position(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
@@ -541,12 +558,14 @@ void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred)
        predicate_tree_position[thread_id] = pred;
 }
 
+/* @return The position of a thread in a predicate tree */
 Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
        return predicate_tree_position[thread_id];
 }
 
+/* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */
 void FuncNode::init_inst_act_map(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
@@ -561,6 +580,7 @@ void FuncNode::init_inst_act_map(thread_id_t tid)
        }
 }
 
+/* Reset elements of thrd_inst_act_map when threads exit functions */
 void FuncNode::reset_inst_act_map(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);

diff --git a/funcnode.h b/funcnode.h
index 53f071f18fb3791d1c59c51ab4aa05ed5f8e40ad..b022284a2fb52a6d36ca67c8649f230f3d96d917 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -32,12 +32,8 @@ public:
 
        void update_tree(action_list_t * act_list);
        void update_inst_tree(func_inst_list_t * inst_list);
-
        void update_predicate_tree(action_list_t * act_list);
        bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable<FuncInst *, ModelAction *, uintptr_t, 0> * inst_act_map, SnapVector<Predicate *> * unset_predicates);
-       void infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map, SnapVector<struct half_pred_expr *> * half_pred_expressions);
-       void generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
-       bool amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act);
 
        void incr_exit_count() { exit_count++; }
        uint32_t get_exit_count() { return exit_count; }
@@ -82,21 +78,26 @@ private:
        /* Possible entry atomic actions in this function */
        func_inst_list_mt entry_insts;
 
+       void infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+       void generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+       bool amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act);
+
        /* Store action_lists when calls to update_tree are deferred */
        ModelList<action_list_t *> action_list_buffer;
 
        /* read_locations: set of locations read by this FuncNode
         * val_loc_map: keep track of locations that have the same values written to;
-        * loc_may_equal_map: deduced from val_loc_map;
-        */
+        * loc_may_equal_map: look up locations that may share the same value as key; 
+        *                      deduced from val_loc_map;       */
        loc_set_t * read_locations;
        HashTable<uint64_t, loc_set_t *, uint64_t, 0> * val_loc_map;
        HashTable<void *, loc_set_t *, uintptr_t, 0> * loc_may_equal_map;
        // value_set_t * values_may_read_from;
 
-       /* run-time position in the predicate tree for each thread */
+       /* Run-time position in the predicate tree for each thread */
        ModelVector<Predicate *> predicate_tree_position;
 
+       /* A run-time map from FuncInst to ModelAction for each thread; needed by NewFuzzer */
        SnapVector<inst_act_map_t *> * thrd_inst_act_map;
 };
 

diff --git a/predicate.cc b/predicate.cc
index 2d7777783dac99e1f28553b416c969a0b34e4591..5cc0219c4b14e36033953d9d1bc37b8773f583ef 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -3,6 +3,7 @@
 Predicate::Predicate(FuncInst * func_inst, bool is_entry) :
        func_inst(func_inst),
        entry_predicate(is_entry),
+       does_write(false),
        pred_expressions(16),
        children(),
        parent(NULL),
@@ -89,6 +90,10 @@ void Predicate::print_predicate()
                                break;
                }
        }
+
+       if (does_write) {
+               model_print("Does write\n");
+       }
        model_print("\"];\n");
 }
 

diff --git a/predicate.h b/predicate.h
index e901d91fe3d71c357a83be46b8a098d8123f69e3..4243a0d88cc98bc47ece42b96f07839c1bf3fe4c 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -66,6 +66,10 @@ public:
        bool is_entry_predicate() { return entry_predicate; }
        void set_entry_predicate() { entry_predicate = true; }
 
+       /* Whether func_inst does write or not */
+       bool is_write() { return does_write; }
+       void set_write(bool is_write) { does_write = is_write; }
+
        void print_predicate();
        void print_pred_subtree();
 
@@ -73,15 +77,16 @@ public:
 private:
        FuncInst * func_inst;
        bool entry_predicate;
+       bool does_write;
 
-       /* may have multiple predicate expressions */
+       /* May have multiple predicate expressions */
        PredExprSet pred_expressions;
        ModelVector<Predicate *> children;
 
-       /* only a single parent may exist */
+       /* Only a single parent may exist */
        Predicate * parent;
 
-       /* may have multiple back edges, e.g. nested loops */
+       /* May have multiple back edges, e.g. nested loops */
        PredSet backedges;
 };