fairness changes...

fix bug with putting enabled information in wrong place
reveals norris bug...

diff --git a/main.cc b/main.cc
index 31184fc559e6a6dc524f47bd58e60f8c7920c21e..26d8beb79d52f8d09a9d16b97f96c79972941822 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -17,6 +17,8 @@
 static void param_defaults(struct model_params * params) {
        params->maxreads = 0;
        params->maxfuturedelay = 100;
 static void param_defaults(struct model_params * params) {
        params->maxreads = 0;
        params->maxfuturedelay = 100;

+       params->fairwindow = 0;
+       params->enabledcount = 1;

 }
 
 static void print_usage(struct model_params *params) {
 }
 
 static void print_usage(struct model_params *params) {


@@ -30,13 +32,17 @@ static void print_usage(struct model_params *params) {
 "-s                    Maximum actions that the model checker will wait for\n"
 "                      a write from the future past the expected number of\n"
 "                      actions. Default: %d\n"
 "-s                    Maximum actions that the model checker will wait for\n"
 "                      a write from the future past the expected number of\n"
 "                      actions. Default: %d\n"

+"-f                    Specify a fairness window in which actions that are\n"
+"                      enabled sufficiently many times should receive\n"
+"                      priority for execution. Default: %d\n"
+"-e                    Enabled count. Default: %d\n"

 "--                    Program arguments follow.\n\n",
 "--                    Program arguments follow.\n\n",

-                       params->maxreads, params->maxfuturedelay);
+params->maxreads, params->maxfuturedelay, params->fairwindow, params->enabledcount);

        exit(EXIT_SUCCESS);
 }
 
 static void parse_options(struct model_params *params, int *argc, char ***argv) {
        exit(EXIT_SUCCESS);
 }
 
 static void parse_options(struct model_params *params, int *argc, char ***argv) {

-       const char *shortopts = "hm:s:";
+       const char *shortopts = "hm:s:f:e:";

        int opt;
        bool error = false;
        while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
        int opt;
        bool error = false;
        while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {


@@ -47,6 +53,12 @@ static void parse_options(struct model_params *params, int *argc, char ***argv)
                case 's':
                        params->maxfuturedelay = atoi(optarg);
                        break;
                case 's':
                        params->maxfuturedelay = atoi(optarg);
                        break;

+               case 'f':
+                       params->fairwindow = atoi(optarg);
+                       break;
+               case 'e':
+                       params->enabledcount = atoi(optarg);
+                       break;

                case 'm':
                        params->maxreads = atoi(optarg);
                        break;
                case 'm':
                        params->maxreads = atoi(optarg);
                        break;

diff --git a/model.cc b/model.cc
index 0283911b6eea07e57c7b7266fe3c80fc2d755595..03a0c689431c90720ec56a1020ef21344920ac08 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -20,10 +20,10 @@ ModelChecker *model;
 /** @brief Constructor */
 ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */
 /** @brief Constructor */
 ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */

+       params(params),

        scheduler(new Scheduler()),
        num_executions(0),
        num_feasible_executions(0),
        scheduler(new Scheduler()),
        num_executions(0),
        num_feasible_executions(0),

-       params(params),

        diverge(NULL),
        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),
        diverge(NULL),
        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),


@@ -277,6 +277,20 @@ void ModelChecker::set_backtracking(ModelAction *act)
                if (node->has_been_explored(tid))
                        continue;
 
                if (node->has_been_explored(tid))
                        continue;
 

+               /* See if fairness allows */
+               if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
+                       bool unfair=false;
+                       for(int t=0;t<node->get_num_threads();t++) {
+                               thread_id_t tother=int_to_id(t);
+                               if (node->is_enabled(tother) && node->has_priority(tother)) {
+                                       unfair=true;
+                                       break;
+                               }
+                       }
+                       if (unfair)
+                               continue;
+               }
+

                /* Cache the latest backtracking point */
                if (!priv->next_backtrack || *prev > *priv->next_backtrack)
                        priv->next_backtrack = prev;
                /* Cache the latest backtracking point */
                if (!priv->next_backtrack || *prev > *priv->next_backtrack)
                        priv->next_backtrack = prev;

diff --git a/model.h b/model.h
index 13704241a83285dba37651a5e7b8ea699a1d2281..0701d467d21f12eeedcad6e88787103b33966e97 100644 (file)
--- a/model.h
+++ b/model.h
@@ -34,6 +34,8 @@ typedef std::vector< const ModelAction *, MyAlloc<const ModelAction *> > rel_hea
 struct model_params {
        int maxreads;
        int maxfuturedelay;
 struct model_params {
        int maxreads;
        int maxfuturedelay;

+       unsigned int fairwindow;
+       unsigned int enabledcount;

 };
 
 struct PendingFutureValue {
 };
 
 struct PendingFutureValue {


@@ -92,6 +94,7 @@ public:
        void finish_execution();
        bool isfeasibleprefix();
        void set_assert() {asserted=true;}
        void finish_execution();
        bool isfeasibleprefix();
        void set_assert() {asserted=true;}

+       const model_params params;

 
        MEMALLOC
 private:
 
        MEMALLOC
 private:


@@ -104,7 +107,6 @@ private:
        int num_executions;
        int num_feasible_executions;
        bool promises_expired();
        int num_executions;
        int num_feasible_executions;
        bool promises_expired();

-       const model_params params;

 
        /**
         * Stores the ModelAction for the current thread action.  Call this
 
        /**
         * Stores the ModelAction for the current thread action.  Call this

diff --git a/nodestack.cc b/nodestack.cc
index 86d7f6bbc61a5f88caeb56ff54810e255514a0fd..378dd8f4eebf3a5636a6203edd4eb4f381252343 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -19,26 +19,55 @@
  * @param nthreads The number of threads which exist at this point in the
  * execution trace.
  */
  * @param nthreads The number of threads which exist at this point in the
  * execution trace.
  */

-Node::Node(ModelAction *act, Node *par, int nthreads, bool *enabled)
+Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)

        : action(act),
        parent(par),
        num_threads(nthreads),
        explored_children(num_threads),
        backtrack(num_threads),
        : action(act),
        parent(par),
        num_threads(nthreads),
        explored_children(num_threads),
        backtrack(num_threads),

+       fairness(num_threads),

        numBacktracks(0),
        numBacktracks(0),

+       enabled_array(NULL),

        may_read_from(),
        read_from_index(0),
        future_values(),
        future_index(-1)
 {
        may_read_from(),
        read_from_index(0),
        future_values(),
        future_index(-1)
 {

-       if (act)
+       if (act) {

                act->set_node(this);
                act->set_node(this);

-       enabled_array=(bool *)MYMALLOC(sizeof(bool)*num_threads);
-       if (enabled != NULL)
-               memcpy(enabled_array, enabled, sizeof(bool)*num_threads);
-       else {
-               for(int i=0;i<num_threads;i++)
-                       enabled_array[i]=false;
+               int currtid=id_to_int(act->get_tid());
+               int prevtid=(prevfairness != NULL)?id_to_int(prevfairness->action->get_tid()):0;
+               
+               if ( model->params.fairwindow != 0 ) {
+                       for(int i=0;i<nthreads;i++) {
+                               ASSERT(i<((int)fairness.size()));
+                               struct fairness_info * fi=& fairness[i];
+                               struct fairness_info * prevfi=(par!=NULL)&&(i<par->get_num_threads())?&par->fairness[i]:NULL;
+                               if (prevfi) {
+                                       *fi=*prevfi;
+                               }
+                               if (parent->enabled_array[i]) {
+                                       fi->enabled_count++;
+                               }
+                               if (i==currtid) {
+                                       fi->turns++;
+                                       fi->priority = false;
+                               }
+                               //Do window processing
+                               if (prevfairness != NULL) {
+                                       if (prevfairness -> parent->enabled_array[i])
+                                               fi->enabled_count--;
+                                       if (i==prevtid) {
+                                               fi->turns--;
+                                       }
+                                       //Need full window to start evaluating conditions
+                                       //If we meet the enabled count and have no turns, give us priority
+                                       if ((fi->enabled_count >= model->params.enabledcount) &&
+                                                       (fi->turns == 0))
+                                               fi->priority = true;
+                               }
+                       }
+               }

        }
 }
 
        }
 }
 


@@ -47,7 +76,8 @@ Node::~Node()
 {
        if (action)
                delete action;
 {
        if (action)
                delete action;

-       MYFREE(enabled_array);
+       if (enabled_array)
+               MYFREE(enabled_array);

 }
 
 /** Prints debugging info for the ModelAction associated with this Node */
 }
 
 /** Prints debugging info for the ModelAction associated with this Node */


@@ -183,8 +213,17 @@ 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)
+void Node::explore_child(ModelAction *act, bool * is_enabled)

 {
 {

+       if ( ! enabled_array )
+               enabled_array=(bool *)MYMALLOC(sizeof(bool)*num_threads);
+       if (is_enabled != NULL)
+               memcpy(enabled_array, is_enabled, sizeof(bool)*num_threads);
+       else {
+               for(int i=0;i<num_threads;i++)
+                       enabled_array[i]=false;
+       }
+

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


@@ -305,58 +344,51 @@ void Node::explore(thread_id_t tid)
        explored_children[i] = true;
 }
 
        explored_children[i] = true;
 }
 

-static void clear_node_list(node_list_t *list, node_list_t::iterator start,
-                                               node_list_t::iterator end)
-{
-       node_list_t::iterator it;
-
-       for (it = start; it != end; it++)
-               delete (*it);
-       list->erase(start, end);
-}
-

 NodeStack::NodeStack()
        : total_nodes(0)
 {
        node_list.push_back(new Node());
        total_nodes++;
 NodeStack::NodeStack()
        : total_nodes(0)
 {
        node_list.push_back(new Node());
        total_nodes++;

-       iter = node_list.begin();
+       iter = 0;

 }
 
 NodeStack::~NodeStack()
 {
 }
 
 NodeStack::~NodeStack()
 {

-       clear_node_list(&node_list, node_list.begin(), node_list.end());

 }
 
 void NodeStack::print()
 {
 }
 
 void NodeStack::print()
 {

-       node_list_t::iterator it;

        printf("............................................\n");
        printf("NodeStack printing node_list:\n");
        printf("............................................\n");
        printf("NodeStack printing node_list:\n");

-       for (it = node_list.begin(); it != node_list.end(); it++) {
+       for (unsigned int it = 0; it < node_list.size(); it++) {

                if (it == this->iter)
                        printf("vvv following action is the current iterator vvv\n");
                if (it == this->iter)
                        printf("vvv following action is the current iterator vvv\n");

-               (*it)->print();
+               node_list[it]->print();

        }
        printf("............................................\n");
 }
 
        }
        printf("............................................\n");
 }
 

+/** Note: The is_enabled set contains what actions were enabled when
+ *  act was chosen. */
+

 ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
 {
        DBG();
 
        ASSERT(!node_list.empty());
 ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
 {
        DBG();
 
        ASSERT(!node_list.empty());

-       node_list_t::iterator it=iter;
-       it++;

 
 

-       if (it != node_list.end()) {
+       if ((iter+1) < node_list.size()) {

                iter++;
                iter++;

-               return (*iter)->get_action();
+               return node_list[iter]->get_action();

        }
 
        /* Record action */
        }
 
        /* Record action */

-       get_head()->explore_child(act);
-       node_list.push_back(new Node(act, get_head(), model->get_num_threads(), is_enabled));
+       get_head()->explore_child(act, is_enabled);
+       Node *prevfairness = NULL;
+       if ( model->params.fairwindow != 0 && iter > model->params.fairwindow ) {
+               prevfairness = node_list[iter-model->params.fairwindow];
+       }
+       node_list.push_back(new Node(act, get_head(), model->get_num_threads(), prevfairness));

        total_nodes++;
        iter++;
        return NULL;
        total_nodes++;
        iter++;
        return NULL;


@@ -373,35 +405,32 @@ ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
 void NodeStack::pop_restofstack(int numAhead)
 {
        /* Diverging from previous execution; clear out remainder of list */
 void NodeStack::pop_restofstack(int numAhead)
 {
        /* Diverging from previous execution; clear out remainder of list */

-       node_list_t::iterator it = iter;
-       while (numAhead--)
-               it++;
-       clear_node_list(&node_list, it, node_list.end());
+       unsigned int it=iter+numAhead;
+       node_list.resize(it);

 }
 
 Node * NodeStack::get_head()
 {
        if (node_list.empty())
                return NULL;
 }
 
 Node * NodeStack::get_head()
 {
        if (node_list.empty())
                return NULL;

-       return *iter;
+       return node_list[iter];

 }
 
 Node * NodeStack::get_next()
 {
 }
 
 Node * NodeStack::get_next()
 {

-       node_list_t::iterator it = iter;

        if (node_list.empty()) {
                DEBUG("Empty\n");
                return NULL;
        }
        if (node_list.empty()) {
                DEBUG("Empty\n");
                return NULL;
        }

-       it++;
-       if (it == node_list.end()) {
+       unsigned int it=iter+1;
+       if (it == node_list.size()) {

                DEBUG("At end\n");
                return NULL;
        }
                DEBUG("At end\n");
                return NULL;
        }

-       return *it;
+       return node_list[it];

 }
 
 void NodeStack::reset_execution()
 {
 }
 
 void NodeStack::reset_execution()
 {

-       iter = node_list.begin();
+       iter = 0;

 }
 }

diff --git a/nodestack.h b/nodestack.h
index a06bef40570556ddbf52bff19959423aaca159a6..1f7d3e4ad3fee660027e974261b8083b3a99e0c3 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -32,6 +32,12 @@ struct future_value {
        modelclock_t expiration;
 };
 
        modelclock_t expiration;
 };
 

+struct fairness_info {
+       unsigned int enabled_count;
+       unsigned int turns;
+       bool priority;
+};
+

 
 /**
  * @brief A single node in a NodeStack
 
 /**
  * @brief A single node in a NodeStack


@@ -44,21 +50,22 @@ struct future_value {
  */
 class Node {
 public:
  */
 class Node {
 public:

-       Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, bool *enabled_array = NULL);
+       Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, Node *prevfairness = NULL);

        ~Node();
        /* return true = thread choice has already been explored */
        bool has_been_explored(thread_id_t tid);
        /* return true = backtrack set is empty */
        bool backtrack_empty();
 
        ~Node();
        /* return true = thread choice has already been explored */
        bool has_been_explored(thread_id_t tid);
        /* return true = backtrack set is empty */
        bool backtrack_empty();
 

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

        /* return false = thread was already in backtrack */
        bool set_backtrack(thread_id_t id);
        thread_id_t get_next_backtrack();
        bool is_enabled(Thread *t);
        bool is_enabled(thread_id_t tid);
        ModelAction * get_action() { return action; }
        /* return false = thread was already in backtrack */
        bool set_backtrack(thread_id_t id);
        thread_id_t get_next_backtrack();
        bool is_enabled(Thread *t);
        bool is_enabled(thread_id_t tid);
        ModelAction * get_action() { return action; }

-
+       bool has_priority(thread_id_t tid) {return fairness[id_to_int(tid)].priority;}
+       int get_num_threads() {return num_threads;}

        /** @return the parent Node to this Node; that is, the action that
         * occurred previously in the stack. */
        Node * get_parent() const { return parent; }
        /** @return the parent Node to this Node; that is, the action that
         * occurred previously in the stack. */
        Node * get_parent() const { return parent; }


@@ -93,6 +100,7 @@ private:
        int num_threads;
        std::vector< bool, MyAlloc<bool> > explored_children;
        std::vector< bool, MyAlloc<bool> > backtrack;
        int num_threads;
        std::vector< bool, MyAlloc<bool> > explored_children;
        std::vector< bool, MyAlloc<bool> > backtrack;

+       std::vector< struct fairness_info, MyAlloc< struct fairness_info> > fairness;

        int numBacktracks;
        bool *enabled_array;
 
        int numBacktracks;
        bool *enabled_array;
 


@@ -107,7 +115,7 @@ private:
        unsigned int future_index;
 };
 
        unsigned int future_index;
 };
 

-typedef std::list< Node *, MyAlloc< Node * > > node_list_t;
+typedef std::vector< Node *, MyAlloc< Node * > > node_list_t;

 
 /**
  * @brief A stack of nodes
 
 /**
  * @brief A stack of nodes


@@ -133,7 +141,7 @@ public:
        MEMALLOC
 private:
        node_list_t node_list;
        MEMALLOC
 private:
        node_list_t node_list;

-       node_list_t::iterator iter;
+       unsigned int iter;

 
        int total_nodes;
 };
 
        int total_nodes;
 };

diff --git a/schedule.cc b/schedule.cc
index 10a335cb3ef82e2428a802d449e9bf75d61b0268..7a703abab8cc7e229f7218c85add8580c7f3ad53 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -73,8 +73,8 @@ void Scheduler::wake(Thread *t)
 }
 
 /**
 }
 
 /**

- * Remove one Thread from the scheduler. This implementation defaults to FIFO,
- * if a thread is not already provided.
+ * Select a Thread. This implementation defaults to round-robin, if a
+ * thread is not already provided.

  *
  * @param t Thread to run, if chosen by an external entity (e.g.,
  * ModelChecker). May be NULL to indicate no external choice.
  *
  * @param t Thread to run, if chosen by an external entity (e.g.,
  * ModelChecker). May be NULL to indicate no external choice.