Make stack popping explicit.

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 4cfc0efddd0a491911404454347c0d136960aad5..a22e17e1f46fd20c780136f6f232399170111356 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -132,6 +132,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
                DEBUG("*** Divergence point ***\n");
                tid = node->get_next_backtrack();
                diverge = NULL;
+               node_stack->pop_restofstack();
        } else {
                tid = next->get_tid();
        }
@@ -278,7 +279,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();
@@ -365,13 +366,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        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;
 
+       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++) {
@@ -403,7 +411,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();
@@ -411,7 +419,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);
 }
 
@@ -452,6 +460,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;