model: force THREAD_START to immediately follow THREAD_CREATE

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 0bb96175eff46b3cfc00b8d926b13055ff8e9c9a..811cf8251ed4252179fefbceb8f4c5a9c5e2b8dd 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1,4 +1,5 @@
 #include <stdio.h>
+#include <algorithm>
 
 #include "model.h"
 #include "action.h"
@@ -9,6 +10,7 @@
 #include "clockvector.h"
 #include "cyclegraph.h"
 #include "promise.h"
+#include "datarace.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -36,7 +38,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 +80,7 @@ void ModelChecker::reset_to_initial_state()
        nextThread = NULL;
        next_backtrack = NULL;
        failed_promise = false;
+       reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -163,7 +167,7 @@ bool ModelChecker::next_execution()
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
 
-       if ((diverge = model->get_next_backtrack()) == NULL)
+       if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
        if (DBG_ENABLED()) {
@@ -171,7 +175,7 @@ bool ModelChecker::next_execution()
                diverge->print();
        }
 
-       model->reset_to_initial_state();
+       reset_to_initial_state();
        return true;
 }
 
@@ -311,6 +315,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        Thread *wake = th->pop_wait_list();
                        scheduler->wake(wake);
                }
+               th->complete();
        }
 
        /* Deal with new thread */
@@ -338,7 +343,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;
        }
@@ -365,10 +370,20 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        /* Do not split atomic actions. */
        if (curr->is_rmwr())
                return thread_current();
+       /* The THREAD_CREATE action points to the created Thread */
+       else if (curr->get_type() == THREAD_CREATE)
+               return (Thread *)curr->get_location();
        else
                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;
@@ -572,9 +587,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
        action_list_t::const_reverse_iterator rit;
 
        /* Find rf in the thread list */
-       for (rit = list->rbegin(); rit != list->rend(); rit++)
-               if (*rit == rf)
-                       break;
+       rit = std::find(list->rbegin(), list->rend(), rf);
+       ASSERT(rit != list->rend());
 
        /* Find the last write/release */
        for (; rit != list->rend(); rit++)
@@ -593,6 +607,11 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
                if (id_to_int(rf->get_tid()) == (int)i)
                        continue;
                list = &(*thrd_lists)[i];
+
+               /* Can we ensure no future writes from this thread may break
+                * the release seq? */
+               bool future_ordered = false;
+
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        const ModelAction *act = *rit;
                        if (!act->is_write())
@@ -600,13 +619,17 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
                        /* Reach synchronization -> this thread is complete */
                        if (act->happens_before(release))
                                break;
-                       if (rf->happens_before(act))
+                       if (rf->happens_before(act)) {
+                               future_ordered = true;
                                continue;
+                       }
 
                        /* Check modification order */
-                       if (mo_graph->checkReachable(rf, act))
+                       if (mo_graph->checkReachable(rf, act)) {
                                /* rf --mo--> act */
+                               future_ordered = true;
                                continue;
+                       }
                        if (mo_graph->checkReachable(act, release))
                                /* act --mo--> release */
                                break;
@@ -617,6 +640,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
                        }
                        certain = false;
                }
+               if (!future_ordered)
+                       return false; /* This thread is uncertain */
        }
 
        if (certain)
@@ -699,6 +724,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()) {
+               set_assert();
+       }
+
        return updated;
 }
 
@@ -790,6 +820,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                } else
                        promise_index++;
        }
+
        return resolved;
 }
 
@@ -824,7 +855,7 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
                                merge_cv->synchronized_since(act)) {
                        //This thread is no longer able to send values back to satisfy the promise
                        int num_synchronized_threads = promise->increment_threads();
-                       if (num_synchronized_threads == model->get_num_threads()) {
+                       if (num_synchronized_threads == get_num_threads()) {
                                //Promise has failed
                                failed_promise = true;
                                return;
@@ -972,17 +1003,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) {
                        ASSERT(current_action);
                        nextThread = check_current_action(current_action);
                        current_action = NULL;
-                       if (!curr->is_blocked())
+                       if (!curr->is_blocked() && !curr->is_complete())
                                scheduler->add_thread(curr);
-               } else if (curr->get_state() == THREAD_RUNNING) {
-                       /* Stopped while running; i.e., completed */
-                       curr->complete();
                } else {
                        ASSERT(false);
                }