X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcnode.cc;h=d328a4c5d24f6753fe0faf9338e153bc7284072a;hp=fb3a075336ad994ba26eb99461c83adb648a913e;hb=70acabc306bc3014b3698e394908faf23a66a0b8;hpb=8c52c96262bbb96bcb4d18706daf8dbd77990b1d diff --git a/funcnode.cc b/funcnode.cc index fb3a0753..d328a4c5 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -2,39 +2,44 @@ FuncNode::FuncNode(ModelHistory * history) : history(history), - predicate_tree_initialized(false), exit_count(0), func_inst_map(), inst_list(), entry_insts(), -// thrd_read_map(), - action_list_buffer() + predicate_tree_position(), + edge_table(32), + out_edges() { predicate_tree_entry = new Predicate(NULL, true); predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true); - // memory will be reclaimed after each execution + // Memories that are reclaimed after each execution + action_list_buffer = new SnapList(); read_locations = new loc_set_t(); + write_locations = new loc_set_t(); val_loc_map = new HashTable(); loc_may_equal_map = new HashTable(); - values_may_read_from = new value_set_t(); + thrd_inst_act_map = new SnapVector(); + + //values_may_read_from = new value_set_t(); } -/* Reallocate some snapshotted memories when new executions start */ +/* Reallocate snapshotted memories when new executions start */ 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(); + inst->unset_location(); } + action_list_buffer = new SnapList(); read_locations = new loc_set_t(); + write_locations = new loc_set_t(); val_loc_map = new HashTable(); loc_may_equal_map = new HashTable(); - values_may_read_from = new value_set_t(); + thrd_inst_act_map = new SnapVector(); + + //values_may_read_from = new value_set_t(); } /* Check whether FuncInst with the same type, position, and location @@ -135,42 +140,56 @@ void FuncNode::update_tree(action_list_t * act_list) /* build inst_list from act_list for later processing */ func_inst_list_t inst_list; - action_list_t read_act_list; + action_list_t rw_act_list; for (sllnode * it = act_list->begin(); it != NULL; it = it->getNext()) { ModelAction * act = it->getVal(); FuncInst * func_inst = get_inst(act); + void * loc = act->get_location(); if (func_inst == NULL) continue; inst_list.push_back(func_inst); + bool act_added = false; + + if (act->is_write()) { + rw_act_list.push_back(act); + act_added = true; + if (!write_locations->contains(loc)) { + write_locations->add(loc); + history->update_loc_wr_func_nodes_map(loc, this); + } - if (func_inst->is_read()) { - read_act_list.push_back(act); + } - /* the first time an action reads from some location, import all the values that have - * been written to this location from ModelHistory and notify ModelHistory that this - * FuncNode may read from this location. + if (act->is_read()) { + if (!act_added) + rw_act_list.push_back(act); + + /* If func_inst may only read_from a single location, then: + * + * The first time an action reads from some location, + * import all the values that have been written to this + * location from ModelHistory and notify ModelHistory + * that this FuncNode may read from this location. */ - void * loc = act->get_location(); - if (!read_locations->contains(loc)) { + if (!read_locations->contains(loc) && func_inst->is_single_location()) { read_locations->add(loc); value_set_t * write_values = write_history->get(loc); add_to_val_loc_map(write_values, loc); - history->add_to_loc_func_nodes_map(loc, this); + history->update_loc_func_nodes_map(loc, this); } } } - model_print("function %s\n", func_name); +// model_print("function %s\n", func_name); // print_val_loc_map(); update_inst_tree(&inst_list); - update_predicate_tree(&read_act_list); -// deep_update(predicate_tree_entry); + update_predicate_tree(&rw_act_list); - print_predicate_tree(); +// print_predicate_tree(); } /** @@ -206,72 +225,19 @@ void FuncNode::update_inst_tree(func_inst_list_t * inst_list) } } -/* @param tid thread id - * Store the values read by atomic read actions into thrd_read_map */ -void FuncNode::store_read(ModelAction * act, uint32_t tid) -{ -/* - ASSERT(act); - - void * location = act->get_location(); - 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); - for (uint32_t i = old_size; i < tid + 1;i++) - thrd_read_map[i] = new read_map_t(); - } - - read_map_t * read_map = thrd_read_map[tid]; - read_map->put(location, read_from_val); -*/ -} - -uint64_t FuncNode::query_last_read(void * location, uint32_t tid) -{ -/* - if (thrd_read_map.size() <= tid) - return VALUE_NONE; - - read_map_t * read_map = thrd_read_map[tid]; - - // last read value not found - if ( !read_map->contains(location) ) - return VALUE_NONE; - - uint64_t read_val = read_map->get(location); - return read_val; -*/ -} - -/* @param tid thread id - * Reset read map for a thread. This function shall only be called - * when a thread exits a function - */ -void FuncNode::clear_read_map(uint32_t tid) -{ -/* - if (thrd_read_map.size() <= tid) - return; - - thrd_read_map[tid]->reset(); -*/ -} - void FuncNode::update_predicate_tree(action_list_t * act_list) { if (act_list == NULL || act_list->size() == 0) return; - /* map a FuncInst to the its predicate */ + /* Map a FuncInst to the its predicate */ HashTable inst_pred_map(128); - // number FuncInsts to detect loops + // 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); HashTable inst_act_map(128); @@ -280,21 +246,25 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) while (it != NULL) { ModelAction * next_act = it->getVal(); FuncInst * next_inst = get_inst(next_act); - SnapVector * unset_predicates = new SnapVector(); - bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map, unset_predicates); + SnapVector unset_predicates = SnapVector(); + bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map, &unset_predicates); - // no predicate expressions, follow the only branch - if (!branch_found && unset_predicates->size() != 0) { - ASSERT(unset_predicates->size() == 1); - Predicate * one_branch = (*unset_predicates)[0]; - curr_pred = one_branch; - branch_found = true; - } + // 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]; - delete unset_predicates; + bool amended = amend_predicate_expr(&curr_pred, next_inst, next_act); + if (amended) + continue; + else { + curr_pred = one_branch; + branch_found = true; + } + } - // detect loops + // Detect loops if (!branch_found && inst_id_map.contains(next_inst)) { FuncInst * curr_inst = curr_pred->get_func_inst(); uint32_t curr_id = inst_id_map.get(curr_inst); @@ -311,98 +281,30 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) } } - // generate new branches + // Generate new branches if (!branch_found) { SnapVector half_pred_expressions; - void * loc = next_act->get_location(); - - 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); - } else if ( next_inst->is_single_location() ){ - loc_set_t * loc_may_equal = loc_may_equal_map->get(loc); - - if (loc_may_equal != NULL) { - 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); - 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); - } - } - } - } else { - // next_inst is not single location - struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL); - half_pred_expressions.push_back(expression); - } - - if (half_pred_expressions.size() == 0) { - // no predicate needs to be generated - Predicate * new_pred = new Predicate(next_inst); - curr_pred->add_child(new_pred); - new_pred->set_parent(curr_pred); + infer_predicates(next_inst, next_act, &loc_act_map, &half_pred_expressions); + generate_predicates(&curr_pred, next_inst, &half_pred_expressions); + continue; + } - if (curr_pred->is_entry_predicate()) - new_pred->add_predicate_expr(NOPREDICATE, NULL, true); + if (next_act->is_write()) + curr_pred->set_write(true); - curr_pred = new_pred; - } else { - generate_predicate(&curr_pred, next_inst, &half_pred_expressions); - bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map, NULL); - ASSERT(branch_found); - } + if (next_act->is_read()) { + loc_act_map.put(next_act->get_location(), next_act); } + inst_act_map.put(next_inst, next_act); inst_pred_map.put(next_inst, curr_pred); if (!inst_id_map.contains(next_inst)) inst_id_map.put(next_inst, inst_counter++); - loc_act_map.put(next_act->get_location(), next_act); - inst_act_map.put(next_inst, next_act); it = it->getNext(); } } -void FuncNode::deep_update(Predicate * curr_pred) -{ - FuncInst * func_inst = curr_pred->get_func_inst(); - if (func_inst != NULL && !func_inst->is_single_location()) { - bool has_null_pred = false; - PredExprSet * pred_expressions = curr_pred->get_pred_expressions(); - PredExprSetIter * pred_expr_it = pred_expressions->iterator(); - while (pred_expr_it->hasNext()) { - pred_expr * pred_expression = pred_expr_it->next(); - if (pred_expression->token == NULLITY) { - has_null_pred = true; - break; - } - } - - if (!has_null_pred) { -// func_inst->print(); - Predicate * another_branch = new Predicate(func_inst); - another_branch->copy_predicate_expr(curr_pred); - another_branch->add_predicate_expr(NULLITY, NULL, 1); - curr_pred->add_predicate_expr(NULLITY, NULL, 0); - - Predicate * parent = curr_pred->get_parent(); - parent->add_child(another_branch); - } - } - - ModelVector * branches = curr_pred->get_children(); - for (uint i = 0; i < branches->size(); i++) { - Predicate * branch = (*branches)[i]; - deep_update(branch); - } -} - /* Given curr_pred and next_inst, find the branch following curr_pred that * contains next_inst and the correct predicate. * @return true if branch found, false otherwise. @@ -419,43 +321,36 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model if (branch->get_func_inst() != next_inst) continue; - /* check against predicate expressions */ + /* 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); } - while (pred_expr_it->hasNext()) { - pred_expr * pred_expression = pred_expr_it->next(); - uint64_t last_read, next_read; + SnapVector concrete_exprs = branch->evaluate(inst_act_map); + for (uint i = 0; i < concrete_exprs.size(); i++) { + struct concrete_pred_expr concrete = concrete_exprs[i]; + uint64_t next_read; bool equality; - switch(pred_expression->token) { + switch (concrete.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 = inst_act_map->get(to_be_compared); - - 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) + equality = (next_read == concrete.value); + if (equality != concrete.equality) predicate_correct = false; - break; case NULLITY: next_read = next_act->get_reads_from_value(); equality = ((void*)next_read == NULL); - if (equality != pred_expression->value) + if (equality != concrete.equality) predicate_correct = false; break; default: @@ -475,11 +370,73 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model return branch_found; } +/* 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) +{ + 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); + 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); + } else if ( next_inst->is_single_location() ){ + loc_set_t * loc_may_equal = loc_may_equal_map->get(loc); + + if (loc_may_equal != NULL) { + 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); + 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); + } + } + } + } else { + // next_inst is not single location + uint64_t read_val = next_act->get_reads_from_value(); + + // only infer NULLITY predicate when it is actually NULL. + if ( (void*)read_val == NULL) { + struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL); + half_pred_expressions->push_back(expression); + } + } + } else { + /* Pure writes */ + // TODO: do anything here? + } +} + /* Able to generate complex predicates when there are multiple predciate expressions */ -void FuncNode::generate_predicate(Predicate ** curr_pred, FuncInst * next_inst, +void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, SnapVector * half_pred_expressions) { - ASSERT(half_pred_expressions->size() != 0); + 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); + + /* entry predicates and predicates containing pure write actions + * have no predicate expressions */ + 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 */ + new_pred->add_predicate_expr(NOPREDICATE, NULL, true); + } + + return; + } + SnapVector predicates; struct half_pred_expr * half_expr = (*half_pred_expressions)[0]; @@ -510,8 +467,36 @@ void FuncNode::generate_predicate(Predicate ** curr_pred, FuncInst * next_inst, (*curr_pred)->add_child(pred); pred->set_parent(*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]; + snapshot_free(tmp); + } } +/* 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) +{ + // there should only be only child + 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); + + unset_pred->add_predicate_expr(NULLITY, NULL, false); + new_pred->add_predicate_expr(NULLITY, NULL, true); + + return true; + } + + return false; +} void FuncNode::add_to_val_loc_map(uint64_t val, void * loc) { @@ -524,11 +509,14 @@ void FuncNode::add_to_val_loc_map(uint64_t val, void * loc) update_loc_may_equal_map(loc, locations); locations->add(loc); - values_may_read_from->add(val); + // values_may_read_from->add(val); } void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc) { + if (values == NULL) + return; + value_set_iter * it = values->iterator(); while (it->hasNext()) { uint64_t val = it->next(); @@ -538,6 +526,9 @@ void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc) void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations) { + if ( old_locations->contains(new_loc) ) + return; + loc_set_t * neighbors = loc_may_equal_map->get(new_loc); if (neighbors == NULL) { @@ -561,6 +552,82 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location } } +/* Every time a thread enters a function, set its position to the predicate tree entry */ +void FuncNode::init_predicate_tree_position(thread_id_t tid) +{ + int thread_id = id_to_int(tid); + if (predicate_tree_position.size() <= (uint) thread_id) + predicate_tree_position.resize(thread_id + 1); + + predicate_tree_position[thread_id] = predicate_tree_entry; +} + +void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred) +{ + int thread_id = id_to_int(tid); + predicate_tree_position[thread_id] = pred; +} + +/* @return The position of a thread in a predicate tree */ +Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid) +{ + int thread_id = id_to_int(tid); + return predicate_tree_position[thread_id]; +} + +/* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */ +void FuncNode::init_inst_act_map(thread_id_t tid) +{ + int thread_id = id_to_int(tid); + uint old_size = thrd_inst_act_map->size(); + + if (thrd_inst_act_map->size() <= (uint) thread_id) { + uint new_size = thread_id + 1; + thrd_inst_act_map->resize(new_size); + + for (uint i = old_size; i < new_size; i++) + (*thrd_inst_act_map)[i] = new inst_act_map_t(128); + } +} + +/* Reset elements of thrd_inst_act_map when threads exit functions */ +void FuncNode::reset_inst_act_map(thread_id_t tid) +{ + int thread_id = id_to_int(tid); + inst_act_map_t * map = (*thrd_inst_act_map)[thread_id]; + map->reset(); +} + +void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act) +{ + int thread_id = id_to_int(tid); + inst_act_map_t * map = (*thrd_inst_act_map)[thread_id]; + FuncInst * read_inst = get_inst(read_act); + map->put(read_inst, read_act); +} + +inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid) +{ + int thread_id = id_to_int(tid); + return (*thrd_inst_act_map)[thread_id]; +} + +/* Add FuncNodes that this node may follow */ +void FuncNode::add_out_edge(FuncNode * other) +{ + if ( !edge_table.contains(other) ) { + edge_table.put(other, OUT_EDGE); + out_edges.push_back(other); + return; + } + + edge_type_t edge = edge_table.get(other); + if (edge == IN_EDGE) { + edge_table.put(other, BI_EDGE); + out_edges.push_back(other); + } +} + void FuncNode::print_predicate_tree() { model_print("digraph function_%s {\n", func_name); @@ -570,6 +637,7 @@ void FuncNode::print_predicate_tree() 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(); @@ -583,24 +651,5 @@ void FuncNode::print_val_loc_map() } model_print("\n"); } -} - -/* @param tid thread id - * Print the values read by the last read actions for each memory location - */ -/* -void FuncNode::print_last_read(uint32_t tid) -{ - ASSERT(thrd_read_map.size() > tid); - read_map_t * read_map = thrd_read_map[tid]; - - mllnode * it; - for (it = read_locations.begin();it != NULL;it=it->getNext()) { - if ( !read_map->contains(it->getVal()) ) - break; - - uint64_t read_val = read_map->get(it->getVal()); - model_print("last read of thread %d at %p: 0x%x\n", tid, it->getVal(), read_val); - } -} */ +}