model: add some mo_graph fixup code to work_queue
authorBrian Norris <banorris@uci.edu>
Fri, 14 Sep 2012 20:11:08 +0000 (13:11 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 18 Sep 2012 20:27:09 +0000 (13:27 -0700)
The work queue has all its work items implemented now. But I haven't fully
verified that this is complete yet.

model.cc

index 9faf4e2..7f1e49d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -447,8 +447,24 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                case WORK_CHECK_RELEASE_SEQ:
                        resolve_release_sequences(work.location, &work_queue);
                        break;
-               case WORK_CHECK_MO_EDGES:
-                       /** @todo Perform follow-up mo_graph checks */
+               case WORK_CHECK_MO_EDGES: {
+                       /** @todo Complete verification of work_queue */
+                       ModelAction *act = work.action;
+                       bool updated = false;
+
+                       if (act->is_read()) {
+                               if (r_modification_order(act, act->get_reads_from()))
+                                       updated = true;
+                       }
+                       if (act->is_write()) {
+                               if (w_modification_order(act))
+                                       updated = true;
+                       }
+
+                       if (updated)
+                               work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
+                       break;
+               }
                default:
                        ASSERT(false);
                        break;