From b588ae090b73e131a824d5328e5e8a6ead760148 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 1 Feb 2013 16:44:22 -0800 Subject: [PATCH] model: template-ize 'r_modification_order' We will need to add "read modification order" edges when 'rf' is either a ModelAction or a Promise. This function works nicely with a template. --- action.h | 2 ++ model.cc | 13 +++++++------ model.h | 5 ++++- 3 files changed, 13 insertions(+), 7 deletions(-) diff --git a/action.h b/action.h index 2647b97..c39af5e 100644 --- a/action.h +++ b/action.h @@ -151,6 +151,8 @@ public: bool get_sleep_flag() { return sleep_flag; } unsigned int hash() const; + bool equals(const ModelAction *x) const { return this == x; } + bool equals(const Promise *x) const { return false; } MEMALLOC private: diff --git a/model.cc b/model.cc index cb78f03..0c2b993 100644 --- a/model.cc +++ b/model.cc @@ -1521,7 +1521,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) * read. * * Basic idea is the following: Go through each other thread and find - * the lastest action that happened before our read. Two cases: + * the last action that happened before our read. Two cases: * * (1) The action is a write => that write must either occur before * the write we read from or be the write we read from. @@ -1530,10 +1530,11 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) * must occur before the write we read from or be the same write. * * @param curr The current action. Must be a read. - * @param rf The action that curr reads from. Must be a write. + * @param rf The ModelAction or Promise that curr reads from. Must be a write. * @return True if modification order edges were added; false otherwise */ -bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf) +template +bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) { std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; @@ -1561,7 +1562,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - if (act->is_write() && act != rf && act != curr) { + if (act->is_write() && !act->equals(rf) && act != curr) { /* C++, Section 29.3 statement 5 */ if (curr->is_seqcst() && last_sc_fence_thread_local && *act < *last_sc_fence_thread_local) { @@ -1591,7 +1592,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf */ if (act->happens_before(curr) && act != curr) { if (act->is_write()) { - if (rf != act) { + if (!act->equals(rf)) { mo_graph->addEdge(act, rf); added = true; } @@ -1601,7 +1602,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf if (prevreadfrom == NULL) continue; - if (rf != prevreadfrom) { + if (!prevreadfrom->equals(rf)) { mo_graph->addEdge(prevreadfrom, rf); added = true; } diff --git a/model.h b/model.h index c76a289..6685ab3 100644 --- a/model.h +++ b/model.h @@ -183,7 +183,10 @@ private: void build_reads_from_past(ModelAction *curr); ModelAction * process_rmw(ModelAction *curr); void post_r_modification_order(ModelAction *curr, const ModelAction *rf); - bool r_modification_order(ModelAction *curr, const ModelAction *rf); + + template + bool r_modification_order(ModelAction *curr, const rf_type *rf); + bool 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, struct release_seq *pending) const; -- 2.34.1