From 4da00745531b0845c16ad5a798f777a962f693be Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 12 Jun 2019 19:40:25 -0700 Subject: [PATCH] new cyclegraph --- cyclegraph.cc | 43 ++++++++++++++++---------- cyclegraph.h | 3 +- execution.cc | 83 +++++++++++++++++++++++---------------------------- execution.h | 6 ++-- 4 files changed, 70 insertions(+), 65 deletions(-) diff --git a/cyclegraph.cc b/cyclegraph.cc index a3e86cf0..5d894f84 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -59,32 +59,32 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) * @param tonode The edge points to this CycleNode * @return True, if new edge(s) are added; otherwise false */ -void CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode) +void CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode, bool forceedge) { //quick check whether edge is redundant - if (checkReachable(fromnode, tonode)) + if (checkReachable(fromnode, tonode) && !forceedge) { return; - - CycleNode *edgeSrcNode = fromnode; + } /* * If the fromnode has a rmwnode, we should * follow its RMW chain to add an edge at the end. */ - CycleNode *rmwnode = fromnode->getRMW(); - if (rmwnode) { - while (rmwnode->getRMW()) - rmwnode = rmwnode->getRMW(); - edgeSrcNode = rmwnode; + while (fromnode->getRMW()) { + CycleNode *nextnode = fromnode->getRMW(); + if (nextnode == tonode) + break; + fromnode = nextnode; } - edgeSrcNode->addEdge(tonode); //Add edge to edgeSrcNode + fromnode->addEdge(tonode); //Add edge to edgeSrcNode /* Propagate clock vector changes */ - if (tonode->cv->merge(edgeSrcNode->cv)) { - queue->push_back(edgeSrcNode); + if (tonode->cv->merge(fromnode->cv)) { + queue->push_back(fromnode); while(!queue->empty()) { const CycleNode *node = queue->back(); + queue->pop_back(); unsigned int numedges = node->getNumEdges(); for(unsigned int i = 0;i < numedges;i++) { CycleNode * enode = node->getEdge(i); @@ -114,7 +114,6 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) CycleNode *fromnode = getNode(from); CycleNode *rmwnode = getNode(rmw); - /* We assume that this RMW has no RMW reading from it yet */ ASSERT(!rmwnode->getRMW()); @@ -133,8 +132,9 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) rmwnode->addEdge(tonode); } } - - addNodeEdge(fromnode, rmwnode); + fromnode->edges.clear(); + + addNodeEdge(fromnode, rmwnode, true); } /** @@ -159,7 +159,18 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) CycleNode *fromnode = getNode(from); CycleNode *tonode = getNode(to); - addNodeEdge(fromnode, tonode); + addNodeEdge(fromnode, tonode, false); +} + +void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to, bool forceedge) +{ + ASSERT(from); + ASSERT(to); + + CycleNode *fromnode = getNode(from); + CycleNode *tonode = getNode(to); + + addNodeEdge(fromnode, tonode, forceedge); } #if SUPPORT_MOD_ORDER_DUMP diff --git a/cyclegraph.h b/cyclegraph.h index 624ce885..e2b58640 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -24,6 +24,7 @@ public: CycleGraph(); ~CycleGraph(); void addEdge(const ModelAction *from, const ModelAction *to); + void addEdge(const ModelAction *from, const ModelAction *to, bool forceedge); void addRMWEdge(const ModelAction *from, const ModelAction *rmw); bool checkReachable(const ModelAction *from, const ModelAction *to) const; @@ -37,7 +38,7 @@ public: CycleNode * getNode_noCreate(const ModelAction *act) const; SNAPSHOTALLOC private: - void addNodeEdge(CycleNode *fromnode, CycleNode *tonode); + void addNodeEdge(CycleNode *fromnode, CycleNode *tonode, bool forceedge); void putNode(const ModelAction *act, CycleNode *node); CycleNode * getNode(const ModelAction *act); diff --git a/execution.cc b/execution.cc index c286b2d7..213b2606 100644 --- a/execution.cc +++ b/execution.cc @@ -272,8 +272,9 @@ bool ModelExecution::is_complete_execution() const * @param rf_set is the set of model actions we can possibly read from * @return True if processing this read updates the mo_graph. */ -bool ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) +void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { + SnapVector * priorset = new SnapVector(); while(true) { int index = fuzzer->selectWrite(curr, rf_set); @@ -282,15 +283,16 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * ASSERT(rf); - mo_graph->startChanges(); - r_modification_order(curr, rf); - if (!is_infeasible()) { + if (r_modification_order(curr, rf, priorset)) { + for(unsigned int i=0;isize();i++) { + mo_graph->addEdge((*priorset)[i], rf); + } read_from(curr, rf); - mo_graph->commitChanges(); get_thread(curr)->set_return_value(curr->get_return_value()); - return updated; + delete priorset; + return; } - mo_graph->rollbackChanges(); + priorset->clear(); (*rf_set)[index] = rf_set->back(); rf_set->pop_back(); } @@ -388,15 +390,13 @@ bool ModelExecution::process_mutex(ModelAction *curr) * @param curr The ModelAction to process * @return True if the mo_graph was updated or promises were resolved */ -bool ModelExecution::process_write(ModelAction *curr) +void ModelExecution::process_write(ModelAction *curr) { - bool updated_mod_order = w_modification_order(curr); + w_modification_order(curr); - mo_graph->commitChanges(); get_thread(curr)->set_return_value(VALUE_NONE); - return updated_mod_order; } /** @@ -730,8 +730,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const { char buf[100]; char *ptr = buf; - if (mo_graph->checkForCycles()) - ptr += sprintf(ptr, "[mo cycle]"); if (priv->bad_synchronization) ptr += sprintf(ptr, "[bad sw ordering]"); if (ptr != buf) @@ -746,8 +744,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const */ bool ModelExecution::is_infeasible() const { - return mo_graph->checkForCycles() || - priv->bad_synchronization; + return priv->bad_synchronization; } /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ @@ -756,7 +753,6 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { lastread->process_rmw(act); if (act->is_rmw()) { mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); - mo_graph->commitChanges(); } return lastread; } @@ -778,7 +774,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { * @return True if modification order edges were added; false otherwise */ -bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector * priorset) +bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector * priorset) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -823,26 +819,26 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * /* C++, Section 29.3 statement 5 */ if (curr->is_seqcst() && last_sc_fence_thread_local && *act < *last_sc_fence_thread_local) { - if (mo_graph->checkReachable(rf, act)) - return false; - priorset->add(act); + if (mo_graph->checkReachable(rf, act)) + return false; + priorset->push_back(act); break; } /* C++, Section 29.3 statement 4 */ else if (act->is_seqcst() && last_sc_fence_local && *act < *last_sc_fence_local) { - if (mo_graph->checkReachable(rf, act)) - return false; - priorset->add(act); - break; + if (mo_graph->checkReachable(rf, act)) + return false; + priorset->push_back(act); + break; } /* C++, Section 29.3 statement 6 */ else if (last_sc_fence_thread_before && *act < *last_sc_fence_thread_before) { - if (mo_graph->checkReachable(rf, act)) - return false; - priorset->add(act); - break; + if (mo_graph->checkReachable(rf, act)) + return false; + priorset->push_back(act); + break; } } @@ -852,15 +848,15 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * */ if (act->happens_before(curr)) { if (act->is_write()) { - if (mo_graph->checkReachable(rf, act)) - return false; - priorset->add(act); + if (mo_graph->checkReachable(rf, act)) + return false; + priorset->push_back(act); } else { const ModelAction *prevrf = act->get_reads_from(); if (!prevrf->equals(rf)) { - if (mo_graph->checkReachable(rf, prevrf)) - return false; - priorset->add(prevrf); + if (mo_graph->checkReachable(rf, prevrf)) + return false; + priorset->push_back(prevrf); } } break; @@ -922,6 +918,7 @@ void ModelExecution::w_modification_order(ModelAction *curr) /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; + bool force_edge = false; for (rit = list->rbegin();rit != list->rend();rit++) { ModelAction *act = *rit; if (act == curr) { @@ -936,6 +933,7 @@ void ModelExecution::w_modification_order(ModelAction *curr) * 3) If normal write, we need to look at earlier actions, so * continue processing list. */ + force_edge = true; if (curr->is_rmw()) { if (curr->get_reads_from() != NULL) break; @@ -948,7 +946,7 @@ void ModelExecution::w_modification_order(ModelAction *curr) /* C++, Section 29.3 statement 7 */ if (last_sc_fence_thread_before && act->is_write() && *act < *last_sc_fence_thread_before) { - mo_graph->addEdge(act, curr); + mo_graph->addEdge(act, curr, force_edge); break; } @@ -964,10 +962,10 @@ void ModelExecution::w_modification_order(ModelAction *curr) * readfrom(act) --mo--> act */ if (act->is_write()) - mo_graph->addEdge(act, curr); + mo_graph->addEdge(act, curr, force_edge); else if (act->is_read()) { //if previous read accessed a null, just keep going - mo_graph->addEdge(act->get_reads_from(), curr); + mo_graph->addEdge(act->get_reads_from(), curr, force_edge); } break; } else if (act->is_read() && !act->could_synchronize_with(curr) && @@ -1047,12 +1045,8 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction * * @return true, if the ModelExecution is certain that release_heads is complete; * false otherwise */ -bool ModelExecution::release_seq_heads(const ModelAction *rf, - rel_heads_list_t *release_heads) const +bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const { - /* Only check for release sequences if there are no cycles */ - if (mo_graph->checkForCycles()) - return false; for ( ;rf != NULL;rf = rf->get_reads_from()) { ASSERT(rf->is_write()); @@ -1331,7 +1325,6 @@ SnapVector * ModelExecution::build_may_read_from(ModelAction *cu last_sc_write = get_last_seq_cst_write(curr); SnapVector * rf_set = new SnapVector(); - SnapVector * priorset = new SnapVector(); /* Iterate over all threads */ for (i = 0;i < thrd_lists->size();i++) { @@ -1366,8 +1359,8 @@ SnapVector * ModelExecution::build_may_read_from(ModelAction *cu } if (allow_read) { - /* Only add feasible reads */ - rf_set->push_back(act); + /* Only add feasible reads */ + rf_set->push_back(act); } /* Include at most one act per-thread that "happens before" curr */ diff --git a/execution.h b/execution.h index 40cd3ac0..b78837fc 100644 --- a/execution.h +++ b/execution.h @@ -127,8 +127,8 @@ private: bool next_execution(); ModelAction * check_current_action(ModelAction *curr); bool initialize_curr_action(ModelAction **curr); - bool process_read(ModelAction *curr, SnapVector * rf_set); - bool process_write(ModelAction *curr); + void process_read(ModelAction *curr, SnapVector * rf_set); + void process_write(ModelAction *curr); bool process_fence(ModelAction *curr); bool process_mutex(ModelAction *curr); @@ -144,7 +144,7 @@ private: SnapVector * build_may_read_from(ModelAction *curr); ModelAction * process_rmw(ModelAction *curr); - bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector *priorset); + bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector *priorset); void w_modification_order(ModelAction *curr); void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads); bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const; -- 2.34.1