model: remove unused #include

[cdsspec-compiler.git] / model.cc

diff --git a/model.cc b/model.cc
index 8e6e1b86035e4d27243508a386edbdfe4f648f8f..614b1a78559779dcdd1ba1ec382557fdb68e43aa 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -363,10 +363,21 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        ASSERT(curr->is_read());
 
+       ModelAction *last_seq_cst = NULL;
+
+       if (curr->is_seqcst())
+               last_seq_cst = get_last_seq_cst(curr->get_location());
+
        /* Track whether this object has been initialized */
        bool initialized = false;
+       /* Would each action synchronize if we read from it? */
+       bool all_synch = true;
+       /* Is the may_read_from set empty? (tracked locally) */
+       bool empty = 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 +387,20 @@ 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);
+                               empty = false;
+
+                               if (!(act->is_release() && curr->is_acquire())
+                                               && !act->same_thread(curr))
+                                       all_synch = false;
                        }
-                       curr->get_node()->add_read_from(act);
 
                        /* Include at most one act per-thread that "happens before" curr */
                        if (act->happens_before(curr)) {
@@ -391,6 +410,9 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                }
        }
 
+       if (!empty && all_synch)
+               initialized = true;
+
        if (!initialized) {
                /* TODO: need a more informative way of reporting errors */
                printf("ERROR: may read from uninitialized atomic\n");
@@ -444,6 +466,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;