From ae3b87a50d4122a8feb95eddc6b0f208f6c7d5cc Mon Sep 17 00:00:00 2001 From: weiyu Date: Fri, 16 Aug 2019 12:23:29 -0700 Subject: [PATCH] defer the initial update of predicate tree for a better quality tree; generate nullity predicates when new Predicate nodes are created instead of changing unset predicates to nullity later --- funcnode.cc | 39 +++++++++++++++++++-------------------- funcnode.h | 11 ++++++++++- history.cc | 18 ++++++++++++++++-- 3 files changed, 45 insertions(+), 23 deletions(-) diff --git a/funcnode.cc b/funcnode.cc index 940a8f78..3a7e4dbe 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -3,6 +3,7 @@ FuncNode::FuncNode() : predicate_tree_initialized(false), predicate_tree_entry(new Predicate(NULL, true)), + exit_count(0), func_inst_map(), inst_list(), entry_insts(), @@ -239,25 +240,6 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) if (!branch_found && unset_predicates->size() != 0) { ASSERT(unset_predicates->size() == 1); Predicate * one_branch = (*unset_predicates)[0]; - - if (!next_inst->is_single_location()) { - Predicate * another_branch = new Predicate(next_inst); - // another_branch->copy_predicate_expr(one_branch); - - uint64_t next_read = next_act->get_reads_from_value(); - bool isnull = ((void*)next_read == NULL); - if (isnull) { - one_branch->add_predicate_expr(NULLITY, NULL, 1); - another_branch->add_predicate_expr(NULLITY, NULL, 0); - } else { - another_branch->add_predicate_expr(NULLITY, NULL, 1); - one_branch->add_predicate_expr(NULLITY, NULL, 0); - } - - curr_pred->add_child(another_branch); - another_branch->set_parent(curr_pred); - } - curr_pred = one_branch; branch_found = true; } @@ -308,6 +290,24 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) curr_pred = new_pred1; else curr_pred = new_pred2; + } else if (!next_inst->is_single_location()) { + Predicate * new_pred1 = new Predicate(next_inst); + new_pred1->add_predicate_expr(NULLITY, NULL, true); + + Predicate * new_pred2 = new Predicate(next_inst); + new_pred2->add_predicate_expr(NULLITY, NULL, false); + + curr_pred->add_child(new_pred1); + curr_pred->add_child(new_pred2); + new_pred1->set_parent(curr_pred); + new_pred2->set_parent(curr_pred); + + uint64_t next_read = next_act->get_reads_from_value(); + bool isnull = ((void*)next_read == NULL); + if (isnull) + curr_pred = new_pred1; + else + curr_pred = new_pred2; } else { Predicate * new_pred = new Predicate(next_inst); curr_pred->add_child(new_pred); @@ -353,7 +353,6 @@ void FuncNode::deep_update(Predicate * curr_pred) Predicate * parent = curr_pred->get_parent(); parent->add_child(another_branch); -// another_branch.add_children(i); } } diff --git a/funcnode.h b/funcnode.h index c4bf9fed..bbc14db1 100644 --- a/funcnode.h +++ b/funcnode.h @@ -39,8 +39,13 @@ public: void update_predicate_tree(action_list_t * act_list); void deep_update(Predicate * pred); bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable* inst_act_map, SnapVector * unset_predicates); - void print_predicate_tree(); + void incr_exit_count() { exit_count++; } + uint32_t get_exit_count() { return exit_count; } + + ModelList * get_action_list_buffer() { return &action_list_buffer; } + + void print_predicate_tree(); void print_last_read(uint32_t tid); MEMALLOC @@ -50,6 +55,8 @@ private: bool predicate_tree_initialized; Predicate * predicate_tree_entry; // a dummy node whose children are the real entries + uint32_t exit_count; + /* Use source line number as the key of hashtable, to check if * atomic operation with this line number has been added or not */ @@ -63,6 +70,8 @@ private: /* Store the values read by atomic read actions per memory location for each thread */ ModelVector thrd_read_map; + + ModelList action_list_buffer; }; #endif /* __FUNCNODE_H__ */ diff --git a/history.cc b/history.cc index 89d11119..0f90e126 100644 --- a/history.cc +++ b/history.cc @@ -65,9 +65,23 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid) FuncNode * func_node = func_nodes[func_id]; func_node->clear_read_map(tid); - // model_print("hello function %s and thread %d\n", func_node->get_func_name(), tid); action_list_t * curr_act_list = func_act_lists->back(); - func_node->update_tree(curr_act_list); + 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. + */ + if (func_node->get_exit_count() >= 2) { + ModelList * action_list_buffer = func_node->get_action_list_buffer(); + while (action_list_buffer->size() > 0) { + action_list_t * act_list = action_list_buffer->back(); + action_list_buffer->pop_back(); + func_node->update_tree(act_list); + } + + func_node->update_tree(curr_act_list); + } else + func_node->get_action_list_buffer()->push_front(curr_act_list); (*thrd_func_list)[id].pop_back(); func_act_lists->pop_back(); -- 2.34.1