add helper functions; prepare for computing which memory locations may store the...
authorweiyu <weiyuluo1232@gmail.com>
Wed, 21 Aug 2019 20:52:25 +0000 (13:52 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Wed, 21 Aug 2019 20:52:25 +0000 (13:52 -0700)
classlist.h
funcnode.cc
funcnode.h
history.cc
history.h
model.cc

index 664301e..5a17449 100644 (file)
@@ -24,10 +24,14 @@ struct bug_message;
 typedef SnapList<ModelAction *> action_list_t;
 typedef SnapList<uint32_t> func_id_list_t;
 typedef SnapList<FuncInst *> func_inst_list_t;
-typedef HSIterator<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSetIter;
+
 typedef HashSet<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSet;
-typedef HSIterator<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free> write_set_iter;
-typedef HashSet<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free> write_set_t;
+typedef HSIterator<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSetIter;
+
+typedef HashSet<uint64_t, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> value_set_t;
+typedef HSIterator<uint64_t, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> value_set_iter;
+typedef HashSet<void *, uintptr_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> loc_set_t;
+typedef HSIterator<void *, uintptr_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> loc_set_iter;
 
 extern volatile int modellock;
 #endif
index dc01396..ccb930f 100644 (file)
@@ -3,26 +3,33 @@
 FuncNode::FuncNode(ModelHistory * history) :
        history(history),
        predicate_tree_initialized(false),
-       predicate_tree_entry(new Predicate(NULL, true)),
        exit_count(0),
        func_inst_map(),
        inst_list(),
        entry_insts(),
-       thrd_read_map(),
+//     thrd_read_map(),
        action_list_buffer()
 {
+       predicate_tree_entry = new Predicate(NULL, true);
        predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
+
+       // memory will be reclaimed after each execution
+       read_locations = new loc_set_t();
+       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
 }
 
 void FuncNode::set_new_exec_flag()
 {
-       for (uint i = 0; i < thrd_read_map.size(); i++)
-               thrd_read_map[i] = new read_map_t();
+//     for (uint i = 0; i < thrd_read_map.size(); i++)
+//             thrd_read_map[i] = new read_map_t();
 
        for (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
                FuncInst * inst = it->getVal();
                inst->reset_location();
        }
+
+       read_locations = new loc_set_t();
+       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
 }
 
 /* Check whether FuncInst with the same type, position, and location
@@ -119,6 +126,8 @@ void FuncNode::update_tree(action_list_t * act_list)
        if (act_list == NULL || act_list->size() == 0)
                return;
 
+       HashTable<void *, value_set_t *, uintptr_t, 4> * write_history = history->getWriteHistory();
+
        /* build inst_list from act_list for later processing */
        func_inst_list_t inst_list;
        action_list_t read_act_list;
@@ -132,8 +141,21 @@ void FuncNode::update_tree(action_list_t * act_list)
 
                inst_list.push_back(func_inst);
 
-               if (func_inst->is_read())
+               if (func_inst->is_read()) {
                        read_act_list.push_back(act);
+
+                       /* 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)) {
+                               read_locations->add(loc);
+                               value_set_t * write_values = write_history->get(loc);
+                               add_to_val_loc_map(write_values, loc);
+                               history->add_to_loc_func_nodes_map(loc, this);
+                       }
+               }
        }
 
 //     model_print("function %s\n", func_name);
@@ -181,13 +203,13 @@ void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
  * Store the values read by atomic read actions into thrd_read_map */
 void FuncNode::store_read(ModelAction * act, uint32_t tid)
 {
+/*
        ASSERT(act);
 
        void * location = act->get_location();
        uint64_t read_from_val = act->get_reads_from_value();
 
-       /* resize and initialize */
-
+       // resize and initialize
        uint32_t old_size = thrd_read_map.size();
        if (old_size <= tid) {
                thrd_read_map.resize(tid + 1);
@@ -197,24 +219,24 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid)
 
        read_map_t * read_map = thrd_read_map[tid];
        read_map->put(location, read_from_val);
-
-       /* Store the memory locations where atomic reads happen */
-       // read_locations.add(location);
+*/
 }
 
 uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
 {
+/*
        if (thrd_read_map.size() <= tid)
                return VALUE_NONE;
 
        read_map_t * read_map = thrd_read_map[tid];
 
-       /* last read value not found */
+       // last read value not found
        if ( !read_map->contains(location) )
                return VALUE_NONE;
 
        uint64_t read_val = read_map->get(location);
        return read_val;
+*/
 }
 
 /* @param tid thread id
@@ -223,10 +245,12 @@ uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
  */
 void FuncNode::clear_read_map(uint32_t tid)
 {
+/*
        if (thrd_read_map.size() <= tid)
                return;
 
        thrd_read_map[tid]->reset();
+*/
 }
 
 void FuncNode::update_predicate_tree(action_list_t * act_list)
@@ -454,6 +478,38 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
        return branch_found;
 }
 
+void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
+{
+       loc_set_t * locations = val_loc_map->get(val);
+
+       if (locations == NULL) {
+               locations = new loc_set_t();
+               val_loc_map->put(val, locations);
+       }
+
+       locations->add(loc);
+
+/*
+       model_print("val %llx: ", val);
+       loc_set_iter * it = locations->iterator();
+       while (it->hasNext()) {
+               void * location = it->next();
+               model_print("%p ", location);
+       }
+       model_print("\n");
+*/
+}
+
+void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc)
+{
+       value_set_iter * it = values->iterator();
+       while (it->hasNext()) {
+               uint64_t val = it->next();
+               add_to_val_loc_map(val, loc);
+       }
+}
+
+
 void FuncNode::print_predicate_tree()
 {
        model_print("digraph function_%s {\n", func_name);
index c84815c..6e08fc2 100644 (file)
@@ -47,6 +47,9 @@ public:
 
        ModelList<action_list_t *> * get_action_list_buffer() { return &action_list_buffer; }
 
+       void add_to_val_loc_map(uint64_t val, void * loc);
+       void add_to_val_loc_map(value_set_t * values, void * loc);
+
        void print_predicate_tree();
        void print_last_read(uint32_t tid);
 
@@ -72,9 +75,13 @@ private:
        func_inst_list_mt entry_insts;
 
        /* Store the values read by atomic read actions per memory location for each thread */
-       ModelVector<read_map_t *> thrd_read_map;
+       //ModelVector<read_map_t *> thrd_read_map;
 
+       /* store action_lists when calls to update_tree are deferred */
        ModelList<action_list_t *> action_list_buffer;
+
+       loc_set_t * read_locations;
+       HashTable<uint64_t, loc_set_t *, uint64_t, 0> * val_loc_map;
 };
 
 #endif /* __FUNCNODE_H__ */
index 2dbc556..68e8575 100644 (file)
@@ -14,8 +14,8 @@ ModelHistory::ModelHistory() :
        func_map(),
        func_map_rev(),
        func_nodes(),
-       write_history(),
-       write_locations()
+       write_history(),        // snapshot data structure
+       loc_func_nodes_map()    // shapshot data structure
 {}
 
 void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
@@ -63,15 +63,14 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
 
        if (last_func_id == func_id) {
                FuncNode * func_node = func_nodes[func_id];
-               func_node->clear_read_map(tid);
+               //func_node->clear_read_map(tid);
 
                action_list_t * curr_act_list = func_act_lists->back();
 
-               func_node->incr_exit_count();
-
                /* defer the processing of curr_act_list until the function has exits a few times 
                 * (currently 2 times) so that more information can be gathered to infer nullity predicates.
                 */
+               func_node->incr_exit_count();
                if (func_node->get_exit_count() >= 2) {
                        ModelList<action_list_t *> * action_list_buffer = func_node->get_action_list_buffer();
                        while (action_list_buffer->size() > 0) {
@@ -125,32 +124,30 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
        uint32_t func_id = (*thrd_func_list)[id].back();
        SnapList<action_list_t *> * func_act_lists = (*thrd_func_act_lists)[id];
 
-       if (act->is_write())
+       if (act->is_write()) {
                add_to_write_history(act->get_location(), act->get_write_value());
+               
+       }
 
-       if (func_id == 0)
+       /* the following does not care about actions without a position */
+       if (func_id == 0 || act->get_position() == NULL)
                return;
-       else if ( func_nodes.size() <= func_id )
+
+       if ( func_nodes.size() <= func_id )
                resize_func_nodes( func_id + 1 );
 
        FuncNode * func_node = func_nodes[func_id];
 
-       /* do not care about actions without a position */
-
-       if (act->get_position() == NULL)
-               return;
-
-       if (act->is_read())
-               func_node->store_read(act, tid);
+//     if (act->is_read())
+//             func_node->store_read(act, tid);
 
        /* add to curr_inst_list */
-
        bool second_part_of_rmw = act->is_rmwc() || act->is_rmw();
        if (!second_part_of_rmw) {
                action_list_t * curr_act_list = func_act_lists->back();
                ASSERT(curr_act_list != NULL);
 
-               ModelAction * last_act;
+               ModelAction * last_act = NULL;
                if (curr_act_list->size() != 0)
                        last_act = curr_act_list->back();
 
@@ -172,6 +169,7 @@ FuncNode * ModelHistory::get_func_node(uint32_t func_id)
        return func_nodes[func_id];
 }
 
+/*
 uint64_t ModelHistory::query_last_read(void * location, thread_id_t tid)
 {
        SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
@@ -188,18 +186,29 @@ 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)
 {
-       write_set_t * write_set = write_history.get(location);
+       value_set_t * write_set = write_history.get(location);
 
        if (write_set == NULL) {
-               write_set = new write_set_t();
+               write_set = new value_set_t();
                write_history.put(location, write_set);
        }
 
        write_set->add(write_val);
-       write_locations.add(location);
+}
+
+void ModelHistory::add_to_loc_func_nodes_map(void * location, FuncNode * node)
+{
+       SnapList<FuncNode *> * func_node_list = loc_func_nodes_map.get(location);
+       if (func_node_list == NULL) {
+               func_node_list = new SnapList<FuncNode *>();
+               loc_func_nodes_map.put(location, func_node_list);
+       }
+
+       func_node_list->push_back(node);
 }
 
 void ModelHistory::set_new_exec_flag()
index 36b5848..3bb6156 100644 (file)
--- a/history.h
+++ b/history.h
@@ -7,7 +7,6 @@
 #include "hashset.h"
 #include "threads-model.h"
 
-
 class ModelHistory {
 public:
        ModelHistory();
@@ -27,10 +26,11 @@ public:
 
        ModelVector<FuncNode *> * getFuncNodes() { return &func_nodes; }
        FuncNode * get_func_node(uint32_t func_id);
-       uint64_t query_last_read(void * location, thread_id_t tid);
+//     uint64_t query_last_read(void * location, thread_id_t tid);
 
        void add_to_write_history(void * location, uint64_t write_val);
-       HashTable<void *, write_set_t *, uintptr_t, 4> * getWriteHistory() { return &write_history; }
+       HashTable<void *, value_set_t *, uintptr_t, 4> * getWriteHistory() { return &write_history; }
+       void add_to_loc_func_nodes_map(void * location, FuncNode * node);
 
        void set_new_exec_flag();
        void print_write();
@@ -42,13 +42,14 @@ private:
 
        /* map function names to integer ids */
        HashTable<const char *, uint32_t, uintptr_t, 4, model_malloc, model_calloc, model_free> func_map;
+
        /* map integer ids to function names */
        ModelVector<const char *> func_map_rev;
 
        ModelVector<FuncNode *> func_nodes;
 
-       HashTable<void *, write_set_t *, uintptr_t, 4> write_history;
-       HashSet<void *, uintptr_t, 4> write_locations;
+       HashTable<void *, value_set_t *, uintptr_t, 4> write_history;
+       HashTable<void *, SnapList<FuncNode *> *, uintptr_t, 4> loc_func_nodes_map;
 };
 
 #endif /* __HISTORY_H__ */
index 5802b5d..58a7859 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -40,7 +40,7 @@ ModelChecker::ModelChecker() :
        inspect_plugin(NULL)
 {
        memset(&stats,0,sizeof(struct execution_stats));
-       init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);    // L: user_main_wrapper passes the user program
+       init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);
 #ifdef TLS
        init_thread->setTLS((char *)get_tls_addr());
 #endif