From: Brian Norris Date: Tue, 18 Sep 2012 20:26:55 +0000 (-0700) Subject: Merge branch 'norris' X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=3262ae1f816dea735cab52d6940523f52ca80fe1;hp=-c Merge branch 'norris' Primary change: push 'add_action_to_lists()' before main work in 'check_current_action()' --- 3262ae1f816dea735cab52d6940523f52ca80fe1 diff --combined model.cc index 38c5d4a,483e832..9faf4e2 --- a/model.cc +++ b/model.cc @@@ -281,7 -281,7 +281,7 @@@ bool ModelChecker::process_read(ModelAc bool r_status = false; if (!second_part_of_rmw) { - check_recency(curr,false); + check_recency(curr); r_status = r_modification_order(curr, reads_from); } @@@ -420,6 -420,10 +420,10 @@@ Thread * ModelChecker::check_current_ac break; } + /* Add current action to lists before work_queue loop */ + if (!second_part_of_rmw) + add_action_to_lists(curr); + work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); while (!work_queue.empty()) { @@@ -451,10 -455,6 +455,6 @@@ } } - /* Add action to list. */ - if (!second_part_of_rmw) - add_action_to_lists(curr); - check_curr_backtracking(curr); set_backtracking(curr); @@@ -500,24 -500,11 +500,24 @@@ bool ModelChecker::isfeasible() /** @returns whether the current partial trace is feasible other than * multiple RMW reading from the same store. */ bool ModelChecker::isfeasibleotherthanRMW() { + if (DBG_ENABLED()) { + if (mo_graph->checkForCycles()) + DEBUG("Infeasible: modification order cycles\n"); + if (failed_promise) + DEBUG("Infeasible: failed promise\n"); + if (too_many_reads) + DEBUG("Infeasible: too many reads\n"); + if (promises_expired()) + DEBUG("Infeasible: promises expired\n"); + } return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired(); } /** Returns whether the current completed trace is feasible. */ bool ModelChecker::isfinalfeasible() { + if (DBG_ENABLED() && promises->size() != 0) + DEBUG("Infeasible: unrevolved promises\n"); + return isfeasible() && promises->size() == 0; } @@@ -544,7 -531,7 +544,7 @@@ ModelAction * ModelChecker::process_rmw * * If so, we decide that the execution is no longer feasible. */ - void ModelChecker::check_recency(ModelAction *curr, bool already_added) { + void ModelChecker::check_recency(ModelAction *curr) { if (params.maxreads != 0) { if (curr->get_node()->get_read_from_size() <= 1) return; @@@ -565,12 -552,10 +565,10 @@@ action_list_t::reverse_iterator rit = list->rbegin(); /* Skip past curr */ - if (already_added) { - for (; (*rit) != curr; rit++) - ; - /* go past curr now */ - rit++; - } + for (; (*rit) != curr; rit++) + ; + /* go past curr now */ + rit++; action_list_t::reverse_iterator ritcopy = rit; //See if we have enough reads from the same value @@@ -661,10 -646,13 +659,13 @@@ bool ModelChecker::r_modification_order for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - /* Include at most one act per-thread that "happens before" curr */ - if (act->happens_before(curr)) { + /* + * Include at most one act per-thread that "happens + * before" curr. Don't consider reflexively. + */ + if (act->happens_before(curr) && act != curr) { if (act->is_write()) { - if (rf != act && act != curr) { + if (rf != act) { mo_graph->addEdge(act, rf); added = true; } @@@ -675,7 -663,6 +676,6 @@@ added = true; } } - break; } } @@@ -768,7 -755,7 +768,7 @@@ bool ModelChecker::w_modification_order if (curr->is_seqcst()) { /* We have to at least see the last sequentially consistent write, so we are initialized. */ - ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location()); + ModelAction *last_seq_cst = get_last_seq_cst(curr); if (last_seq_cst != NULL) { mo_graph->addEdge(last_seq_cst, curr); added = true; @@@ -782,8 -769,23 +782,23 @@@ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; + if (act == curr) { + /* + * If RMW, we already have all relevant edges, + * so just skip to next thread. + * If normal write, we need to look at earlier + * actions, so continue processing list. + */ + if (curr->is_rmw()) + break; + else + continue; + } - /* Include at most one act per-thread that "happens before" curr */ + /* + * Include at most one act per-thread that "happens + * before" curr + */ if (act->happens_before(curr)) { /* * Note: if act is RMW, just add edge: @@@ -791,11 -793,9 +806,9 @@@ * The following edge should be handled elsewhere: * readfrom(act) --mo--> act */ - if (act->is_write()) { - //RMW shouldn't have an edge to themselves - if (act!=curr) - mo_graph->addEdge(act, curr); - } else if (act->is_read() && act->get_reads_from() != NULL) + if (act->is_write()) + mo_graph->addEdge(act, curr); + else if (act->is_read() && act->get_reads_from() != NULL) mo_graph->addEdge(act->get_reads_from(), curr); added = true; break; @@@ -1085,18 -1085,21 +1098,21 @@@ ModelAction * ModelChecker::get_last_ac } /** - * Gets the last memory_order_seq_cst action (in the total global sequence) - * performed on a particular object (i.e., memory location). - * @param location The object location to check - * @return The last seq_cst action performed + * Gets the last memory_order_seq_cst write (in the total global sequence) + * performed on a particular object (i.e., memory location), not including the + * current action. + * @param curr The current ModelAction; also denotes the object location to + * check + * @return The last seq_cst write */ - ModelAction * ModelChecker::get_last_seq_cst(const void *location) + ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) { + void *location = curr->get_location(); action_list_t *list = obj_map->get_safe_ptr(location); /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) - if ((*rit)->is_write() && (*rit)->is_seqcst()) + if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr) return *rit; return NULL; } @@@ -1210,7 -1213,7 +1226,7 @@@ void ModelChecker::build_reads_from_pas bool initialized = false; if (curr->is_seqcst()) { - last_seq_cst = get_last_seq_cst(curr->get_location()); + last_seq_cst = get_last_seq_cst(curr); /* We have to at least see the last sequentially consistent write, so we are initialized. */ if (last_seq_cst != NULL)