really should be using a type that is big enough for all commonly used data types...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 8e6e1b86035e4d27243508a386edbdfe4f648f8f..0c5733b543cf84899a582cdabfd6eecb1fba8b90 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -278,7 +278,7 @@ void ModelChecker::check_current_action(void)
        /* TODO: perform release/acquire synchronization here; include
         * reads_from as ModelAction member? */
        Thread *th = get_thread(curr->get_tid());
-       int value = VALUE_NONE;
+       uint64_t value = VALUE_NONE;
        if (curr->is_read()) {
                const ModelAction *reads_from = curr->get_node()->get_next_read_from();
                value = reads_from->get_value();
@@ -363,10 +363,22 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        ASSERT(curr->is_read());
 
+       ModelAction *last_seq_cst = NULL;
+
        /* Track whether this object has been initialized */
        bool initialized = false;
 
+       if (curr->is_seqcst()) {
+               last_seq_cst = get_last_seq_cst(curr->get_location());
+               /* We have to at least see the last sequentially consistent write,
+                        so we are initialized. */
+               if (last_seq_cst != NULL)
+                       initialized = true;
+       }
+
+       /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
+               /* 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++) {
@@ -376,12 +388,15 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                        if (!act->is_write())
                                continue;
 
-                       DEBUG("Adding action to may_read_from:\n");
-                       if (DBG_ENABLED()) {
-                               act->print();
-                               curr->print();
+                       /* Don't consider more than one seq_cst write */
+                       if (!act->is_seqcst() || act == last_seq_cst) {
+                               DEBUG("Adding action to may_read_from:\n");
+                               if (DBG_ENABLED()) {
+                                       act->print();
+                                       curr->print();
+                               }
+                               curr->get_node()->add_read_from(act);
                        }
-                       curr->get_node()->add_read_from(act);
 
                        /* Include at most one act per-thread that "happens before" curr */
                        if (act->happens_before(curr)) {
@@ -395,7 +410,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                /* TODO: need a more informative way of reporting errors */
                printf("ERROR: may read from uninitialized atomic\n");
        }
-
+       
        if (DBG_ENABLED() || !initialized) {
                printf("Reached read action:\n");
                curr->print();
@@ -403,7 +418,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                curr->get_node()->print_may_read_from();
                printf("End printing may_read_from\n");
        }
-
+       
        ASSERT(initialized);
 }
 
@@ -444,6 +459,17 @@ void ModelChecker::remove_thread(Thread *t)
        scheduler->remove_thread(t);
 }
 
+/**
+ * Switch from a user-context to the "master thread" context (a.k.a. system
+ * context). This switch is made with the intention of exploring a particular
+ * model-checking action (described by a ModelAction object). Must be called
+ * from a user-thread context.
+ * @param act The current action that will be explored. May be NULL, although
+ * there is little reason to switch to the model-checker without an action to
+ * explore (note: act == NULL is sometimes used as a hack to allow a thread to
+ * yield control without performing any progress; see thrd_join()).
+ * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
+ */
 int ModelChecker::switch_to_master(ModelAction *act)
 {
        Thread *old;