model: add promise-node edges for 'read' actions
authorBrian Norris <banorris@uci.edu>
Sat, 2 Feb 2013 01:51:56 +0000 (17:51 -0800)
committerBrian Norris <banorris@uci.edu>
Wed, 6 Feb 2013 21:44:39 +0000 (13:44 -0800)
model.cc

index 0c2b993..15f1831 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))