threads/model: allocate Thread from w/in ModelChecker

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index cbf1f3313ac3d2e89e7053e43c96bcf32a096ed6..400adc208047f8d2c7b4700c31bc20b650854e34 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -296,7 +296,6 @@ 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();
@@ -970,7 +969,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++) {
@@ -2677,7 +2679,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        DBG();
        Thread *old = thread_current();
        set_current_action(act);
-       old->set_state(THREAD_READY);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
                exit(EXIT_FAILURE);
@@ -2745,13 +2746,10 @@ bool ModelChecker::take_step(ModelAction *curr)
        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;
        }