From: weiyu Date: Wed, 14 Aug 2019 23:33:55 +0000 (-0700) Subject: experiment with adding NULLITY predicate X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=6b105d0bea24fa7a534d7f83e4c34dadc9d4b02d;hp=9a2ba97d13c76e9048ba7c499b3cbca0d02a84ca experiment with adding NULLITY predicate --- diff --git a/funcinst.cc b/funcinst.cc index cecaca7b..a3a2874e 100644 --- a/funcinst.cc +++ b/funcinst.cc @@ -1,7 +1,7 @@ #include "funcinst.h" FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) : - collisions() + single_location(true) { ASSERT(act); ASSERT(func_node); @@ -44,6 +44,7 @@ bool FuncInst::add_succ(FuncInst * other) return true; } +/* FuncInst * FuncInst::search_in_collision(ModelAction *act) { action_type type = act->get_type(); @@ -56,6 +57,7 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act) } return NULL; } +*/ bool FuncInst::is_read() const { diff --git a/funcinst.h b/funcinst.h index 654ba653..3b2890f0 100644 --- a/funcinst.h +++ b/funcinst.h @@ -13,7 +13,6 @@ public: FuncInst(ModelAction *act, FuncNode *func_node); ~FuncInst(); - //ModelAction * get_action() const { return action; } const char * get_position() const { return position; } void * get_location() const { return location; } action_type get_type() const { return type; } @@ -23,30 +22,40 @@ public: bool add_pred(FuncInst * other); bool add_succ(FuncInst * other); - FuncInst * search_in_collision(ModelAction *act); + //FuncInst * search_in_collision(ModelAction *act); + //func_inst_list_mt * get_collisions() { return &collisions; } - func_inst_list_mt * get_collisions() { return &collisions; } func_inst_list_mt * get_preds() { return &predecessors; } func_inst_list_mt * get_succs() { return &successors; } bool is_read() const; bool is_write() const; + bool is_single_location() { return single_location; } + void not_single_location() { single_location = false; } void print(); MEMALLOC private: - //ModelAction * const action; const char * position; + + /* Atomic operations with the same source line number may act at different + * memory locations, such as the next field of the head pointer in ms-queue. + * location only stores the memory location when this FuncInst was constructed. + */ void * location; action_type type; memory_order order; FuncNode * func_node; - /* collisions store a list of FuncInsts with the same position + bool single_location; + + /* Currently not in use. May remove this field later + * + * collisions store a list of FuncInsts with the same position * but different action types. For example, CAS is broken down * as three different atomic operations in cmodelint.cc */ - func_inst_list_mt collisions; + // func_inst_list_mt collisions; func_inst_list_mt predecessors; func_inst_list_mt successors; diff --git a/funcnode.cc b/funcnode.cc index 188ed173..5b6fb355 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -29,17 +29,9 @@ void FuncNode::add_inst(ModelAction *act) if ( func_inst_map.contains(position) ) { FuncInst * inst = func_inst_map.get(position); - if (inst->get_type() != act->get_type() ) { - // model_print("action with a different type occurs at line number %s\n", position); - FuncInst * func_inst = inst->search_in_collision(act); - - if (func_inst != NULL) - return; - - func_inst = new FuncInst(act, this); - inst->get_collisions()->push_back(func_inst); - inst_list.push_back(func_inst); // delete? - } + ASSERT(inst->get_type() == act->get_type()); + if (inst->get_location() != act->get_location()) + inst->not_single_location(); return; } @@ -69,8 +61,6 @@ FuncInst * FuncNode::get_inst(ModelAction *act) if (inst == NULL) return NULL; -// ASSERT(inst->get_location() == act->get_location()); - action_type inst_type = inst->get_type(); action_type act_type = act->get_type(); @@ -130,8 +120,12 @@ void FuncNode::update_tree(action_list_t * act_list) read_act_list.push_back(act); } + model_print("function %s\n", func_name); update_inst_tree(&inst_list); update_predicate_tree(&read_act_list); + deep_update(predicate_tree_entry); + + print_predicate_tree(); } /** @@ -271,8 +265,8 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) curr_pred->add_child(new_pred1); curr_pred->add_child(new_pred2); - //new_pred1->add_parent(curr_pred); - //new_pred2->add_parent(curr_pred); + new_pred1->set_parent(curr_pred); + new_pred2->set_parent(curr_pred); ModelAction * last_act = loc_act_map.get(next_act->get_location()); uint64_t last_read = last_act->get_reads_from_value(); @@ -285,7 +279,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) } else { Predicate * new_pred = new Predicate(next_inst); curr_pred->add_child(new_pred); - //new_pred->add_parent(curr_pred); + new_pred->set_parent(curr_pred); curr_pred = new_pred; } @@ -294,9 +288,40 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) loc_act_map.put(next_act->get_location(), 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 * parent = curr_pred->get_parent(); + curr_pred->add_predicate(NULLITY, NULL, 0); + + Predicate * another_branch = new Predicate(func_inst); + another_branch->add_predicate(NULLITY, NULL, 1); + parent->add_child(another_branch); +// another_branch.add_children(i); + } + } -// model_print("function %s\n", func_name); -// print_predicate_tree(); + 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 @@ -317,7 +342,6 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model /* no predicate, follow the only branch */ if (pred_expressions->getSize() == 0) { -// model_print("no predicate exists: "); next_inst->print(); *curr_pred = branch; branch_found = true; break; @@ -337,7 +361,6 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model next_read = next_act->get_reads_from_value(); equality = (last_read == next_read); - if (equality == pred_expression->value) { *curr_pred = branch; // model_print("predicate: token: %d, location: %p, value: %d - ", pred_expression->token, pred_expression->location, pred_expression->value); next_inst->print(); @@ -345,6 +368,13 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model } break; case NULLITY: + next_read = next_act->get_reads_from_value(); + equality = ((void*)next_read == NULL); + //model_print("%s ", next_act->get_position()); next_act->print(); + if (equality == pred_expression->value) { + *curr_pred = branch; + branch_found = true; + } break; default: model_print("unkown predicate token\n"); diff --git a/funcnode.h b/funcnode.h index 4ba23985..730a7b7c 100644 --- a/funcnode.h +++ b/funcnode.h @@ -37,6 +37,7 @@ public: /* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */ 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* loc_act_map); void print_predicate_tree(); diff --git a/predicate.cc b/predicate.cc index 77f362da..128ac3dc 100644 --- a/predicate.cc +++ b/predicate.cc @@ -5,7 +5,7 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry) : entry_predicate(is_entry), pred_expressions(), children(), - parents(), + parent(NULL), backedge(NULL) {} @@ -37,12 +37,6 @@ void Predicate::add_child(Predicate * child) children.push_back(child); } -void Predicate::add_parent(Predicate * parent) -{ - /* check duplication? */ - parents.push_back(parent); -} - void Predicate::print_predicate() { model_print("\"%p\" [shape=box, label=\"\n", this); diff --git a/predicate.h b/predicate.h index 2f15a126..dbb959ea 100644 --- a/predicate.h +++ b/predicate.h @@ -41,11 +41,11 @@ public: PredExprSet * get_pred_expressions() { return &pred_expressions; } void add_predicate(token_t token, void * location, bool value); void add_child(Predicate * child); - void add_parent(Predicate * parent); + void set_parent(Predicate * parent_pred) { parent = parent_pred; } void set_backedge(Predicate * back_pred) { backedge = back_pred; } ModelVector * get_children() { return &children; } - ModelVector * get_parents() { return &parents; } + Predicate * get_parent() { return parent; } Predicate * get_backedge() { return backedge; } bool is_entry_predicate() { return entry_predicate; } @@ -62,7 +62,9 @@ private: /* may have multiple predicates */ PredExprSet pred_expressions; ModelVector children; - ModelVector parents; + + /* only a single parent may exist */ + Predicate * parent; /* assume almost one back edge exists */ Predicate * backedge;