model: add promise-node edges for 'read' actions

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 0c2b993868421edf898441896e6fb9f4236c0bea..15f1831627e0621896fadc3638ec27e6814cfc07 100644 (file)
--- 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))