reset memory locations of FuncInsts when new executions start

diff --git a/funcinst.h b/funcinst.h
index 3b2890f0bdafa33ea9e041b23ddfa47987eb3fac..9aec00f6cc3ae74880c4fc3af6a47cec5df28dd3 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -14,7 +14,11 @@ public:
        ~FuncInst();
 
        const char * get_position() const { return position; }
        ~FuncInst();
 
        const char * get_position() const { return position; }

+

        void * get_location() const { return location; }
        void * get_location() const { return location; }

+       void set_location(void * loc) { location = loc; }
+       void reset_location() { location = NULL; }
+

        action_type get_type() const { return type; }
        memory_order get_mo() const { return order; }
        FuncNode * get_func_node() const { return func_node; }
        action_type get_type() const { return type; }
        memory_order get_mo() const { return order; }
        FuncNode * get_func_node() const { return func_node; }

diff --git a/funcnode.cc b/funcnode.cc
index 085ab5bd49e2d2e12ebc82402bf42a39da727905..dc01396575a7baf5ead37d299c64a7389a00bc25 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -1,17 +1,30 @@
 #include "funcnode.h"
 
 #include "funcnode.h"
 

-FuncNode::FuncNode() :
+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(),
        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->add_predicate_expr(NOPREDICATE, NULL, true);
 }
 
 {
        predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
 }
 

+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 (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
+               FuncInst * inst = it->getVal();
+               inst->reset_location();
+       }
+}
+

 /* Check whether FuncInst with the same type, position, and location
  * as act has been added to func_inst_map or not. If not, add it.
  *
 /* Check whether FuncInst with the same type, position, and location
  * as act has been added to func_inst_map or not. If not, add it.
  *


@@ -33,6 +46,11 @@ void FuncNode::add_inst(ModelAction *act)
                FuncInst * inst = func_inst_map.get(position);
 
                ASSERT(inst->get_type() == act->get_type());
                FuncInst * inst = func_inst_map.get(position);
 
                ASSERT(inst->get_type() == act->get_type());

+
+               // locations are set to NULL when new executions start
+               if (inst->get_location() == NULL)
+                       inst->set_location(act->get_location());
+

                if (inst->get_location() != act->get_location())
                        inst->not_single_location();
 
                if (inst->get_location() != act->get_location())
                        inst->not_single_location();
 


@@ -98,9 +116,7 @@ void FuncNode::add_entry_inst(FuncInst * inst)
  */
 void FuncNode::update_tree(action_list_t * act_list)
 {
  */
 void FuncNode::update_tree(action_list_t * act_list)
 {

-       if (act_list == NULL)
-               return;
-       else if (act_list->size() == 0)
+       if (act_list == NULL || act_list->size() == 0)

                return;
 
        /* build inst_list from act_list for later processing */
                return;
 
        /* build inst_list from act_list for later processing */


@@ -125,7 +141,7 @@ void FuncNode::update_tree(action_list_t * act_list)
        update_predicate_tree(&read_act_list);
 //     deep_update(predicate_tree_entry);
 
        update_predicate_tree(&read_act_list);
 //     deep_update(predicate_tree_entry);
 

-       print_predicate_tree();
+//     print_predicate_tree();

 }
 
 /** 
 }
 
 /** 


@@ -171,6 +187,7 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid)
        uint64_t read_from_val = act->get_reads_from_value();
 
        /* resize and initialize */
        uint64_t read_from_val = act->get_reads_from_value();
 
        /* 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);

diff --git a/funcnode.h b/funcnode.h
index bbc14db11617cfaa14b1ec7248c891b06ef47265..c84815cf3326706622b120fca383759555f25ed5 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -6,19 +6,21 @@
 #include "hashtable.h"
 #include "hashset.h"
 #include "predicate.h"
 #include "hashtable.h"
 #include "hashset.h"
 #include "predicate.h"

+#include "history.h"

 
 typedef ModelList<FuncInst *> func_inst_list_mt;
 
 typedef ModelList<FuncInst *> func_inst_list_mt;

-typedef HashTable<void *, uint64_t, uintptr_t, 4, model_malloc, model_calloc, model_free> read_map_t;
+typedef HashTable<void *, uint64_t, uintptr_t, 4> read_map_t;

 
 class FuncNode {
 public:
 
 class FuncNode {
 public:

-       FuncNode();
+       FuncNode(ModelHistory * history);

        ~FuncNode();
 
        uint32_t get_func_id() { return func_id; }
        const char * get_func_name() { return func_name; }
        void set_func_id(uint32_t id) { func_id = id; }
        void set_func_name(const char * name) { func_name = name; }
        ~FuncNode();
 
        uint32_t get_func_id() { return func_id; }
        const char * get_func_name() { return func_name; }
        void set_func_id(uint32_t id) { func_id = id; }
        void set_func_name(const char * name) { func_name = name; }

+       void set_new_exec_flag();

 
        void add_inst(ModelAction *act);
        FuncInst * get_inst(ModelAction *act);
 
        void add_inst(ModelAction *act);
        FuncInst * get_inst(ModelAction *act);


@@ -52,6 +54,7 @@ public:
 private:
        uint32_t func_id;
        const char * func_name;
 private:
        uint32_t func_id;
        const char * func_name;

+       ModelHistory * history;

        bool predicate_tree_initialized;
        Predicate * predicate_tree_entry;       // a dummy node whose children are the real entries
 
        bool predicate_tree_initialized;
        Predicate * predicate_tree_entry;       // a dummy node whose children are the real entries
 

diff --git a/history.cc b/history.cc
index 0f90e12662648be6995bef48933d153223b40bf1..2dbc556e7424c6ea8eb46499afac0ce68ae1bcd5 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -66,6 +66,7 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
                func_node->clear_read_map(tid);
 
                action_list_t * curr_act_list = func_act_lists->back();
                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 
                func_node->incr_exit_count();
 
                /* defer the processing of curr_act_list until the function has exits a few times 


@@ -101,7 +102,7 @@ void ModelHistory::resize_func_nodes(uint32_t new_size)
 
        for (uint32_t id = old_size;id < new_size;id++) {
                const char * func_name = func_map_rev[id];
 
        for (uint32_t id = old_size;id < new_size;id++) {
                const char * func_name = func_map_rev[id];

-               FuncNode * func_node = new FuncNode();
+               FuncNode * func_node = new FuncNode(this);

                func_node->set_func_id(id);
                func_node->set_func_name(func_name);
                func_nodes[id] = func_node;
                func_node->set_func_id(id);
                func_node->set_func_name(func_name);
                func_nodes[id] = func_node;


@@ -124,6 +125,9 @@ 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())
+               add_to_write_history(act->get_location(), act->get_write_value());
+

        if (func_id == 0)
                return;
        else if ( func_nodes.size() <= func_id )
        if (func_id == 0)
                return;
        else if ( func_nodes.size() <= func_id )


@@ -132,16 +136,15 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
        FuncNode * func_node = func_nodes[func_id];
 
        /* do not care about actions without a position */
        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->get_position() == NULL)
                return;
 
        if (act->is_read())
                func_node->store_read(act, tid);
 

-       if (act->is_write())
-               add_to_write_history(act->get_location(), act->get_write_value());
-

        /* 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();
        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();


@@ -199,6 +202,14 @@ void ModelHistory::add_to_write_history(void * location, uint64_t write_val)
        write_locations.add(location);
 }
 
        write_locations.add(location);
 }
 

+void ModelHistory::set_new_exec_flag()
+{
+       for (uint i = 1; i < func_nodes.size(); i++) {
+               FuncNode * func_node = func_nodes[i];
+               func_node->set_new_exec_flag();
+       }
+}
+

 void ModelHistory::print_write()
 {
 }
 void ModelHistory::print_write()
 {
 }

diff --git a/history.h b/history.h
index 5f5e731840a647e73e70490b72b314d83d865fe7..36b584831fdcba9ac3f1112e700dcb6650b3f6f4 100644 (file)
--- a/history.h
+++ b/history.h
@@ -32,6 +32,7 @@ public:
        void add_to_write_history(void * location, uint64_t write_val);
        HashTable<void *, write_set_t *, uintptr_t, 4> * getWriteHistory() { return &write_history; }
 
        void add_to_write_history(void * location, uint64_t write_val);
        HashTable<void *, write_set_t *, uintptr_t, 4> * getWriteHistory() { return &write_history; }
 

+       void set_new_exec_flag();

        void print_write();
        void print_func_node();
 
        void print_write();
        void print_func_node();
 

diff --git a/model.cc b/model.cc
index f3a7b6a77bad087a2dd0ff15e138cbcf8f32d79a..5802b5d02dd77da3d799bab6400ee261848b2c58 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -264,6 +264,7 @@ bool ModelChecker::next_execution()
 // test code
        execution_number ++;
        reset_to_initial_state();
 // test code
        execution_number ++;
        reset_to_initial_state();

+       history->set_new_exec_flag();

        return false;
 }
 
        return false;
 }