Do not allow a thread to stash the next pending action if its last action was a SLEEP...

diff --git a/execution.cc b/execution.cc
index e6203cb548861653ed600b83238f112f4e42d667..e7ca575d8165f01ac30393027de18e5b9b01e1e2 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -161,6 +161,7 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa
                if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
                        return true;
        }
                if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
                        return true;
        }

+       /* The sleep is literally sleeping */

        if (asleep->is_sleep()) {
                if (fuzzer->shouldWake(asleep))
                        return true;
        if (asleep->is_sleep()) {
                if (fuzzer->shouldWake(asleep))
                        return true;


@@ -178,7 +179,7 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
                                /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);
                                if (thr->get_pending()->is_sleep())
                                /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);
                                if (thr->get_pending()->is_sleep())

-                                       thr->set_pending(NULL);
+                                       thr->set_wakeup_state(true);

                        }
                }
        }
                        }
                }
        }


@@ -827,7 +828,8 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  * @return True if modification order edges were added; false otherwise
  */
 
  * @return True if modification order edges were added; false otherwise
  */
 

-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
+       SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)

 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;
 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;

diff --git a/model.cc b/model.cc
index 4c4b47ac4c12e466bbe4d03b687a9a3f5debf113..1e3dd2dee12b0c9071bf0e17e5e2ab273affd488 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -413,7 +413,7 @@ void ModelChecker::run()
                        for (unsigned int i = 0;i < get_num_threads();i++) {
                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);
                        for (unsigned int i = 0;i < get_num_threads();i++) {
                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);

-                               if (!thr->is_model_thread() && !thr->is_complete() && (!thr->get_pending())) {
+                               if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {

                                        switch_from_master(thr);
                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);
                                        switch_from_master(thr);
                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);


@@ -459,6 +459,11 @@ void ModelChecker::run()
                                t = get_next_thread();
                        if (!t || t->is_model_thread())
                                break;
                                t = get_next_thread();
                        if (!t || t->is_model_thread())
                                break;

+                       if (t->just_woken_up()) {
+                               t->set_wakeup_state(false);
+                               t->set_pending(NULL);
+                               continue;       // Allow this thread to stash the next pending action
+                       }

 
                        /* Consume the next action for a Thread */
                        ModelAction *curr = t->get_pending();
 
                        /* Consume the next action for a Thread */
                        ModelAction *curr = t->get_pending();

diff --git a/schedule.cc b/schedule.cc
index 4a9752a761ee105472e79543ec0fd89fbdd2f114..f68786a825698f64052729f5032b332a3925e824 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -108,7 +108,7 @@ bool Scheduler::is_sleep_set(const Thread *t) const
 /**
  * @brief Check if execution is stuck with no enabled threads and some sleeping
  * thread
 /**
  * @brief Check if execution is stuck with no enabled threads and some sleeping
  * thread

- * @return True if no threads are enabled an some thread is in the sleep set;
+ * @return True if no threads are enabled and some thread is in the sleep set;

  * false otherwise
  */
 bool Scheduler::all_threads_sleeping() const
  * false otherwise
  */
 bool Scheduler::all_threads_sleeping() const


@@ -202,16 +202,31 @@ void Scheduler::wake(Thread *t)
 Thread * Scheduler::select_next_thread()
 {
        int avail_threads = 0;
 Thread * Scheduler::select_next_thread()
 {
        int avail_threads = 0;

-       int thread_list[enabled_len];
-       for (int i = 0;i< enabled_len;i++) {
+       int sleep_threads = 0;
+       int thread_list[enabled_len], sleep_list[enabled_len];
+       Thread * thread;
+
+       for (int i = 0; i < enabled_len; i++) {

                if (enabled[i] == THREAD_ENABLED)
                        thread_list[avail_threads++] = i;
                if (enabled[i] == THREAD_ENABLED)
                        thread_list[avail_threads++] = i;

+               else if (enabled[i] == THREAD_SLEEP_SET)
+                       sleep_list[sleep_threads++] = i;

        }
 
        }
 

-       if (avail_threads == 0 && !execution->getFuzzer()->has_paused_threads())
-               return NULL;    // No threads available
+       if (avail_threads == 0 && !execution->getFuzzer()->has_paused_threads()) {
+               if (sleep_threads != 0) {
+                       // No threads available, but some threads sleeping. Wake up one of them
+                       thread = execution->getFuzzer()->selectThread(sleep_list, sleep_threads);
+                       remove_sleep(thread);
+                       thread->set_wakeup_state(true);
+               } else {
+                       return NULL;    // No threads available and no threads sleeping.
+               }
+       } else {
+               // Some threads are available
+               thread = execution->getFuzzer()->selectThread(thread_list, avail_threads);
+       }

 
 

-       Thread * thread = execution->getFuzzer()->selectThread(thread_list, avail_threads);

        curr_thread_index = id_to_int(thread->get_id());
        return thread;
 }
        curr_thread_index = id_to_int(thread->get_id());
        return thread;
 }

diff --git a/threads-model.h b/threads-model.h
index e2084abf5008e071bb4cd09e55b3d95a71b3a326..f2162a89e55752ffde61e74ebf3f0c675584d4ba 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -93,6 +93,9 @@ public:
         *  @see Thread::pending */
        void set_pending(ModelAction *act) { pending = act; }
 
         *  @see Thread::pending */
        void set_pending(ModelAction *act) { pending = act; }
 

+       bool just_woken_up() { return wakeup_state; }
+       void set_wakeup_state(bool state) { wakeup_state = state; }
+

        Thread * waiting_on() const;
        bool is_waiting_on(const Thread *t) const;
 
        Thread * waiting_on() const;
        bool is_waiting_on(const Thread *t) const;
 


@@ -144,6 +147,9 @@ private:
         */
        ModelAction *pending;
 
         */
        ModelAction *pending;
 

+       /** @brief True if this thread was just woken up */
+       bool wakeup_state;
+

        void (*start_routine)(void *);
        void *(*pstart_routine)(void *);
 
        void (*start_routine)(void *);
        void *(*pstart_routine)(void *);