add helper functions; prepare for computing which memory locations may store the...

diff --git a/classlist.h b/classlist.h
index 664301e9b5045c6dd51478e0b3e5f1cfb7e0bba4..5a17449c9dddcc643497cb3f1ff37def00994a53 100644 (file)
--- a/classlist.h
+++ b/classlist.h
@@ -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 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 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
 
 extern volatile int modellock;
 #endif

diff --git a/funcnode.cc b/funcnode.cc
index dc01396575a7baf5ead37d299c64a7389a00bc25..ccb930fa2581def84d39175859124735f8874dfc 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -3,26 +3,33 @@
 FuncNode::FuncNode(ModelHistory * history) :
        history(history),
        predicate_tree_initialized(false),
 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(),
        exit_count(0),
        func_inst_map(),
        inst_list(),
        entry_insts(),

-       thrd_read_map(),
+//     thrd_read_map(),

        action_list_buffer()
 {
        action_list_buffer()
 {

+       predicate_tree_entry = new Predicate(NULL, true);

        predicate_tree_entry->add_predicate_expr(NOPREDICATE, 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()
 {
 }
 
 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();
        }
 
        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
 }
 
 /* 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;
 
        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;
        /* 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);
 
 
                inst_list.push_back(func_inst);
 

-               if (func_inst->is_read())
+               if (func_inst->is_read()) {

                        read_act_list.push_back(act);
                        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);
        }
 
 //     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)
 {
  * 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();
 
        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);
        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);
 
        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)
 {
 }
 
 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];
 
        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;
        if ( !read_map->contains(location) )
                return VALUE_NONE;
 
        uint64_t read_val = read_map->get(location);
        return read_val;

+*/

 }
 
 /* @param tid thread id
 }
 
 /* @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)
 {
  */
 void FuncNode::clear_read_map(uint32_t tid)
 {

+/*

        if (thrd_read_map.size() <= tid)
                return;
 
        thrd_read_map[tid]->reset();
        if (thrd_read_map.size() <= tid)
                return;
 
        thrd_read_map[tid]->reset();

+*/

 }
 
 void FuncNode::update_predicate_tree(action_list_t * act_list)
 }
 
 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;
 }
 
        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);
 void FuncNode::print_predicate_tree()
 {
        model_print("digraph function_%s {\n", func_name);

diff --git a/funcnode.h b/funcnode.h
index c84815cf3326706622b120fca383759555f25ed5..6e08fc26d40d62582bbf567519f16f6696c2160d 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -47,6 +47,9 @@ public:
 
        ModelList<action_list_t *> * get_action_list_buffer() { return &action_list_buffer; }
 
 
        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);
 
        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 */
        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;
        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__ */
 };
 
 #endif /* __FUNCNODE_H__ */

diff --git a/history.cc b/history.cc
index 2dbc556e7424c6ea8eb46499afac0ce68ae1bcd5..68e8575fa25dadd204958dbbf5d61be239a58e67 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -14,8 +14,8 @@ ModelHistory::ModelHistory() :
        func_map(),
        func_map_rev(),
        func_nodes(),
        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)
 {}
 
 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];
 
        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();
 
 
                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.
                 */
                /* 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) {
                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];
 
        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());
                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;
                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];
 
                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 */
 
        /* 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);
 
        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();
 
                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];
 }
 
        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();
 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;
 }
 
        return last_read_val;
 }

+*/

 
 void ModelHistory::add_to_write_history(void * location, uint64_t write_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) {
 
        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_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()
 }
 
 void ModelHistory::set_new_exec_flag()

diff --git a/history.h b/history.h
index 36b584831fdcba9ac3f1112e700dcb6650b3f6f4..3bb615640eca3e86728675db2c366c508689d4d4 100644 (file)
--- a/history.h
+++ b/history.h
@@ -7,7 +7,6 @@
 #include "hashset.h"
 #include "threads-model.h"
 
 #include "hashset.h"
 #include "threads-model.h"
 

-

 class ModelHistory {
 public:
        ModelHistory();
 class ModelHistory {
 public:
        ModelHistory();


@@ -27,10 +26,11 @@ public:
 
        ModelVector<FuncNode *> * getFuncNodes() { return &func_nodes; }
        FuncNode * get_func_node(uint32_t func_id);
 
        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);
 
        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();
 
        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 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;
 
        /* 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__ */
 };
 
 #endif /* __HISTORY_H__ */

diff --git a/model.cc b/model.cc
index 5802b5d02dd77da3d799bab6400ee261848b2c58..58a785923d2826673cfb259962cd306dda3cbed1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -40,7 +40,7 @@ ModelChecker::ModelChecker() :
        inspect_plugin(NULL)
 {
        memset(&stats,0,sizeof(struct execution_stats));
        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
 #ifdef TLS
        init_thread->setTLS((char *)get_tls_addr());
 #endif