Implement timedwait

diff --git a/action.cc b/action.cc
index 4cdca0d7a7272b2f4c6eef265ef34ca613bc0c3f..d8ce567039bfc451c13916aefc6d15b4b5211e38 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -251,6 +251,10 @@ bool ModelAction::is_wait() const {
        return type == ATOMIC_WAIT || type == ATOMIC_TIMEDWAIT;
 }
 
        return type == ATOMIC_WAIT || type == ATOMIC_TIMEDWAIT;
 }
 

+bool ModelAction::is_timedwait() const {
+       return type == ATOMIC_TIMEDWAIT;
+}
+

 bool ModelAction::is_notify() const {
        return type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
 }
 bool ModelAction::is_notify() const {
        return type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
 }

diff --git a/action.h b/action.h
index 6dea9bc0d61555c7ad017e00f30b4fcb9af58ad9..5357fe4b6501ca0025737c8c3f400b18e38cb6a7 100644 (file)
--- a/action.h
+++ b/action.h
@@ -140,6 +140,7 @@ public:
        bool is_trylock() const;
        bool is_unlock() const;
        bool is_wait() const;
        bool is_trylock() const;
        bool is_unlock() const;
        bool is_wait() const;

+       bool is_timedwait() const;

        bool is_create() const;
        bool is_notify() const;
        bool is_notify_one() const;
        bool is_create() const;
        bool is_notify() const;
        bool is_notify_one() const;

diff --git a/execution.cc b/execution.cc
index 4b8461e8f678c38302e6551f1ec56ecdc69d11ac..4953718d360499b85dfa8eed8bc6d8415bc1e33a 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -2,6 +2,7 @@
 #include <algorithm>
 #include <new>
 #include <stdarg.h>
 #include <algorithm>
 #include <new>
 #include <stdarg.h>

+#include <errno.h>

 
 #include "model.h"
 #include "execution.h"
 
 #include "model.h"
 #include "execution.h"


@@ -247,10 +248,8 @@ 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
  */
  * @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 Thread *thread) const
+bool ModelExecution::should_wake_up(const ModelAction * asleep) const

 {
 {

-       const ModelAction *asleep = thread->get_pending();
-

        /* The sleep is literally sleeping */
        switch (asleep->get_type()) {
                case THREAD_SLEEP:
        /* The sleep is literally sleeping */
        switch (asleep->get_type()) {
                case THREAD_SLEEP:


@@ -275,14 +274,16 @@ void ModelExecution::wake_up_sleeping_actions()
                thread_id_t tid = int_to_id(i);
                if (scheduler->is_sleep_set(tid)) {
                        Thread *thr = get_thread(tid);
                thread_id_t tid = int_to_id(i);
                if (scheduler->is_sleep_set(tid)) {
                        Thread *thr = get_thread(tid);

-                       if (should_wake_up(thr)) {
+                       ModelAction * pending = thr->get_pending();
+                       if (should_wake_up(pending)) {

                                /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);
                                /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);

-                               ModelAction * pending = thr->get_pending();
+

                                if (pending->is_sleep()) {
                                        thr->set_wakeup_state(true);
                                } else if (pending->is_wait()) {
                                        thr->set_wakeup_state(true);
                                if (pending->is_sleep()) {
                                        thr->set_wakeup_state(true);
                                } else if (pending->is_wait()) {
                                        thr->set_wakeup_state(true);

+                                       /* Remove this thread from list of waiters */

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


@@ -290,6 +291,10 @@ void ModelExecution::wake_up_sleeping_actions()
                                                        break;
                                                }
                                        }
                                                        break;
                                                }
                                        }

+
+                                       /* Set ETIMEDOUT error */
+                                       if (pending->is_timedwait())
+                                               thr->set_return_value(ETIMEDOUT);

                                }
                        }
                }
                                }
                        }
                }


@@ -507,24 +512,38 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                waiters->push_back(curr);
                curr_thrd->set_pending(curr);   // Forbid this thread to stash a new action
 
                waiters->push_back(curr);
                curr_thrd->set_pending(curr);   // Forbid this thread to stash a new action
 

-               if (fuzzer->waitShouldFail(curr))
-                       scheduler->add_sleep(curr_thrd);        // Place this thread into THREAD_SLEEP_SET
+               if (fuzzer->waitShouldFail(curr))               // If wait should fail spuriously,
+                       scheduler->add_sleep(curr_thrd);        // place this thread into THREAD_SLEEP_SET

                else
                        scheduler->sleep(curr_thrd);
 
                break;
        }
                else
                        scheduler->sleep(curr_thrd);
 
                break;
        }

-       case ATOMIC_TIMEDWAIT:
-       case ATOMIC_UNLOCK: {
-               //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
-               //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
-               //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
-               //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
-               //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
-               //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
-               //FAILS AND IN THE CASE IT DOESN'T...  TIMED WAITS
-               //MUST EVENMTUALLY RELEASE...
+       case ATOMIC_TIMEDWAIT: {
+               Thread *curr_thrd = get_thread(curr);
+               if (!fuzzer->randomizeWaitTime(curr)) {
+                       curr_thrd->set_return_value(ETIMEDOUT);
+                       return false;
+               }

 
 

+               /* 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;
+
+               /* 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
+               scheduler->add_sleep(curr_thrd);
+               break;
+       }
+       case ATOMIC_UNLOCK: {

                // TODO: lock count for recursive mutexes
                /* wake up the other threads */
                Thread *curr_thrd = get_thread(curr);
                // TODO: lock count for recursive mutexes
                /* wake up the other threads */
                Thread *curr_thrd = get_thread(curr);

diff --git a/execution.h b/execution.h
index 51062eae7d7a2be04511f963198834ca3c02e6b6..82d629ce31a808b2cb07353d914e1ae4ecd42c91 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -99,7 +99,7 @@ public:
        SNAPSHOTALLOC
 private:
        int get_execution_number() const;
        SNAPSHOTALLOC
 private:
        int get_execution_number() const;

-       bool should_wake_up(const Thread *thread) const;
+       bool should_wake_up(const ModelAction * asleep) const;

        void wake_up_sleeping_actions();
        modelclock_t get_next_seq_num();
        bool next_execution();
        void wake_up_sleeping_actions();
        modelclock_t get_next_seq_num();
        bool next_execution();

diff --git a/fuzzer.cc b/fuzzer.cc
index f3be1d3ff3cd1630398cb3671ce8f5ba241fc8f3..7e488ce85fe84dbf6126b81b90aa9c48f8bf2c6f 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -58,10 +58,28 @@ bool Fuzzer::waitShouldFail(ModelAction * wait)
 
 bool Fuzzer::waitShouldWakeUp(const ModelAction * wait)
 {
 
 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;
 
        struct timespec currtime;
        clock_gettime(CLOCK_MONOTONIC, &currtime);
        uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
 

-       return (time_to_expire < lcurrtime);
+       return (wait->get_time() < lcurrtime);
+}
+
+bool Fuzzer::randomizeWaitTime(ModelAction * timed_wait)
+{
+       uint64_t abstime = timed_wait->get_time();
+       struct timespec currtime;
+       clock_gettime(CLOCK_MONOTONIC, &currtime);
+       uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+       if (abstime <= lcurrtime)
+               return false;
+
+       // Shorten wait time
+       if ((random() & 1) == 0) {
+               uint64_t tmp = abstime - lcurrtime;
+               uint64_t time_to_expire = random() % tmp + lcurrtime;
+               timed_wait->set_time(time_to_expire);
+       }
+
+       return true;

 }
 }

diff --git a/fuzzer.h b/fuzzer.h
index e3cd445b789a1288ffb040613096c39b1c688448..65210e09ae8e147693d3b5300e4c5db3ff766cc6 100644 (file)
--- a/fuzzer.h
+++ b/fuzzer.h
@@ -17,6 +17,7 @@ public:
        bool shouldWake(const ModelAction *sleep);
        virtual bool waitShouldFail(ModelAction *wait);
        bool waitShouldWakeUp(const ModelAction *wait);
        bool shouldWake(const ModelAction *sleep);
        virtual bool waitShouldFail(ModelAction *wait);
        bool waitShouldWakeUp(const ModelAction *wait);

+       bool randomizeWaitTime(ModelAction * timed_wait);

        virtual void register_engine(ModelChecker * _model, ModelExecution * execution) {}
        SNAPSHOTALLOC
 private:
        virtual void register_engine(ModelChecker * _model, ModelExecution * execution) {}
        SNAPSHOTALLOC
 private:

diff --git a/model.cc b/model.cc
index 2aa31e9b596d9e46f5b147536134e3648bc9d498..4b2143dc36ab4e303840059dd9ed1f7f22cd2c43 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -385,7 +385,7 @@ Thread* ModelChecker::getNextThread(Thread *old)
                }
 
                ModelAction *act = thr->get_pending();
                }
 
                ModelAction *act = thr->get_pending();

-               if (act && execution->is_enabled(tid)){
+               if (act && scheduler->is_enabled(tid)){

                        /* Don't schedule threads which should be disabled */
                        if (!execution->check_action_enabled(act)) {
                                scheduler->sleep(thr);
                        /* Don't schedule threads which should be disabled */
                        if (!execution->check_action_enabled(act)) {
                                scheduler->sleep(thr);

diff --git a/pthread.cc b/pthread.cc
index 20999aea4899c61f6fb20e0f6707d29e16737dde..fecca66b738be3527a65bb2387f99c05f058d822 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -174,7 +174,6 @@ int pthread_cond_wait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex) {
 int pthread_cond_timedwait(pthread_cond_t *p_cond,
                                                                                                         pthread_mutex_t *p_mutex, const struct timespec *abstime) {
        ModelExecution *execution = model->get_execution();
 int pthread_cond_timedwait(pthread_cond_t *p_cond,
                                                                                                         pthread_mutex_t *p_mutex, const struct timespec *abstime) {
        ModelExecution *execution = model->get_execution();

-

        if ( !execution->getCondMap()->contains(p_cond) )
                pthread_cond_init(p_cond, NULL);
        if ( !execution->getMutexMap()->contains(p_mutex) )
        if ( !execution->getCondMap()->contains(p_cond) )
                pthread_cond_init(p_cond, NULL);
        if ( !execution->getMutexMap()->contains(p_mutex) )


@@ -183,10 +182,14 @@ int pthread_cond_timedwait(pthread_cond_t *p_cond,
        cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
        cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
 
        cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
        cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
 

-       model->switch_thread(new ModelAction(ATOMIC_TIMEDWAIT, std::memory_order_seq_cst, v, (uint64_t) m));
+       uint64_t time = abstime->tv_sec * 1000000000 + abstime->tv_nsec;
+       ModelAction * timed_wait = new ModelAction(ATOMIC_TIMEDWAIT, std::memory_order_seq_cst, v, (uint64_t) m);
+       timed_wait->set_time(time);
+       if (model->switch_thread(timed_wait) == ETIMEDOUT) {
+               //model_print("thread %u wait timedout\n", thread_current_id());
+               return ETIMEDOUT;
+       }

        m->lock();
        m->lock();

-
-       // model_print("Timed_wait is called\n");

        return 0;
 }
 
        return 0;
 }