be even more aggressive about sleep sets...

if an action was sleeping, it should only read from a value that could potentially result in synchronization with a release done while it was sleeping

diff --git a/action.cc b/action.cc
index c1adc2e7bc65cd94d26a4b7cf93ac3482c2b2d1a..b7bf024a4e79447220bfb50cd5268413e474f9b3 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -33,7 +33,8 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        reads_from(NULL),
        node(NULL),
        seq_number(ACTION_INITIAL_CLOCK),
-       cv(NULL)
+       cv(NULL),
+       sleep_flag(false)
 {
        Thread *t = thread ? thread : thread_current();
        this->tid = t->get_id();

diff --git a/action.h b/action.h
index 96b791ee50bb12695de577b21f75e8926347103b..68db2c35899c479b5aa1b0b9329f049a14b84e45 100644 (file)
--- a/action.h
+++ b/action.h
@@ -125,6 +125,9 @@ public:
        void process_rmw(ModelAction * act);
        void copy_typeandorder(ModelAction * act);
 
+       void set_sleep_flag() { sleep_flag=true; }
+       bool get_sleep_flag() { return sleep_flag; }
+
        MEMALLOC
 private:
 
@@ -155,6 +158,8 @@ private:
        /** The clock vector stored with this action; only needed if this
         * action is a store release? */
        ClockVector *cv;
+
+       bool sleep_flag;
 };
 
 typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;

diff --git a/model.cc b/model.cc
index d77ba4bdb7982b11757642d7ddb253703ecf7109..f8482cbf7b9db9eb9689a213c5de18cf3b583ad9 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -179,7 +179,6 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
                        tid = prevnode->get_next_backtrack();
                        /* Make sure the backtracked thread isn't sleeping. */
-                       scheduler->remove_sleep(thread_map->get(id_to_int(tid)));
                        node_stack->pop_restofstack(1);
                        if (diverge==earliest_diverge) {
                                earliest_diverge=prevnode->get_action();
@@ -213,6 +212,7 @@ void ModelChecker::execute_sleep_set() {
                        thr->set_state(THREAD_RUNNING);
                        scheduler->next_thread(thr);
                        Thread::swap(&system_context, thr);
+                       priv->current_action->set_sleep_flag();
                        thr->set_pending(priv->current_action);
                }
        }
@@ -346,7 +346,8 @@ void ModelChecker::set_backtracking(ModelAction *act)
        for(int i = low_tid; i < high_tid; i++) {
                thread_id_t tid = int_to_id(i);
 
-               if (!node->is_enabled(tid))
+               /* Don't backtrack into a point where the thread is disabled or sleeping. */
+               if (node->get_enabled_array()[i]!=THREAD_ENABLED)
                        continue;
        
                /* Check if this has been explored already */
@@ -1846,7 +1847,12 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                        act->print();
                                        curr->print();
                                }
-                               curr->get_node()->add_read_from(act);
+
+                               if (curr->get_sleep_flag()) {
+                                       if (sleep_can_read_from(curr, act))
+                                               curr->get_node()->add_read_from(act);
+                               } else
+                                       curr->get_node()->add_read_from(act);
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */
@@ -1873,6 +1879,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        ASSERT(initialized);
 }
 
+bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
+       while(true) {
+               Node *prevnode=write->get_node()->get_parent();
+               bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+               if (write->is_release()&&thread_sleep)
+                       return true;
+               if (!write->is_rmw())
+                       return false;
+               if (write->get_reads_from()==NULL)
+                       return true;
+               write=write->get_reads_from();
+       }
+}
+
 static void print_list(action_list_t *list)
 {
        action_list_t::iterator it;

diff --git a/model.h b/model.h
index 1bd32a1fffcb926449f2b5fc7a11f7d74410cf34..8316f04bd7aef32986f3d54f31dd1ca8afdca090 100644 (file)
--- a/model.h
+++ b/model.h
@@ -118,6 +118,7 @@ private:
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler *scheduler;
 
+       bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
        bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
        bool has_asserted() {return asserted;}
        void reset_asserted() {asserted=false;}