Implement spurious wakeup for ATOMIC_WAIT

diff --git a/action.h b/action.h
index fbf566fb7a8f61497284c6ab1e826dd39b0f44e0..6dea9bc0d61555c7ad017e00f30b4fcb9af58ad9 100644 (file)
--- a/action.h
+++ b/action.h
@@ -116,7 +116,8 @@ public:
        uint64_t get_write_value() const;
        uint64_t get_return_value() const;
        ModelAction * get_reads_from() const { return reads_from; }
-       uint64_t get_time() const {return time;}
+       uint64_t get_time() const { return time; }
+       void set_time(uint64_t _time) { time = _time; }
        cdsc::mutex * get_mutex() const;
 
        void set_read_from(ModelAction *act);

diff --git a/execution.cc b/execution.cc
index 8f459d172bd9a1cd8caebd3e5908be856bd889ec..4b8461e8f678c38302e6551f1ec56ecdc69d11ac 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -247,30 +247,50 @@ void ModelExecution::restore_last_seq_num()
  * @param thread The thread that we might wake up
  * @return True, if we should wake up the sleeping thread; false otherwise
  */
-bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
+bool ModelExecution::should_wake_up(const Thread *thread) const
 {
        const ModelAction *asleep = thread->get_pending();
 
        /* The sleep is literally sleeping */
-       if (asleep->is_sleep()) {
-               if (fuzzer->shouldWake(asleep))
-                       return true;
+       switch (asleep->get_type()) {
+               case THREAD_SLEEP:
+                       if (fuzzer->shouldWake(asleep))
+                               return true;
+                       break;
+               case ATOMIC_WAIT:
+               case ATOMIC_TIMEDWAIT:
+                       if (fuzzer->waitShouldWakeUp(asleep))
+                               return true;
+                       break;
+               default:
+                       return false;
        }
 
        return false;
 }
 
-void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
+void ModelExecution::wake_up_sleeping_actions()
 {
        for (unsigned int i = 0;i < get_num_threads();i++) {
                thread_id_t tid = int_to_id(i);
                if (scheduler->is_sleep_set(tid)) {
                        Thread *thr = get_thread(tid);
-                       if (should_wake_up(curr, thr)) {
+                       if (should_wake_up(thr)) {
                                /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);
-                               if (thr->get_pending()->is_sleep())
+                               ModelAction * pending = thr->get_pending();
+                               if (pending->is_sleep()) {
+                                       thr->set_wakeup_state(true);
+                               } else if (pending->is_wait()) {
                                        thr->set_wakeup_state(true);
+                                       simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, pending->get_location());
+                                       for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
+                                               if (rit->getVal()->get_tid() == tid) {
+                                                       waiters->erase(rit);
+                                                       break;
+                                               }
+                                       }
+                               }
                        }
                }
        }
@@ -471,32 +491,26 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                break;
        }
        case ATOMIC_WAIT: {
-               //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
-               if (fuzzer->shouldWait(curr)) {
-                       Thread *curr_thrd = get_thread(curr);
-                       /* wake up the other threads */
-                       for (unsigned int i = 0;i < get_num_threads();i++) {
-                               Thread *t = get_thread(int_to_id(i));
-                               if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
-                                       scheduler->wake(t);
-                       }
+               Thread *curr_thrd = get_thread(curr);
+               /* wake up the other threads */
+               for (unsigned int i = 0;i < get_num_threads();i++) {
+                       Thread *t = get_thread(int_to_id(i));
+                       if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+                               scheduler->wake(t);
+               }
 
-                       /* unlock the lock - after checking who was waiting on it */
-                       state->locked = NULL;
+               /* unlock the lock - after checking who was waiting on it */
+               state->locked = NULL;
 
-                       /* remove old wait action and disable this thread */
-                       simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
-                       for (sllnode<ModelAction *> * it = waiters->begin();it != NULL;it = it->getNext()) {
-                               ModelAction * wait = it->getVal();
-                               if (wait->get_tid() == curr->get_tid()) {
-                                       waiters->erase(it);
-                                       break;
-                               }
-                       }
+               /* disable this thread */
+               simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+               waiters->push_back(curr);
+               curr_thrd->set_pending(curr);   // Forbid this thread to stash a new action
 
-                       waiters->push_back(curr);
+               if (fuzzer->waitShouldFail(curr))
+                       scheduler->add_sleep(curr_thrd);        // Place this thread into THREAD_SLEEP_SET
+               else
                        scheduler->sleep(curr_thrd);
-               }
 
                break;
        }
@@ -528,7 +542,10 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                //activate all the waiting threads
                for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
-                       scheduler->wake(get_thread(rit->getVal()));
+                       Thread * thread = get_thread(rit->getVal());
+                       if (thread->get_state() != THREAD_COMPLETED)
+                               scheduler->wake(thread);
+                       thread->set_wakeup_state(true);
                }
                waiters->clear();
                break;
@@ -537,7 +554,9 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                if (waiters->size() != 0) {
                        Thread * thread = fuzzer->selectNotify(waiters);
-                       scheduler->wake(thread);
+                       if (thread->get_state() != THREAD_COMPLETED)
+                               scheduler->wake(thread);
+                       thread->set_wakeup_state(true);
                }
                break;
        }
@@ -809,7 +828,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 
        DBG();
 
-       wake_up_sleeping_actions(curr);
+       wake_up_sleeping_actions();
 
        SnapVector<ModelAction *> * rf_set = NULL;
        bool canprune = false;

diff --git a/execution.h b/execution.h
index 31e9810ef40149fdd2003cc6fd78744cf9675b14..51062eae7d7a2be04511f963198834ca3c02e6b6 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -99,8 +99,8 @@ public:
        SNAPSHOTALLOC
 private:
        int get_execution_number() const;
-       bool should_wake_up(const ModelAction *curr, const Thread *thread) const;
-       void wake_up_sleeping_actions(ModelAction *curr);
+       bool should_wake_up(const Thread *thread) const;
+       void wake_up_sleeping_actions();
        modelclock_t get_next_seq_num();
        bool next_execution();
        bool initialize_curr_action(ModelAction **curr);

diff --git a/fuzzer.cc b/fuzzer.cc
index e102d9c34431a13dea089d9437857640e2691cfd..f3be1d3ff3cd1630398cb3671ce8f5ba241fc8f3 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -39,7 +39,29 @@ bool Fuzzer::shouldWake(const ModelAction *sleep) {
        return ((sleep->get_time()+sleep->get_value()) < lcurrtime);
 }
 
-bool Fuzzer::shouldWait(const ModelAction * act)
+/* Decide whether wait should spuriously fail or not */
+bool Fuzzer::waitShouldFail(ModelAction * wait)
 {
-       return true;
+       if ((random() & 1) == 0) {
+               struct timespec currtime;
+        clock_gettime(CLOCK_MONOTONIC, &currtime);
+        uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+
+               // The time after which wait fail spuriously, in nanoseconds
+               uint64_t time = random() % 1000000;
+               wait->set_time(time + lcurrtime);
+               return true;
+       }
+
+       return false;
+}
+
+bool Fuzzer::waitShouldWakeUp(const ModelAction * wait)
+{
+       uint64_t time_to_expire = wait->get_time();
+       struct timespec currtime;
+       clock_gettime(CLOCK_MONOTONIC, &currtime);
+       uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+
+       return (time_to_expire < lcurrtime);
 }

diff --git a/fuzzer.h b/fuzzer.h
index 0fcfb51f67e66ff9ee439f9b48c1bd860838cbfa..e3cd445b789a1288ffb040613096c39b1c688448 100644 (file)
--- a/fuzzer.h
+++ b/fuzzer.h
@@ -15,7 +15,8 @@ public:
        Thread * selectNotify(simple_action_list_t * waiters);
        bool shouldSleep(const ModelAction *sleep);
        bool shouldWake(const ModelAction *sleep);
-       virtual bool shouldWait(const ModelAction *wait);
+       virtual bool waitShouldFail(ModelAction *wait);
+       bool waitShouldWakeUp(const ModelAction *wait);
        virtual void register_engine(ModelChecker * _model, ModelExecution * execution) {}
        SNAPSHOTALLOC
 private:

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 7d4e8b1810880f600393e76f5618af8dc2b9516b..76f4e4ceaec8a967ebb52ad54bba996268065588 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -444,8 +444,3 @@ bool NewFuzzer::find_threads(ModelAction * pending_read)
 
        return finds_waiting_for;
 }
-
-bool NewFuzzer::shouldWait(const ModelAction * act)
-{
-       return true;
-}

diff --git a/newfuzzer.h b/newfuzzer.h
index 26fab3f6c2fff4e0ed995e4d68a8dd7733ecb5f5..67454ffc268198c96b13360c23df9a0da0939990 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -32,7 +32,6 @@ public:
        Thread * selectNotify(simple_action_list_t * waiters);
        bool shouldSleep(const ModelAction * sleep);
        bool shouldWake(const ModelAction * sleep);
-       bool shouldWait(const ModelAction * wait);
 
        void register_engine(ModelChecker * model, ModelExecution * execution);
        Predicate * get_selected_child_branch(thread_id_t tid);

diff --git a/schedule.cc b/schedule.cc
index 30af582dcc237991b690f606eb0c1e5ca11afa1b..f55c7b0deed28d98cc89530fb8c88a32fc99c1e4 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -98,7 +98,6 @@ bool Scheduler::is_enabled(thread_id_t tid) const
 /**
  * @brief Check if a Thread is currently in the sleep set
  * @param t The Thread to check
- * @return True if the Thread is currently enabled
  */
 bool Scheduler::is_sleep_set(const Thread *t) const
 {
@@ -139,6 +138,8 @@ enabled_type_t Scheduler::get_enabled(const Thread *t) const
 /**
  * Add a Thread to the sleep set.
  * @param t The Thread to add
+ * A Thread is in THREAD_SLEEP_SET if it is sleeping or blocked by a wait
+ * operation that should fail spuriously (decide by fuzzer).
  */
 void Scheduler::add_sleep(Thread *t)
 {