From 284151d644be0946f887561a03344866f0665c03 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sat, 2 Mar 2013 00:04:44 -0800 Subject: [PATCH] check_recency: only allow newer stores to "overwrite" For a "live" memory system, we only want to force a store to appear if it is modification-ordered after the store we're reading from. Also, delete my old comment about reads-from feasibility. --- model.cc | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/model.cc b/model.cc index fba9cf0..36c23bf 100644 --- a/model.cc +++ b/model.cc @@ -1694,11 +1694,9 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) if (write == rf) continue; - //NOTE: SHOULD MAKE SURE write is MOd after rf - - /* Test to see whether this is a feasible write to read from */ - /** NOTE: all members of read-from set should be - * feasible, so we no longer check it here **/ + /* Only look for "newer" writes */ + if (!mo_graph->checkReachable(rf, write)) + continue; ritcopy = rit; -- 2.34.1