From d29571ea49a6abb1b291e547b497ea914da1bef2 Mon Sep 17 00:00:00 2001 From: weiyu Date: Tue, 20 Aug 2019 15:19:59 -0700 Subject: [PATCH] reset memory locations of FuncInsts when new executions start --- funcinst.h | 4 ++++ funcnode.cc | 29 +++++++++++++++++++++++------ funcnode.h | 7 +++++-- history.cc | 19 +++++++++++++++---- history.h | 1 + model.cc | 1 + 6 files changed, 49 insertions(+), 12 deletions(-) diff --git a/funcinst.h b/funcinst.h index 3b2890f0..9aec00f6 100644 --- a/funcinst.h +++ b/funcinst.h @@ -14,7 +14,11 @@ public: ~FuncInst(); const char * get_position() const { return position; } + 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; } diff --git a/funcnode.cc b/funcnode.cc index 085ab5bd..dc013965 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -1,17 +1,30 @@ #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(), - thrd_read_map() + thrd_read_map(), + action_list_buffer() { 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 * 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. * @@ -33,6 +46,11 @@ void FuncNode::add_inst(ModelAction *act) 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(); @@ -98,9 +116,7 @@ void FuncNode::add_entry_inst(FuncInst * inst) */ 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 */ @@ -125,7 +141,7 @@ void FuncNode::update_tree(action_list_t * act_list) 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 */ + 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 bbc14db1..c84815cf 100644 --- a/funcnode.h +++ b/funcnode.h @@ -6,19 +6,21 @@ #include "hashtable.h" #include "hashset.h" #include "predicate.h" +#include "history.h" typedef ModelList func_inst_list_mt; -typedef HashTable read_map_t; +typedef HashTable read_map_t; 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; } + void set_new_exec_flag(); void add_inst(ModelAction *act); FuncInst * get_inst(ModelAction *act); @@ -52,6 +54,7 @@ public: 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 diff --git a/history.cc b/history.cc index 0f90e126..2dbc556e 100644 --- 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->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]; - 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; @@ -124,6 +125,9 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) uint32_t func_id = (*thrd_func_list)[id].back(); SnapList * 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 ) @@ -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 */ + 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 */ + 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); } +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() { } diff --git a/history.h b/history.h index 5f5e7318..36b58483 100644 --- a/history.h +++ b/history.h @@ -32,6 +32,7 @@ public: void add_to_write_history(void * location, uint64_t write_val); HashTable * getWriteHistory() { return &write_history; } + void set_new_exec_flag(); void print_write(); void print_func_node(); diff --git a/model.cc b/model.cc index f3a7b6a7..5802b5d0 100644 --- a/model.cc +++ b/model.cc @@ -264,6 +264,7 @@ bool ModelChecker::next_execution() // test code execution_number ++; reset_to_initial_state(); + history->set_new_exec_flag(); return false; } -- 2.34.1