From b3ff4f8b32505a6e44b70ddc754af6ecb2321474 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 1 Feb 2013 17:51:56 -0800 Subject: [PATCH] model: add promise-node edges for 'read' actions --- model.cc | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/model.cc b/model.cc index 0c2b993..15f1831 100644 --- a/model.cc +++ b/model.cc @@ -739,6 +739,9 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) value = fv.value; curr->set_read_from_promise(promise); promises->push_back(promise); + mo_graph->startChanges(); + updated = r_modification_order(curr, promise); + mo_graph->commitChanges(); } get_thread(curr)->set_return_value(value); return updated; @@ -1304,8 +1307,14 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr) if (act->is_read()) { const ModelAction *rf = act->get_reads_from(); - if (rf != NULL && r_modification_order(act, rf)) - updated = true; + const Promise *promise = act->get_reads_from_promise(); + if (rf) { + if (r_modification_order(act, rf)) + updated = true; + } else if (promise) { + if (r_modification_order(act, promise)) + updated = true; + } } if (act->is_write()) { if (w_modification_order(act)) -- 2.34.1