threads: bugfix - do not call thread_current() from model-checker

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index cbf1f3313ac3d2e89e7053e43c96bcf32a096ed6..c832b03710fc360ab17bcb5b3afe7a5920c1cfa6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -39,7 +39,6 @@ struct bug_message {
  */
 struct model_snapshot_members {
        model_snapshot_members() :
-               current_action(NULL),
                /* First thread created will have id INITIAL_THREAD_ID */
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),
@@ -59,7 +58,6 @@ struct model_snapshot_members {
                bugs.clear();
        }
 
-       ModelAction *current_action;
        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
        ModelAction *next_backtrack;
@@ -218,7 +216,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
        if (curr != NULL) {
                /* Do not split atomic actions. */
                if (curr->is_rmwr())
-                       return thread_current();
+                       return get_thread(curr);
                else if (curr->get_type() == THREAD_CREATE)
                        return curr->get_thread_operand();
        }
@@ -296,11 +294,9 @@ void ModelChecker::execute_sleep_set()
                thread_id_t tid = int_to_id(i);
                Thread *thr = get_thread(tid);
                if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
-                       thr->set_state(THREAD_RUNNING);
                        scheduler->next_thread(thr);
                        Thread::swap(&system_context, thr);
-                       priv->current_action->set_sleep_flag();
-                       thr->set_pending(priv->current_action);
+                       thr->get_pending()->set_sleep_flag();
                }
        }
 }
@@ -970,7 +966,10 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 
        switch (curr->get_type()) {
        case THREAD_CREATE: {
-               Thread *th = curr->get_thread_operand();
+               thrd_t *thrd = (thrd_t *)curr->get_location();
+               struct thread_params *params = (struct thread_params *)curr->get_value();
+               Thread *th = new Thread(thrd, params->func, params->arg);
+               add_thread(th);
                th->set_creation(curr);
                /* Promises can be satisfied by children */
                for (unsigned int i = 0; i < promises->size(); i++) {
@@ -1213,16 +1212,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
        return true;
 }
 
-/**
- * Stores the ModelAction for the current thread action.  Call this
- * immediately before switching from user- to system-context to pass
- * data between them.
- * @param act The ModelAction created by the user-thread action
- */
-void ModelChecker::set_current_action(ModelAction *act) {
-       priv->current_action = act;
-}
-
 /**
  * This is the heart of the model checker routine. It performs model-checking
  * actions corresponding to a given "current action." Among other processes, it
@@ -2676,8 +2665,7 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
        DBG();
        Thread *old = thread_current();
-       set_current_action(act);
-       old->set_state(THREAD_READY);
+       old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
                exit(EXIT_FAILURE);
@@ -2688,12 +2676,13 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 /**
  * Takes the next step in the execution, if possible.
  * @param curr The current step to take
- * @return Returns true (success) if a step was taken and false otherwise.
+ * @return Returns the next Thread to run, if any; NULL if this execution
+ * should terminate
  */
-bool ModelChecker::take_step(ModelAction *curr)
+Thread * ModelChecker::take_step(ModelAction *curr)
 {
        if (has_asserted())
-               return false;
+               return NULL;
 
        Thread *curr_thrd = get_thread(curr);
        ASSERT(curr_thrd->get_state() == THREAD_READY);
@@ -2702,15 +2691,14 @@ bool ModelChecker::take_step(ModelAction *curr)
 
        /* Infeasible -> don't take any more steps */
        if (is_infeasible())
-               return false;
+               return NULL;
        else if (isfeasibleprefix() && have_bug_reports()) {
                set_assert();
-               return false;
+               return NULL;
        }
 
-       if (params.bound != 0)
-               if (priv->used_sequence_numbers > params.bound)
-                       return false;
+       if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
+               return NULL;
 
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())
                scheduler->remove_thread(curr_thrd);
@@ -2737,26 +2725,15 @@ bool ModelChecker::take_step(ModelAction *curr)
                ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
                                std::memory_order_seq_cst, NULL, VALUE_NONE,
                                model_thread);
-               set_current_action(fixup);
-               return true;
+               model_thread->set_pending(fixup);
+               return model_thread;
        }
 
        /* next_thrd == NULL -> don't take any more steps */
        if (!next_thrd)
-               return false;
-
-       next_thrd->set_state(THREAD_RUNNING);
-
-       if (next_thrd->get_pending() != NULL) {
-               /* restart a pending action */
-               set_current_action(next_thrd->get_pending());
-               next_thrd->set_pending(NULL);
-               next_thrd->set_state(THREAD_READY);
-               return true;
-       }
+               return NULL;
 
-       /* Return false only if swap fails with an error */
-       return (Thread::swap(&system_context, next_thrd) == 0);
+       return next_thrd;
 }
 
 /** Wrapper to run the user's main function, with appropriate arguments */
@@ -2771,15 +2748,18 @@ void ModelChecker::run()
        do {
                thrd_t user_thread;
                Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
-
                add_thread(t);
 
-               /* Run user thread up to its first action */
-               scheduler->next_thread(t);
-               Thread::swap(&system_context, t);
+               do {
+                       scheduler->next_thread(t);
+                       Thread::swap(&system_context, t);
 
-               /* Wait for all threads to complete */
-               while (take_step(priv->current_action));
+                       /* Consume the next action for a Thread */
+                       ModelAction *curr = t->get_pending();
+                       t->set_pending(NULL);
+                       t = take_step(curr);
+               } while (t && !t->is_model_thread());
+               /** @TODO Re-write release sequence fixups here */
        } while (next_execution());
 
        print_stats();