add yield support

diff --git a/action.cc b/action.cc
index be8c4a6c0cdc69bde75fd08436a33705fa9157af..4b380c2dd404fafc1b4be9846433967daa8cd167 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -151,6 +151,11 @@ bool ModelAction::could_be_write() const
        return is_write() || is_rmwr();
 }
 
        return is_write() || is_rmwr();
 }
 

+bool ModelAction::is_yield() const
+{
+       return type == THREAD_YIELD;
+}
+

 bool ModelAction::is_rmwr() const
 {
        return type == ATOMIC_RMWR;
 bool ModelAction::is_rmwr() const
 {
        return type == ATOMIC_RMWR;

diff --git a/action.h b/action.h
index a20792033f471ba21744b9de870aa42840490f38..e375016e4c96367634a207f8f92948a5ac56c965 100644 (file)
--- a/action.h
+++ b/action.h
@@ -121,6 +121,7 @@ public:
        bool is_uninitialized() const;
        bool is_read() const;
        bool is_write() const;
        bool is_uninitialized() const;
        bool is_read() const;
        bool is_write() const;

+       bool is_yield() const;

        bool could_be_write() const;
        bool is_rmwr() const;
        bool is_rmwc() const;
        bool could_be_write() const;
        bool is_rmwr() const;
        bool is_rmwc() const;

diff --git a/libthreads.cc b/libthreads.cc
index 8e213aa858be5f56510871412e2cee3c906b78d6..75d1910718db8f1f594213072582be48b2c35ee3 100644 (file)
--- a/libthreads.cc
+++ b/libthreads.cc
@@ -27,7 +27,7 @@ int thrd_join(thrd_t t)
 /** A no-op, for now */
 void thrd_yield(void)
 {
 /** A no-op, for now */
 void thrd_yield(void)
 {

-       //model->switch_to_master(new ModelAction(THREAD_YIELD, std::memory_order_seq_cst, thread_current(), VALUE_NONE));
+       model->switch_to_master(new ModelAction(THREAD_YIELD, std::memory_order_seq_cst, thread_current(), VALUE_NONE));

 }
 
 thrd_t thrd_current(void)
 }
 
 thrd_t thrd_current(void)

diff --git a/main.cc b/main.cc
index b6e41523c0084d3699c5083c7c5ce4ca3cbb94e6..693e93c979244ed9061693be03df9f6029cda6d8 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -18,6 +18,7 @@ static void param_defaults(struct model_params *params)
        params->maxreads = 0;
        params->maxfuturedelay = 100;
        params->fairwindow = 0;
        params->maxreads = 0;
        params->maxfuturedelay = 100;
        params->fairwindow = 0;

+       params->yieldon = false;

        params->enabledcount = 1;
        params->bound = 0;
        params->maxfuturevalues = 0;
        params->enabledcount = 1;
        params->bound = 0;
        params->maxfuturevalues = 0;


@@ -46,17 +47,18 @@ static void print_usage(struct model_params *params)
 "-f                    Specify a fairness window in which actions that are\n"
 "                      enabled sufficiently many times should receive\n"
 "                      priority for execution. 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"

+"-y                    Turn on yield support. Default: %d\n"

 "-e                    Enabled count. Default: %d\n"
 "-b                    Upper length bound. Default: %d\n"
 "-v                    Print verbose execution information.\n"
 "--                    Program arguments follow.\n\n",
 "-e                    Enabled count. Default: %d\n"
 "-b                    Upper length bound. Default: %d\n"
 "-v                    Print verbose execution information.\n"
 "--                    Program arguments follow.\n\n",

-params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->enabledcount, params->bound);
+params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->enabledcount, params->bound);

        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:M:s:S:f:e:b:v";
+       const char *shortopts = "hym:M:s:S:f:e:b:v";

        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) {


@@ -88,6 +90,9 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                case 'v':
                        params->verbose = 1;
                        break;
                case 'v':
                        params->verbose = 1;
                        break;

+               case 'y':
+                       params->yieldon = true;
+                       break;

                default: /* '?' */
                        error = true;
                        break;
                default: /* '?' */
                        error = true;
                        break;

diff --git a/model.cc b/model.cc
index d15a094f7d8049e1a1e81ed8ac78527b6d1ca66a..8e513a3a47c972d70b0e9c3c6a9d72ba3e867171 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -822,6 +822,21 @@ void ModelChecker::set_backtracking(ModelAction *act)
                        if (unfair)
                                continue;
                }
                        if (unfair)
                                continue;
                }

+
+               /* See if CHESS-like yield fairness allows */
+               if (model->params.yieldon) {
+                       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_over(tid, tother)) {
+                                       unfair = true;
+                                       break;
+                               }
+                       }
+                       if (unfair)
+                               continue;
+               }
+               

                /* Cache the latest backtracking point */
                set_latest_backtrack(prev);
 
                /* Cache the latest backtracking point */
                set_latest_backtrack(prev);
 


@@ -1476,6 +1491,11 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 
        wake_up_sleeping_actions(curr);
 
 
        wake_up_sleeping_actions(curr);
 

+       /* Compute fairness information for CHESS yield algorithm */
+       if (model->params.yieldon) {
+               curr->get_node()->update_yield(scheduler);
+       }
+

        /* Add the action to lists before any other model-checking tasks */
        if (!second_part_of_rmw)
                add_action_to_lists(curr);
        /* Add the action to lists before any other model-checking tasks */
        if (!second_part_of_rmw)
                add_action_to_lists(curr);

diff --git a/model.h b/model.h
index c368ce6ef9cc7ca937cf78b580de1b5a80a6dd9d..71b8b7ac0b97b2dcf4990de667f2418f29c41d94 100644 (file)
--- a/model.h
+++ b/model.h
@@ -38,6 +38,7 @@ typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;
 struct model_params {
        int maxreads;
        int maxfuturedelay;
 struct model_params {
        int maxreads;
        int maxfuturedelay;

+       bool yieldon;

        unsigned int fairwindow;
        unsigned int enabledcount;
        unsigned int bound;
        unsigned int fairwindow;
        unsigned int enabledcount;
        unsigned int bound;

diff --git a/nodestack.cc b/nodestack.cc
index 8ffdc3358073d7be220e1ab27aa2019f83cfced1..dbc630739473bfa2fd0dbd44717ea2873c3c3bfd 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -45,7 +45,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
        relseq_break_writes(),
        relseq_break_index(0),
        misc_index(0),
        relseq_break_writes(),
        relseq_break_index(0),
        misc_index(0),

-       misc_max(0)
+       misc_max(0),
+       yield_data(NULL)

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


@@ -86,12 +87,63 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
        }
 }
 
        }
 }
 

+int Node::get_yield_data(int tid1, int tid2) const {
+       if (tid1<num_threads && tid2 < num_threads)
+               return yield_data[YIELD_INDEX(tid1,tid2,num_threads)];
+       else
+               return YIELD_S | YIELD_D;
+}
+
+void Node::update_yield(Scheduler * scheduler) {
+       yield_data=(int *) model_calloc(1, sizeof(int)*num_threads*num_threads);
+       //handle base case
+       if (parent == NULL) {
+               for(int i = 0; i < num_threads*num_threads; i++) {
+                       yield_data[i] = YIELD_S | YIELD_D;
+               }
+               return;
+       }
+       int curr_tid=id_to_int(action->get_tid());
+
+       for(int u = 0; u < num_threads; u++) {
+               for(int v = 0; v < num_threads; v++) {
+                       int yield_state=parent->get_yield_data(u, v);
+                       bool next_enabled=scheduler->is_enabled(int_to_id(v));
+                       bool curr_enabled=parent->is_enabled(int_to_id(v));
+                       if (!next_enabled) {
+                               //Compute intersection of ES and E
+                               yield_state&=~YIELD_E;
+                               //Check to see if we disabled the thread
+                               if (u==curr_tid && curr_enabled)
+                                       yield_state|=YIELD_D;
+                       }
+                       yield_data[YIELD_INDEX(u, v, num_threads)]=yield_state;
+               }
+               yield_data[YIELD_INDEX(u, curr_tid, num_threads)]=(yield_data[YIELD_INDEX(u, curr_tid, num_threads)]&~YIELD_P)|YIELD_S;
+       }
+       //handle curr.yield(t) part of computation
+       if (action->is_yield()) {
+               for(int v = 0; v < num_threads; v++) {
+                       int yield_state=yield_data[YIELD_INDEX(curr_tid, v, num_threads)];
+                       if ((yield_state & (YIELD_E | YIELD_D)) && (!(yield_state & YIELD_S)))
+                               yield_state |= YIELD_P;
+                       yield_state &= YIELD_P;
+                       if (scheduler->is_enabled(int_to_id(v))) {
+                               yield_state|=YIELD_E;
+                       }
+                       yield_data[YIELD_INDEX(curr_tid, v, num_threads)]=yield_state;
+               }
+       }
+}
+

 /** @brief Node desctructor */
 Node::~Node()
 {
        delete action;
        if (enabled_array)
                model_free(enabled_array);
 /** @brief Node desctructor */
 Node::~Node()
 {
        delete action;
        if (enabled_array)
                model_free(enabled_array);

+       if (yield_data)
+               model_free(yield_data);

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


@@ -324,6 +376,11 @@ bool Node::has_priority(thread_id_t tid) const
        return fairness[id_to_int(tid)].priority;
 }
 
        return fairness[id_to_int(tid)].priority;
 }
 

+bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const
+{
+       return get_yield_data(id_to_int(tid1), id_to_int(tid2)) & YIELD_P;
+}
+

 /*********************************** read from ********************************/
 
 /**
 /*********************************** read from ********************************/
 
 /**

diff --git a/nodestack.h b/nodestack.h
index 3cffac9c9b2219905020262302f4c580f9f03784..0a9422572eb0c4bd3ae6ce18b96757c57281a29f 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -29,6 +29,13 @@ typedef enum {
        READ_FROM_NONE,
 } read_from_type_t;
 
        READ_FROM_NONE,
 } read_from_type_t;
 

+#define YIELD_E 1
+#define YIELD_D 2
+#define YIELD_S 4
+#define YIELD_P 8
+#define YIELD_INDEX(tid1, tid2, num_threads) (tid1*num_threads+tid2)
+
+

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


@@ -58,6 +65,8 @@ public:
 
        ModelAction * get_action() const { return action; }
        bool has_priority(thread_id_t tid) const;
 
        ModelAction * get_action() const { return action; }
        bool has_priority(thread_id_t tid) const;

+       void update_yield(Scheduler *);
+       bool has_priority_over(thread_id_t tid, thread_id_t tid2) const;

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


@@ -105,7 +114,7 @@ public:
        MEMALLOC
 private:
        void explore(thread_id_t tid);
        MEMALLOC
 private:
        void explore(thread_id_t tid);

-
+       int get_yield_data(int tid1, int tid2) const;

        bool read_from_past_empty() const;
        bool increment_read_from_past();
        bool read_from_promise_empty() const;
        bool read_from_past_empty() const;
        bool increment_read_from_past();
        bool read_from_promise_empty() const;


@@ -144,6 +153,7 @@ private:
 
        int misc_index;
        int misc_max;
 
        int misc_index;
        int misc_max;

+       int * yield_data;

 };
 
 typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;
 };
 
 typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;

diff --git a/schedule.cc b/schedule.cc
index f65d1e99c2932c1893a9764d6f95c8b2f5faf80a..1eb57d7515823012c51026db219af0e6e9bf0a77 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -200,26 +200,42 @@ void Scheduler::wake(Thread *t)
 Thread * Scheduler::select_next_thread()
 {
        int old_curr_thread = curr_thread_index;
 Thread * Scheduler::select_next_thread()
 {
        int old_curr_thread = curr_thread_index;

-       bool have_enabled_thread_with_priority = false;

        Node *n = model->get_curr_node();
 
        Node *n = model->get_curr_node();
 

-       for (int i = 0; i < enabled_len; i++) {
-               thread_id_t tid = int_to_id(i);
-               if (n->has_priority(tid)) {
-                       DEBUG("Node (tid %d) has priority\n", i);
-                       if (enabled[i] != THREAD_DISABLED)
-                               have_enabled_thread_with_priority = true;
+       bool have_enabled_thread_with_priority = false;
+       if (model->params.fairwindow != 0) {
+               for (int i = 0; i < enabled_len; i++) {
+                       thread_id_t tid = int_to_id(i);
+                       if (n->has_priority(tid)) {
+                               DEBUG("Node (tid %d) has priority\n", i);
+                               if (enabled[i] != THREAD_DISABLED)
+                                       have_enabled_thread_with_priority = true;
+                       }

                }
                }

-       }
+       }       

 
        for (int i = 0; i < enabled_len; i++) {
                curr_thread_index = (old_curr_thread + i + 1) % enabled_len;
                thread_id_t curr_tid = int_to_id(curr_thread_index);
 
        for (int i = 0; i < enabled_len; i++) {
                curr_thread_index = (old_curr_thread + i + 1) % enabled_len;
                thread_id_t curr_tid = int_to_id(curr_thread_index);

+               if (model->params.yieldon) {
+                       bool bad_thread = false;
+                       for (int j = 0; j < enabled_len; j++) {
+                               thread_id_t tother = int_to_id(j);
+                               if ((enabled[j] != THREAD_DISABLED) && n->has_priority_over(curr_tid, tother)) {
+                                       bad_thread=true;
+                                       break;
+                               }
+                       }
+                       if (bad_thread)
+                               continue;
+               }
+               

                if (enabled[curr_thread_index] == THREAD_ENABLED &&
                                (!have_enabled_thread_with_priority || n->has_priority(curr_tid))) {
                        return model->get_thread(curr_tid);
                }
        }
                if (enabled[curr_thread_index] == THREAD_ENABLED &&
                                (!have_enabled_thread_with_priority || n->has_priority(curr_tid))) {
                        return model->get_thread(curr_tid);
                }
        }

+       

        /* No thread was enabled */
        return NULL;
 }
        /* No thread was enabled */
        return NULL;
 }

diff --git a/test/linuxrwlocksyield.c b/test/linuxrwlocksyield.c
new file mode 100644 (file)
index 0000000..9a676b0
--- /dev/null
+++ b/test/linuxrwlocksyield.c
@@ -0,0 +1,118 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "librace.h"
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       atomic_int lock;
+} rwlock_t;
+
+static inline int read_can_lock(rwlock_t *lock)
+{
+       return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
+}
+
+static inline int write_can_lock(rwlock_t *lock)
+{
+       return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
+}
+
+static inline void read_lock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+       while (priorvalue <= 0) {
+               atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+               do {
+                       priorvalue = atomic_load_explicit(&rw->lock, memory_order_relaxed);
+                       if (priorvalue > 0)
+                               break;
+                       thrd_yield();
+               } while (true);
+               priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+       }
+}
+
+static inline void write_lock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       while (priorvalue != RW_LOCK_BIAS) {
+               atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+               do {
+                       priorvalue = atomic_load_explicit(&rw->lock, memory_order_relaxed);
+                       if (priorvalue == RW_LOCK_BIAS)
+                               break;
+                       thrd_yield();
+               } while (true);
+               priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       }
+}
+
+static inline int read_trylock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+       if (priorvalue > 0)
+               return 1;
+
+       atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+       return 0;
+}
+
+static inline int write_trylock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       if (priorvalue == RW_LOCK_BIAS)
+               return 1;
+
+       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+       return 0;
+}
+
+static inline void read_unlock(rwlock_t *rw)
+{
+       atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
+}
+
+rwlock_t mylock;
+int shareddata;
+
+static void a(void *obj)
+{
+       int i;
+       for(i = 0; i < 2; i++) {
+               if ((i % 2) == 0) {
+                       read_lock(&mylock);
+                       load_32(&shareddata);
+                       read_unlock(&mylock);
+               } else {
+                       write_lock(&mylock);
+                       store_32(&shareddata,(unsigned int)i);
+                       write_unlock(&mylock);
+               }
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t t1, t2;
+       atomic_init(&mylock.lock, RW_LOCK_BIAS);
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+
+       return 0;
+}