Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 866bc94d6fb288bb759974ef2fc6bce722fbbb89..217d6421ac403e60108ec074c900168bbce67888 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -9,6 +9,7 @@
 #include "clockvector.h"
 #include "cyclegraph.h"
 #include "promise.h"
+#include "datarace.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -36,7 +37,8 @@ ModelChecker::ModelChecker(struct model_params params) :
        node_stack(new NodeStack()),
        next_backtrack(NULL),
        mo_graph(new CycleGraph()),
-       failed_promise(false)
+       failed_promise(false),
+       asserted(false)
 {
 }
 
@@ -77,6 +79,7 @@ void ModelChecker::reset_to_initial_state()
        nextThread = NULL;
        next_backtrack = NULL;
        failed_promise = false;
+       reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -244,6 +247,18 @@ ModelAction * ModelChecker::get_next_backtrack()
        return next;
 }
 
+/**
+ * This is the heart of the model checker routine. It performs model-checking
+ * actions corresponding to a given "current action." Among other processes, it
+ * calculates reads-from relationships, updates synchronization clock vectors,
+ * forms a memory_order constraints graph, and handles replay/backtrack
+ * execution when running permutations of previously-observed executions.
+ *
+ * @param curr The current action to process
+ * @return The next Thread that must be executed. May be NULL if ModelChecker
+ * makes no choice (e.g., according to replay execution, combining RMW actions,
+ * etc.)
+ */
 Thread * ModelChecker::check_current_action(ModelAction *curr)
 {
        bool already_added = false;
@@ -287,6 +302,19 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        if (curr->get_type() == THREAD_CREATE) {
                Thread *th = (Thread *)curr->get_location();
                th->set_creation(curr);
+       } else if (curr->get_type() == THREAD_JOIN) {
+               Thread *wait, *join;
+               wait = get_thread(curr->get_tid());
+               join = (Thread *)curr->get_location();
+               if (!join->is_complete())
+                       scheduler->wait(wait, join);
+       } else if (curr->get_type() == THREAD_FINISH) {
+               Thread *th = get_thread(curr->get_tid());
+               while (!th->wait_list_empty()) {
+                       Thread *wake = th->pop_wait_list();
+                       scheduler->wake(wake);
+               }
+               th->complete();
        }
 
        /* Deal with new thread */
@@ -314,7 +342,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                }
        } else if (curr->is_write()) {
                if (w_modification_order(curr))
-                       updated = true;;
+                       updated = true;
                if (resolve_promises(curr))
                        updated = true;
        }
@@ -345,6 +373,13 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                return get_next_replay_thread();
 }
 
+/** @returns whether the current partial trace must be a prefix of a
+ * feasible trace. */
+
+bool ModelChecker::isfeasibleprefix() {
+       return promises->size()==0;
+}
+
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
        return !mo_graph->checkForCycles() && !failed_promise;
@@ -675,6 +710,11 @@ bool ModelChecker::resolve_release_sequences(void *location)
                        it++;
        }
 
+       // If we resolved promises or data races, see if we have realized a data race.
+       if (checkDataRaces()) {
+               model->set_assert();
+       }
+
        return updated;
 }
 
@@ -766,6 +806,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                } else
                        promise_index++;
        }
+
        return resolved;
 }
 
@@ -929,10 +970,7 @@ void ModelChecker::remove_thread(Thread *t)
  * 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()).
+ * @param act The current action that will be explored. Must not be NULL.
  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
  */
 int ModelChecker::switch_to_master(ModelAction *act)
@@ -951,17 +989,17 @@ int ModelChecker::switch_to_master(ModelAction *act)
 bool ModelChecker::take_step() {
        Thread *curr, *next;
 
+       if (has_asserted())
+               return false;
+
        curr = thread_current();
        if (curr) {
                if (curr->get_state() == THREAD_READY) {
-                       if (current_action) {
-                               nextThread = check_current_action(current_action);
-                               current_action = NULL;
-                       }
-                       scheduler->add_thread(curr);
-               } else if (curr->get_state() == THREAD_RUNNING) {
-                       /* Stopped while running; i.e., completed */
-                       curr->complete();
+                       ASSERT(current_action);
+                       nextThread = check_current_action(current_action);
+                       current_action = NULL;
+                       if (!curr->is_blocked() && !curr->is_complete())
+                               scheduler->add_thread(curr);
                } else {
                        ASSERT(false);
                }