nodestack: improve bounds-checking assertion

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index e5926730b87c512b388e058a23f08e031a5df33a..52eab24c6790fdc472bdfc30937fa356aa319fed 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -441,7 +441,7 @@ ModelAction * ModelChecker::get_next_backtrack()
  */
 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 {
-       uint64_t value;
+       uint64_t value = VALUE_NONE;
        bool updated = false;
        while (true) {
                const ModelAction *reads_from = curr->get_node()->get_read_from();
@@ -1366,32 +1366,40 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
        return true;
 }
 
-/** Arbitrary reads from the future are not allowed.  Section 29.3
- * part 9 places some constraints.  This method checks one result of constraint
- * constraint.  Others require compiler support. */
-bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
+/**
+ * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
+ * some constraints. This method checks one the following constraint (others
+ * require compiler support):
+ *
+ *   If X --hb-> Y --mo-> Z, then X should not read from Z.
+ */
+bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
+{
        std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+       unsigned int i;
 
-       //Get write that follows reader action
-       action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
-       action_list_t::reverse_iterator rit;
-       ModelAction *first_write_after_read=NULL;
-
-       for (rit = list->rbegin(); rit != list->rend(); rit++) {
-               ModelAction *act = *rit;
-               if (act==reader)
-                       break;
-               if (act->is_write())
-                       first_write_after_read=act;
-       }
+       /* Iterate over all threads */
+       for (i = 0; i < thrd_lists->size(); i++) {
+               ModelAction *write_after_read = NULL;
 
-       if (first_write_after_read==NULL)
-               return true;
+               /* Iterate over actions in thread, starting from most recent */
+               action_list_t *list = &(*thrd_lists)[i];
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *act = *rit;
 
-       return !mo_graph->checkReachable(first_write_after_read, writer);
-}
+                       if (!reader->happens_before(act))
+                               break;
+                       else if (act->is_write())
+                               write_after_read = act;
+               }
 
+               if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+                       return false;
+       }
 
+       return true;
+}
 
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
@@ -1994,6 +2002,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        if (!initialized) {
                /** @todo Need a more informative way of reporting errors. */
                printf("ERROR: may read from uninitialized atomic\n");
+               set_assert();
        }
 
        if (DBG_ENABLED() || !initialized) {
@@ -2003,8 +2012,6 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                curr->get_node()->print_may_read_from();
                printf("End printing may_read_from\n");
        }
-
-       ASSERT(initialized);
 }
 
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {