Add back model_thread; it is still needed

diff --git a/execution.cc b/execution.cc
index 61d33cb9b629478a4d442bebfbacd155c4383fc6..d2efaba7a95dd522c96ba712eb4c761e7e36de60 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -87,6 +87,8 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */

+       model_thread = new Thread(get_next_id());
+       add_thread(model_thread);

        fuzzer->register_engine(m, this);
        scheduler->register_engine(this);
 #ifdef TLS
        fuzzer->register_engine(m, this);
        scheduler->register_engine(this);
 #ifdef TLS


@@ -97,7 +99,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
 /** @brief Destructor */
 ModelExecution::~ModelExecution()
 {
 /** @brief Destructor */
 ModelExecution::~ModelExecution()
 {

-       for (unsigned int i = 0;i < get_num_threads();i++)
+       for (unsigned int i = INITIAL_THREAD_ID;i < get_num_threads();i++)

                delete get_thread(int_to_id(i));
 
        delete mo_graph;
                delete get_thread(int_to_id(i));
 
        delete mo_graph;


@@ -266,7 +268,7 @@ bool ModelExecution::should_wake_up(const ModelAction * asleep) const
 
 void ModelExecution::wake_up_sleeping_actions()
 {
 
 void ModelExecution::wake_up_sleeping_actions()
 {

-       for (unsigned int i = 0;i < get_num_threads();i++) {
+       for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {

                thread_id_t tid = int_to_id(i);
                if (scheduler->is_sleep_set(tid)) {
                        Thread *thr = get_thread(tid);
                thread_id_t tid = int_to_id(i);
                if (scheduler->is_sleep_set(tid)) {
                        Thread *thr = get_thread(tid);


@@ -345,7 +347,7 @@ void ModelExecution::set_assert()
 bool ModelExecution::is_deadlocked() const
 {
        bool blocking_threads = false;
 bool ModelExecution::is_deadlocked() const
 {
        bool blocking_threads = false;

-       for (unsigned int i = 0;i < get_num_threads();i++) {
+       for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {

                thread_id_t tid = int_to_id(i);
                if (is_enabled(tid))
                        return false;
                thread_id_t tid = int_to_id(i);
                if (is_enabled(tid))
                        return false;


@@ -365,7 +367,7 @@ bool ModelExecution::is_deadlocked() const
  */
 bool ModelExecution::is_complete_execution() const
 {
  */
 bool ModelExecution::is_complete_execution() const
 {

-       for (unsigned int i = 0;i < get_num_threads();i++)
+       for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++)

                if (is_enabled(int_to_id(i)))
                        return false;
        return true;
                if (is_enabled(int_to_id(i)))
                        return false;
        return true;


@@ -494,7 +496,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
        case ATOMIC_WAIT: {
                Thread *curr_thrd = get_thread(curr);
                /* wake up the other threads */
        case ATOMIC_WAIT: {
                Thread *curr_thrd = get_thread(curr);
                /* wake up the other threads */

-               for (unsigned int i = 0;i < get_num_threads();i++) {
+               for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {

                        Thread *t = get_thread(int_to_id(i));
                        if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
                                scheduler->wake(t);
                        Thread *t = get_thread(int_to_id(i));
                        if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
                                scheduler->wake(t);


@@ -523,7 +525,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                }
 
                /* wake up the other threads */
                }
 
                /* wake up the other threads */

-               for (unsigned int i = 0;i < get_num_threads();i++) {
+               for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {

                        Thread *t = get_thread(int_to_id(i));
                        if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
                                scheduler->wake(t);
                        Thread *t = get_thread(int_to_id(i));
                        if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
                                scheduler->wake(t);


@@ -543,7 +545,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                // TODO: lock count for recursive mutexes
                /* wake up the other threads */
                Thread *curr_thrd = get_thread(curr);
                // TODO: lock count for recursive mutexes
                /* wake up the other threads */
                Thread *curr_thrd = get_thread(curr);

-               for (unsigned int i = 0;i < get_num_threads();i++) {
+               for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {

                        Thread *t = get_thread(int_to_id(i));
                        if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
                                scheduler->wake(t);
                        Thread *t = get_thread(int_to_id(i));
                        if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
                                scheduler->wake(t);


@@ -675,7 +677,7 @@ void ModelExecution::process_thread_action(ModelAction *curr)
                }
 
                /* Wake up any joining threads */
                }
 
                /* Wake up any joining threads */

-               for (unsigned int i = 0;i < get_num_threads();i++) {
+               for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {

                        Thread *waiting = get_thread(int_to_id(i));
                        if (waiting->waiting_on() == th &&
                                        waiting->get_pending()->is_thread_join())
                        Thread *waiting = get_thread(int_to_id(i));
                        if (waiting->waiting_on() == th &&
                                        waiting->get_pending()->is_thread_join())

diff --git a/execution.h b/execution.h
index b8bfb03580c324309c2af068d6239fed005f5eba..5e80e186e01d95677c11e46d677d437a87b60386 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -19,7 +19,8 @@
 #include <condition_variable>
 #include "classlist.h"
 
 #include <condition_variable>
 #include "classlist.h"
 

-#define INITIAL_THREAD_ID       0
+#define INITIAL_THREAD_ID      0
+#define MAIN_THREAD_ID         1

 
 struct PendingFutureValue {
        PendingFutureValue(ModelAction *writer, ModelAction *reader) :
 
 struct PendingFutureValue {
        PendingFutureValue(ModelAction *writer, ModelAction *reader) :

diff --git a/model.cc b/model.cc
index 4b94d75a9016a2b4d0cffaab2e9e6ced32f808cc..f73377062c7a09b6e4108d56cb5421b7674785a2 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -75,7 +75,7 @@ ModelChecker::ModelChecker() :
        history(new ModelHistory()),
        execution(new ModelExecution(this, scheduler)),
        execution_number(1),
        history(new ModelHistory()),
        execution(new ModelExecution(this, scheduler)),
        execution_number(1),

-       curr_thread_num(INITIAL_THREAD_ID),
+       curr_thread_num(MAIN_THREAD_ID),

        trace_analyses(),
        inspect_plugin(NULL)
 {
        trace_analyses(),
        inspect_plugin(NULL)
 {


@@ -353,7 +353,7 @@ void ModelChecker::startRunExecution(Thread *old) {
                        execution->collectActions();
                }
 
                        execution->collectActions();
                }
 

-               curr_thread_num = INITIAL_THREAD_ID;
+               curr_thread_num = MAIN_THREAD_ID;

                Thread *thr = getNextThread(old);
                if (thr != nullptr) {
                        scheduler->set_current_thread(thr);
                Thread *thr = getNextThread(old);
                if (thr != nullptr) {
                        scheduler->set_current_thread(thr);


@@ -421,7 +421,7 @@ void ModelChecker::finishRunExecution(Thread *old)
        scheduler->set_current_thread(NULL);
 
        /** Reset curr_thread_num to initial value for next execution. */
        scheduler->set_current_thread(NULL);
 
        /** Reset curr_thread_num to initial value for next execution. */

-       curr_thread_num = INITIAL_THREAD_ID;
+       curr_thread_num = MAIN_THREAD_ID;

 
        /** If we have more executions, we won't make it past this call. */
        finish_execution(execution_number < params.maxexecutions);
 
        /** If we have more executions, we won't make it past this call. */
        finish_execution(execution_number < params.maxexecutions);

diff --git a/threads.cc b/threads.cc
index 024f6ea582e12381b8a76e5c8f53972f57ba48c7..bd1b624959629d3613e76afda0b72a58e795d122 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -419,7 +419,9 @@ Thread::Thread(thread_id_t tid) :
        last_action_val(0),
        model_thread(true)
 {
        last_action_val(0),
        model_thread(true)
 {

-       real_memset(&context, 0, sizeof(context));
+       // real_memset is not defined when
+       // the model thread is constructed
+       memset(&context, 0, sizeof(context));

 }
 
 /**
 }
 
 /**