create enumeration for enabled information...switch from bools to the enumeration

diff --git a/nodestack.cc b/nodestack.cc
index 6b1d4ef9c86929fdd14d14172149abaacec96133..4cf89500fc1faba0f98714173fbd4eca557edefa 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -47,7 +47,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
                                if (prevfi) {
                                        *fi=*prevfi;
                                }
                                if (prevfi) {
                                        *fi=*prevfi;
                                }

-                               if (parent->enabled_array[i]) {
+                               if (parent->enabled_array[i]==THREAD_ENABLED) {

                                        fi->enabled_count++;
                                }
                                if (i==currtid) {
                                        fi->enabled_count++;
                                }
                                if (i==currtid) {


@@ -56,7 +56,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
                                }
                                //Do window processing
                                if (prevfairness != NULL) {
                                }
                                //Do window processing
                                if (prevfairness != NULL) {

-                                       if (prevfairness -> parent->enabled_array[i])
+                                       if (prevfairness -> parent->enabled_array[i] == THREAD_ENABLED)

                                                fi->enabled_count--;
                                        if (i==prevtid) {
                                                fi->turns--;
                                                fi->enabled_count--;
                                        if (i==prevtid) {
                                                fi->turns--;


@@ -216,15 +216,15 @@ bool Node::read_from_empty() {
  * Mark the appropriate backtracking information for exploring a thread choice.
  * @param act The ModelAction to explore
  */
  * Mark the appropriate backtracking information for exploring a thread choice.
  * @param act The ModelAction to explore
  */

-void Node::explore_child(ModelAction *act, bool * is_enabled)
+void Node::explore_child(ModelAction *act, enabled_type_t * is_enabled)

 {
        if ( ! enabled_array )
 {
        if ( ! enabled_array )

-               enabled_array=(bool *)model_malloc(sizeof(bool)*num_threads);
+               enabled_array=(enabled_type_t *)model_malloc(sizeof(enabled_type_t)*num_threads);

        if (is_enabled != NULL)
        if (is_enabled != NULL)

-               memcpy(enabled_array, is_enabled, sizeof(bool)*num_threads);
+               memcpy(enabled_array, is_enabled, sizeof(enabled_type_t)*num_threads);

        else {
                for(int i=0;i<num_threads;i++)
        else {
                for(int i=0;i<num_threads;i++)

-                       enabled_array[i]=false;
+                       enabled_array[i]=THREAD_DISABLED;

        }
 
        explore(act->get_tid());
        }
 
        explore(act->get_tid());


@@ -265,13 +265,13 @@ thread_id_t Node::get_next_backtrack()
 bool Node::is_enabled(Thread *t)
 {
        int thread_id=id_to_int(t->get_id());
 bool Node::is_enabled(Thread *t)
 {
        int thread_id=id_to_int(t->get_id());

-       return thread_id < num_threads && enabled_array[thread_id];
+       return thread_id < num_threads && (enabled_array[thread_id] == THREAD_ENABLED);

 }
 
 bool Node::is_enabled(thread_id_t tid)
 {
        int thread_id=id_to_int(tid);
 }
 
 bool Node::is_enabled(thread_id_t tid)
 {
        int thread_id=id_to_int(tid);

-       return thread_id < num_threads && enabled_array[thread_id];
+       return thread_id < num_threads && (enabled_array[thread_id] == THREAD_ENABLED);

 }
 
 bool Node::has_priority(thread_id_t tid)
 }
 
 bool Node::has_priority(thread_id_t tid)


@@ -391,7 +391,7 @@ void NodeStack::print()
 /** Note: The is_enabled set contains what actions were enabled when
  *  act was chosen. */
 
 /** Note: The is_enabled set contains what actions were enabled when
  *  act was chosen. */
 

-ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
+ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t * is_enabled)

 {
        DBG();
 
 {
        DBG();
 

diff --git a/nodestack.h b/nodestack.h
index fca063e7a4f86c2462f75a01f006d9c911487a26..55deac5beffa2a6a0d3deec210c4246f0b8074db 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -12,6 +12,7 @@
 
 #include "mymemory.h"
 #include "modeltypes.h"
 
 #include "mymemory.h"
 #include "modeltypes.h"

+#include "schedule.h"

 
 class ModelAction;
 class Thread;
 
 class ModelAction;
 class Thread;


@@ -59,7 +60,7 @@ public:
        /* return true = backtrack set is empty */
        bool backtrack_empty();
 
        /* return true = backtrack set is empty */
        bool backtrack_empty();
 

-       void explore_child(ModelAction *act, bool * is_enabled);
+       void explore_child(ModelAction *act, enabled_type_t * is_enabled);

        /* return false = thread was already in backtrack */
        bool set_backtrack(thread_id_t id);
        thread_id_t get_next_backtrack();
        /* return false = thread was already in backtrack */
        bool set_backtrack(thread_id_t id);
        thread_id_t get_next_backtrack();


@@ -104,7 +105,7 @@ private:
        std::vector< bool, ModelAlloc<bool> > backtrack;
        std::vector< struct fairness_info, ModelAlloc< struct fairness_info> > fairness;
        int numBacktracks;
        std::vector< bool, ModelAlloc<bool> > backtrack;
        std::vector< struct fairness_info, ModelAlloc< struct fairness_info> > fairness;
        int numBacktracks;

-       bool *enabled_array;
+       enabled_type_t *enabled_array;

 
        /** The set of ModelActions that this the action at this Node may read
         *  from. Only meaningful if this Node represents a 'read' action. */
 
        /** The set of ModelActions that this the action at this Node may read
         *  from. Only meaningful if this Node represents a 'read' action. */


@@ -131,7 +132,7 @@ class NodeStack {
 public:
        NodeStack();
        ~NodeStack();
 public:
        NodeStack();
        ~NodeStack();

-       ModelAction * explore_action(ModelAction *act, bool * is_enabled);
+       ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled);

        Node * get_head();
        Node * get_next();
        void reset_execution();
        Node * get_head();
        Node * get_next();
        void reset_execution();

diff --git a/promise.cc b/promise.cc
index 259ba058ddba82bbd8eaeb0b8559a24144cd087e..5197ed3a1e0376d1ea4f6060bcfa042f7cd4f0e9 100644 (file)
--- a/promise.cc
+++ b/promise.cc
@@ -11,10 +11,10 @@ bool Promise::increment_threads(thread_id_t tid) {
                return false;
        
        synced_thread[id]=true;
                return false;
        
        synced_thread[id]=true;

-       bool * enabled=model->get_scheduler()->get_enabled();
+       enabled_type_t * enabled=model->get_scheduler()->get_enabled();

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

-               if (!synced_thread[id] && enabled[id])
+               if (!synced_thread[id] && (enabled[id] == THREAD_ENABLED))

                        return false;
        }
        return true;
                        return false;
        }
        return true;

diff --git a/schedule.cc b/schedule.cc
index 88200a81cc650617044b4b0449477fbed1afb4e9..a236bd0cc66644197e178e00d4cc44b0a195f3c2 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -15,13 +15,13 @@ Scheduler::Scheduler() :
 {
 }
 
 {
 }
 

-void Scheduler::set_enabled(Thread *t, bool enabled_status) {
+void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {

        int threadid=id_to_int(t->get_id());
        if (threadid>=enabled_len) {
        int threadid=id_to_int(t->get_id());
        if (threadid>=enabled_len) {

-               bool *new_enabled = (bool *)snapshot_malloc(sizeof(bool) * (threadid + 1));
-               memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(bool));
+               enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1));
+               memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(enabled_type_t));

                if (is_enabled != NULL) {
                if (is_enabled != NULL) {

-                       memcpy(new_enabled, is_enabled, enabled_len*sizeof(bool));
+                       memcpy(new_enabled, is_enabled, enabled_len*sizeof(enabled_type_t));

                        snapshot_free(is_enabled);
                }
                is_enabled=new_enabled;
                        snapshot_free(is_enabled);
                }
                is_enabled=new_enabled;


@@ -37,7 +37,7 @@ void Scheduler::set_enabled(Thread *t, bool enabled_status) {
 void Scheduler::add_thread(Thread *t)
 {
        DEBUG("thread %d\n", id_to_int(t->get_id()));
 void Scheduler::add_thread(Thread *t)
 {
        DEBUG("thread %d\n", id_to_int(t->get_id()));

-       set_enabled(t, true);
+       set_enabled(t, THREAD_ENABLED);

 }
 
 /**
 }
 
 /**


@@ -48,7 +48,7 @@ void Scheduler::remove_thread(Thread *t)
 {
        if (current == t)
                current = NULL;
 {
        if (current == t)
                current = NULL;

-       set_enabled(t, false);
+       set_enabled(t, THREAD_DISABLED);

 }
 
 /**
 }
 
 /**


@@ -58,7 +58,7 @@ void Scheduler::remove_thread(Thread *t)
  */
 void Scheduler::sleep(Thread *t)
 {
  */
 void Scheduler::sleep(Thread *t)
 {

-       set_enabled(t, false);
+       set_enabled(t, THREAD_DISABLED);

        t->set_state(THREAD_BLOCKED);
 }
 
        t->set_state(THREAD_BLOCKED);
 }
 


@@ -68,7 +68,7 @@ void Scheduler::sleep(Thread *t)
  */
 void Scheduler::wake(Thread *t)
 {
  */
 void Scheduler::wake(Thread *t)
 {

-       set_enabled(t, true);
+       set_enabled(t, THREAD_DISABLED);

        t->set_state(THREAD_READY);
 }
 
        t->set_state(THREAD_READY);
 }
 

diff --git a/schedule.h b/schedule.h
index fb4d082adc2dbe220baf49d8347fc70fe6c0d560..18936b612dacbed81e91a949d164e990b5f964b5 100644 (file)
--- a/schedule.h
+++ b/schedule.h
@@ -11,6 +11,12 @@
 /* Forward declaration */
 class Thread;
 
 /* Forward declaration */
 class Thread;
 

+typedef enum enabled_type {
+       THREAD_DISABLED,
+       THREAD_ENABLED,
+       THREAD_SLEEP_SET
+} enabled_type_t;
+

 /** @brief The Scheduler class performs the mechanics of Thread execution
  * scheduling. */
 class Scheduler {
 /** @brief The Scheduler class performs the mechanics of Thread execution
  * scheduling. */
 class Scheduler {


@@ -23,15 +29,15 @@ public:
        Thread * next_thread(Thread *t);
        Thread * get_current_thread() const;
        void print() const;
        Thread * next_thread(Thread *t);
        Thread * get_current_thread() const;
        void print() const;

-       bool * get_enabled() { return is_enabled; };
+       enabled_type_t * get_enabled() { return is_enabled; };

 
        SNAPSHOTALLOC
 private:
        /** The list of available Threads that are not currently running */
 
        SNAPSHOTALLOC
 private:
        /** The list of available Threads that are not currently running */

-       bool * is_enabled;
+       enabled_type_t * is_enabled;

        int enabled_len;
        int curr_thread_index;
        int enabled_len;
        int curr_thread_index;

-       void set_enabled(Thread *t, bool enabled_status);
+       void set_enabled(Thread *t, enabled_type_t enabled_status);

 
        /** The currently-running Thread */
        Thread *current;
 
        /** The currently-running Thread */
        Thread *current;