X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcnode.cc;h=dc903ef82a49782f857c870a47ff793a9578aec1;hp=e5279bd1fd72598642be43265d4fe039cbd744ba;hb=06e698d4ca55451771b8cfcd71f03088447464f7;hpb=0d3c4eca7d657d93c5a30681f22d9856847370f9 diff --git a/funcnode.cc b/funcnode.cc index e5279bd1..dc903ef8 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -6,6 +6,7 @@ #include "concretepredicate.h" #include "model.h" +#include FuncNode::FuncNode(ModelHistory * history) : history(history), @@ -14,13 +15,22 @@ FuncNode::FuncNode(ModelHistory * history) : func_inst_map(), inst_list(), entry_insts(), + inst_pred_map(128), + inst_id_map(128), + loc_act_map(128), predicate_tree_position(), + predicate_leaves(), + leaves_tmp_storage(), + weight_debug_vec(), + failed_predicates(), edge_table(32), out_edges() { predicate_tree_entry = new Predicate(NULL, true); predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true); + predicate_tree_exit = new Predicate(NULL, false, true); + predicate_tree_exit->set_depth(MAX_DEPTH); /* Snapshot data structures below */ action_list_buffer = new SnapList(); @@ -260,16 +270,15 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) return; incr_marker(); - - /* Map a FuncInst to the its predicate */ - HashTable inst_pred_map(128); - - // Number FuncInsts to detect loops - HashTable inst_id_map(128); uint32_t inst_counter = 0; - /* Only need to store the locations of read actions */ - HashTable loc_act_map(128); + // Clear hashtables + loc_act_map.reset(); + inst_pred_map.reset(); + inst_id_map.reset(); + + // Clear the set of leaves encountered in this path + leaves_tmp_storage.clear(); sllnode *it = act_list->begin(); Predicate * curr_pred = predicate_tree_entry; @@ -278,19 +287,16 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) FuncInst * next_inst = get_inst(next_act); next_inst->set_associated_act(next_act, marker); - SnapVector unset_predicates = SnapVector(); - bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicates); + Predicate * unset_predicate = NULL; + bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicate); // A branch with unset predicate expression is detected - if (!branch_found && unset_predicates.size() != 0) { - ASSERT(unset_predicates.size() == 1); - Predicate * one_branch = unset_predicates[0]; - - bool amended = amend_predicate_expr(&curr_pred, next_inst, next_act); + if (!branch_found && unset_predicate != NULL) { + bool amended = amend_predicate_expr(curr_pred, next_inst, next_act); if (amended) continue; else { - curr_pred = one_branch; + curr_pred = unset_predicate; branch_found = true; } } @@ -305,6 +311,10 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) Predicate * old_pred = inst_pred_map.get(next_inst); Predicate * back_pred = old_pred->get_parent(); + // For updating weights + leaves_tmp_storage.push_back(curr_pred); + + // Add to the set of backedges curr_pred->add_backedge(back_pred); curr_pred = back_pred; continue; @@ -314,8 +324,8 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) // Generate new branches 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); + infer_predicates(next_inst, next_act, &half_pred_expressions); + generate_predicates(curr_pred, next_inst, &half_pred_expressions); continue; } @@ -323,6 +333,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) curr_pred->set_write(true); if (next_act->is_read()) { + /* Only need to store the locations of read actions */ loc_act_map.put(next_act->get_location(), next_act); } @@ -334,7 +345,13 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) curr_pred->incr_expl_count(); } - curr_pred->set_exit(predicate_tree_exit); + if (curr_pred->get_exit() == NULL) { + // Exit predicate is unset yet + curr_pred->set_exit(predicate_tree_exit); + } + + leaves_tmp_storage.push_back(curr_pred); + update_predicate_tree_weight(); } /* Given curr_pred and next_inst, find the branch following curr_pred that @@ -342,7 +359,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) * @return true if branch found, false otherwise. */ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, -ModelAction * next_act, SnapVector * unset_predicates) + ModelAction * next_act, Predicate ** unset_predicate) { /* Check if a branch with func_inst and corresponding predicate exists */ bool branch_found = false; @@ -355,51 +372,58 @@ ModelAction * next_act, SnapVector * unset_predicates) /* Check against predicate expressions */ bool predicate_correct = true; PredExprSet * pred_expressions = branch->get_pred_expressions(); - PredExprSetIter * pred_expr_it = pred_expressions->iterator(); /* Only read and rmw actions my have unset predicate expressions */ if (pred_expressions->getSize() == 0) { predicate_correct = false; - unset_predicates->push_back(branch); + if (*unset_predicate == NULL) + *unset_predicate = branch; + else + ASSERT(false); + + continue; } + PredExprSetIter * pred_expr_it = pred_expressions->iterator(); while (pred_expr_it->hasNext()) { pred_expr * pred_expression = pred_expr_it->next(); uint64_t last_read, next_read; bool equality; switch(pred_expression->token) { - case NOPREDICATE: - predicate_correct = true; - break; - case EQUALITY: - FuncInst * to_be_compared; - ModelAction * last_act; - - to_be_compared = pred_expression->func_inst; - last_act = to_be_compared->get_associated_act(marker); - - last_read = last_act->get_reads_from_value(); - next_read = next_act->get_reads_from_value(); - equality = (last_read == next_read); - if (equality != pred_expression->value) - predicate_correct = false; + case NOPREDICATE: + predicate_correct = true; + break; + case EQUALITY: + FuncInst * to_be_compared; + ModelAction * last_act; + + to_be_compared = pred_expression->func_inst; + last_act = to_be_compared->get_associated_act(marker); + + last_read = last_act->get_reads_from_value(); + next_read = next_act->get_reads_from_value(); + equality = (last_read == next_read); + if (equality != pred_expression->value) + predicate_correct = false; - break; - case NULLITY: - next_read = next_act->get_reads_from_value(); - // TODO: implement likely to be null - equality = ( (void*) (next_read & 0xffffffff) == NULL); - if (equality != pred_expression->value) - predicate_correct = false; - break; - default: + break; + case NULLITY: + next_read = next_act->get_reads_from_value(); + // TODO: implement likely to be null + equality = ( (void*) (next_read & 0xffffffff) == NULL); + if (equality != pred_expression->value) predicate_correct = false; - model_print("unkown predicate token\n"); - break; + break; + default: + predicate_correct = false; + model_print("unkown predicate token\n"); + break; } } + delete pred_expr_it; + if (predicate_correct) { *curr_pred = branch; branch_found = true; @@ -412,15 +436,14 @@ ModelAction * next_act, SnapVector * unset_predicates) /* Infer predicate expressions, which are generated in FuncNode::generate_predicates */ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act, -HashTable * loc_act_map, -SnapVector * half_pred_expressions) + SnapVector * half_pred_expressions) { void * loc = next_act->get_location(); if (next_inst->is_read()) { /* read + rmw */ - if ( loc_act_map->contains(loc) ) { - ModelAction * last_act = loc_act_map->get(loc); + if ( loc_act_map.contains(loc) ) { + ModelAction * last_act = loc_act_map.get(loc); FuncInst * last_inst = get_inst(last_act); struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst); half_pred_expressions->push_back(expression); @@ -431,14 +454,16 @@ SnapVector * half_pred_expressions) loc_set_iter * loc_it = loc_may_equal->iterator(); while (loc_it->hasNext()) { void * neighbor = loc_it->next(); - if (loc_act_map->contains(neighbor)) { - ModelAction * last_act = loc_act_map->get(neighbor); + if (loc_act_map.contains(neighbor)) { + ModelAction * last_act = loc_act_map.get(neighbor); FuncInst * last_inst = get_inst(last_act); struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst); half_pred_expressions->push_back(expression); } } + + delete loc_it; } } else { // next_inst is not single location @@ -457,17 +482,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, -SnapVector * half_pred_expressions) +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 */ @@ -504,10 +533,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]; @@ -516,18 +551,27 @@ 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(); + ModelVector * children = curr_pred->get_children(); + + Predicate * unset_pred = NULL; + for (uint i = 0;i < children->size();i++) { + Predicate * child = (*children)[i]; + if (child->get_func_inst() == next_inst) { + unset_pred = child; + break; + } + } + 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); @@ -562,6 +606,8 @@ void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc) uint64_t val = it->next(); add_to_val_loc_map(val, loc); } + + delete it; } void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations) @@ -590,6 +636,8 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location } _neighbors->add(new_loc); } + + delete loc_it; } /* Every time a thread enters a function, set its position to the predicate tree entry */ @@ -720,6 +768,172 @@ int FuncNode::compute_distance(FuncNode * target, int max_step) return -1; } +void FuncNode::add_failed_predicate(Predicate * pred) +{ + failed_predicates.add(pred); +} + +/* Implement quick sort to sort leaves before assigning base scores */ +template +static int partition(ModelVector<_Tp *> * arr, int low, int high) +{ + 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 ++; + _Tp * tmp = (*arr)[i]; + (*arr)[i] = (*arr)[j]; + (*arr)[j] = tmp; + } + } + + _Tp * tmp = (*arr)[i + 1]; + (*arr)[i + 1] = (*arr)[high]; + (*arr)[high] = tmp; + + return i + 1; +} + +/* Implement quick sort to sort leaves before assigning base scores */ +template +static void quickSort(ModelVector<_Tp *> * 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_initial_weight() +{ + PredSetIter * it = predicate_leaves.iterator(); + leaves_tmp_storage.clear(); + + while (it->hasNext()) { + Predicate * pred = it->next(); + double weight = 100.0 / sqrt(pred->get_expl_count() + pred->get_fail_count() + 1); + pred->set_weight(weight); + leaves_tmp_storage.push_back(pred); + } + delete it; + + quickSort(&leaves_tmp_storage, 0, leaves_tmp_storage.size() - 1); + + // assign scores for internal nodes; + while ( !leaves_tmp_storage.empty() ) { + Predicate * leaf = leaves_tmp_storage.back(); + leaves_tmp_storage.pop_back(); + + Predicate * curr = leaf->get_parent(); + while (curr != NULL) { + if (curr->get_weight() != 0) { + // Has been exlpored + break; + } + + ModelVector * children = curr->get_children(); + double weight_sum = 0; + bool has_unassigned_node = false; + + for (uint i = 0;i < children->size();i++) { + Predicate * child = (*children)[i]; + + // If a child has unassigned weight + double weight = child->get_weight(); + if (weight == 0) { + has_unassigned_node = true; + break; + } else + weight_sum += weight; + } + + if (!has_unassigned_node) { + double average_weight = (double) weight_sum / (double) children->size(); + double weight = average_weight * pow(0.9, curr->get_depth()); + curr->set_weight(weight); + } else + break; + + curr = curr->get_parent(); + } + } +} + +void FuncNode::update_predicate_tree_weight() +{ + if (marker == 2) { + // Predicate tree is initially built + assign_initial_weight(); + return; + } + + weight_debug_vec.clear(); + + PredSetIter * it = failed_predicates.iterator(); + while (it->hasNext()) { + Predicate * pred = it->next(); + leaves_tmp_storage.push_back(pred); + } + delete it; + failed_predicates.reset(); + + quickSort(&leaves_tmp_storage, 0, leaves_tmp_storage.size() - 1); + for (uint i = 0;i < leaves_tmp_storage.size();i++) { + Predicate * pred = leaves_tmp_storage[i]; + double weight = 100.0 / sqrt(pred->get_expl_count() + pred->get_fail_count() + 1); + pred->set_weight(weight); + } + + // Update weights in internal nodes + while ( !leaves_tmp_storage.empty() ) { + Predicate * leaf = leaves_tmp_storage.back(); + leaves_tmp_storage.pop_back(); + + Predicate * curr = leaf->get_parent(); + while (curr != NULL) { + ModelVector * children = curr->get_children(); + double weight_sum = 0; + bool has_unassigned_node = false; + + for (uint i = 0;i < children->size();i++) { + Predicate * child = (*children)[i]; + + double weight = child->get_weight(); + if (weight != 0) + weight_sum += weight; + else if ( predicate_leaves.contains(child) ) { + // If this child is a leaf + double weight = 100.0 / sqrt(child->get_expl_count() + 1); + child->set_weight(weight); + weight_sum += weight; + } else { + has_unassigned_node = true; + weight_debug_vec.push_back(child); // For debugging purpose + break; + } + } + + if (!has_unassigned_node) { + double average_weight = (double) weight_sum / (double) children->size(); + double weight = average_weight * pow(0.9, curr->get_depth()); + curr->set_weight(weight); + } else + break; + + curr = curr->get_parent(); + } + } + + for (uint i = 0;i < weight_debug_vec.size();i++) { + Predicate * tmp = weight_debug_vec[i]; + ASSERT( tmp->get_weight() != 0 ); + } +} + void FuncNode::print_predicate_tree() { model_print("digraph function_%s {\n", func_name); @@ -727,22 +941,3 @@ void FuncNode::print_predicate_tree() predicate_tree_exit->print_predicate(); model_print("}\n"); // end of graph } - -void FuncNode::print_val_loc_map() -{ -/* - value_set_iter * val_it = values_may_read_from->iterator(); - while (val_it->hasNext()) { - uint64_t value = val_it->next(); - model_print("val %llx: ", value); - - loc_set_t * locations = val_loc_map->get(value); - loc_set_iter * loc_it = locations->iterator(); - while (loc_it->hasNext()) { - void * location = loc_it->next(); - model_print("%p ", location); - } - model_print("\n"); - } - */ -}