From 34aa82864b18e6f11d806ef77e4b992c2e19f370 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 12 Mar 2013 10:47:41 -0700 Subject: [PATCH] model: bugfix - missing SC mo_graph edge We must enforce a rule such as the following, derived from C++ Section 29.3, statement 3 (second subpoint): if is_store(X) && is_seq_cst(X) && is_store(Y) && is_load(Z) && is_seq_cst(Z) && X --sc-> Z && Y --rf-> Z && X != Y then X --mo-> Y This has been checked (via manual test-case) to fix a bug which allowed an inconsistent mo/sc/rf relationship. --- model.cc | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/model.cc b/model.cc index a03ea46..d9ff365 100644 --- a/model.cc +++ b/model.cc @@ -1812,6 +1812,9 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) /* Last SC fence in the current thread */ ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); + ModelAction *last_sc_write = NULL; + if (curr->is_seqcst()) + last_sc_write = get_last_seq_cst_write(curr); /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -1863,6 +1866,12 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) } } + /* C++, Section 29.3 statement 3 (second subpoint) */ + if (curr->is_seqcst() && last_sc_write && act == last_sc_write) { + added = mo_graph->addEdge(act, rf) || added; + break; + } + /* * Include at most one act per-thread that "happens * before" curr @@ -2463,8 +2472,11 @@ ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const action_list_t *list = get_safe_ptr_action(obj_map, 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() && (*rit) != curr) + for (rit = list->rbegin(); (*rit) != curr; rit++) + ; + rit++; /* Skip past curr */ + for ( ; rit != list->rend(); rit++) + if ((*rit)->is_write() && (*rit)->is_seqcst()) return *rit; return NULL; } -- 2.34.1