From 7d703e06ecec3abb3c173378e18ad6c28eb6f3d7 Mon Sep 17 00:00:00 2001 From: weiyu Date: Tue, 10 Dec 2019 11:09:27 -0800 Subject: [PATCH] Store the set of predicate leaves in FuncNode --- funcnode.cc | 92 +++++++++++++++++++++++++++++++++++----------------- funcnode.h | 5 +-- predicate.cc | 11 ------- predicate.h | 6 ---- 4 files changed, 66 insertions(+), 48 deletions(-) diff --git a/funcnode.cc b/funcnode.cc index 663447bf..5bb73b98 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -16,6 +16,7 @@ FuncNode::FuncNode(ModelHistory * history) : inst_list(), entry_insts(), predicate_tree_position(), + predicate_leaves(), edge_table(32), out_edges() { @@ -23,7 +24,6 @@ FuncNode::FuncNode(ModelHistory * history) : predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true); predicate_tree_exit = new Predicate(NULL, false, true); - predicate_tree_exit->alloc_pre_exit_predicates(); predicate_tree_exit->set_depth(MAX_DEPTH); /* Snapshot data structures below */ @@ -290,7 +290,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) ASSERT(unset_predicates.size() == 1); Predicate * one_branch = unset_predicates[0]; - bool amended = amend_predicate_expr(&curr_pred, next_inst, next_act); + bool amended = amend_predicate_expr(curr_pred, next_inst, next_act); if (amended) continue; else { @@ -319,7 +319,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) if (!branch_found) { SnapVector half_pred_expressions; infer_predicates(next_inst, next_act, &loc_act_map, &half_pred_expressions); - generate_predicates(&curr_pred, next_inst, &half_pred_expressions); + generate_predicates(curr_pred, next_inst, &half_pred_expressions); continue; } @@ -464,17 +464,21 @@ SnapVector * half_pred_expressions) } /* Able to generate complex predicates when there are multiple predciate expressions */ -void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, +void FuncNode::generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector * half_pred_expressions) { if (half_pred_expressions->size() == 0) { Predicate * new_pred = new Predicate(next_inst); - (*curr_pred)->add_child(new_pred); - new_pred->set_parent(*curr_pred); + curr_pred->add_child(new_pred); + new_pred->set_parent(curr_pred); + + /* Maintain predicate leaves */ + predicate_leaves.add(new_pred); + predicate_leaves.remove(curr_pred); /* entry predicates and predicates containing pure write actions * have no predicate expressions */ - if ( (*curr_pred)->is_entry_predicate() ) + if ( curr_pred->is_entry_predicate() ) new_pred->add_predicate_expr(NOPREDICATE, NULL, true); else if (next_inst->is_write()) { /* next_inst->is_write() <==> pure writes */ @@ -511,10 +515,16 @@ SnapVector * half_pred_expressions) for (uint i = 0;i < predicates.size();i++) { Predicate * pred= predicates[i]; - (*curr_pred)->add_child(pred); - pred->set_parent(*curr_pred); + curr_pred->add_child(pred); + pred->set_parent(curr_pred); + + /* Add new predicate leaves */ + predicate_leaves.add(pred); } + /* Remove predicate node that has children */ + predicate_leaves.remove(curr_pred); + /* Free memories allocated by infer_predicate */ for (uint i = 0;i < half_pred_expressions->size();i++) { struct half_pred_expr * tmp = (*half_pred_expressions)[i]; @@ -523,18 +533,18 @@ SnapVector * half_pred_expressions) } /* Amend predicates that contain no predicate expressions. Currenlty only amend with NULLITY predicates */ -bool FuncNode::amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act) +bool FuncNode::amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act) { // there should only be only child - Predicate * unset_pred = (*curr_pred)->get_children()->back(); + Predicate * unset_pred = curr_pred->get_children()->back(); uint64_t read_val = next_act->get_reads_from_value(); // only generate NULLITY predicate when it is actually NULL. if ( !next_inst->is_single_location() && (void*)read_val == NULL ) { Predicate * new_pred = new Predicate(next_inst); - (*curr_pred)->add_child(new_pred); - new_pred->set_parent(*curr_pred); + curr_pred->add_child(new_pred); + new_pred->set_parent(curr_pred); unset_pred->add_predicate_expr(NULLITY, NULL, false); new_pred->add_predicate_expr(NULLITY, NULL, true); @@ -727,26 +737,50 @@ int FuncNode::compute_distance(FuncNode * target, int max_step) return -1; } -void FuncNode::assign_base_score() +/* Implement quick sort to sort leaves before assigning base scores */ +static int partition(SnapVector * arr, int low, int high) { - SnapVector leaves; - SnapList queue; - queue.push_front(predicate_tree_entry); - - // assign leaf score - while ( !queue.empty() ) { - Predicate * node = queue.back(); - queue.pop_back(); - - ModelVector * children = node->get_children(); - if (children->empty()) { - node->set_weight(1); - leaves.push_back(node); + unsigned int pivot = (*arr)[high]->get_depth(); + int i = low - 1; + + for (int j = low; j <= high - 1; j++) { + if ( (*arr)[j]->get_depth() < pivot ) { + i++; + Predicate *tmp = (*arr)[i]; + (*arr)[i] = (*arr)[j]; + (*arr)[j] = tmp; } + } + + Predicate * tmp = (*arr)[i + 1]; + (*arr)[i + 1] = (*arr)[high]; + (*arr)[high] = tmp; - for (uint i = 0; i < children->size(); i++) - queue.push_front( (*children)[i] ); + return i + 1; +} + +/* Implement quick sort to sort leaves before assigning base scores */ +static void quickSort(SnapVector * arr, int low, int high) +{ + if (low < high) { + int pi = partition(arr, low, high); + + quickSort(arr, low, pi - 1); + quickSort(arr, pi + 1, high); } +} + +void FuncNode::assign_base_score() +{ + PredSetIter * it = predicate_leaves.iterator(); + SnapVector leaves; + while (it->hasNext()) { + Predicate * pred = it->next(); + pred->set_weight(1); + leaves.push_back(pred); + } + + quickSort(&leaves, 0, leaves.size() - 1); // assign scores for internal nodes; while ( !leaves.empty() ) { diff --git a/funcnode.h b/funcnode.h index ea0be029..ecb270b0 100644 --- a/funcnode.h +++ b/funcnode.h @@ -88,8 +88,8 @@ private: func_inst_list_mt entry_insts; void infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable * loc_act_map, SnapVector * half_pred_expressions); - void generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, SnapVector * half_pred_expressions); - bool amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act); + void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector * half_pred_expressions); + bool amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act); /* Store action_lists when calls to update_tree are deferred */ SnapList * action_list_buffer; @@ -110,6 +110,7 @@ private: /* Run-time position in the predicate tree for each thread */ ModelVector predicate_tree_position; + PredSet predicate_leaves; /* Store the relation between this FuncNode and other FuncNodes */ HashTable edge_table; diff --git a/predicate.cc b/predicate.cc index eb979f88..b2c6e605 100644 --- a/predicate.cc +++ b/predicate.cc @@ -64,17 +64,6 @@ void Predicate::set_parent(Predicate * parent_pred) void Predicate::set_exit(Predicate * exit_pred) { exit = exit_pred; - exit_pred->add_pre_exit_predicate(this); -} - -void Predicate::alloc_pre_exit_predicates() -{ - pre_exit_predicates = new ModelVector(); -} - -void Predicate::add_pre_exit_predicate(Predicate * pred) -{ - pre_exit_predicates->push_back(pred); } void Predicate::copy_predicate_expr(Predicate * other) diff --git a/predicate.h b/predicate.h index 0512835f..8b1e7c81 100644 --- a/predicate.h +++ b/predicate.h @@ -38,9 +38,6 @@ public: bool is_entry_predicate() { return entry_predicate; } void set_entry_predicate() { entry_predicate = true; } - void alloc_pre_exit_predicates(); - void add_pre_exit_predicate(Predicate * pred); - /* Whether func_inst does write or not */ bool is_write() { return does_write; } void set_write(bool is_write) { does_write = is_write; } @@ -84,9 +81,6 @@ private: Predicate * parent; Predicate * exit; - /* Predicates precede exit nodes. Only used by exit predicates */ - ModelVector * pre_exit_predicates; - /* May have multiple back edges, e.g. nested loops */ PredSet backedges; }; -- 2.34.1