add sleep support

diff --git a/action.cc b/action.cc
index f00a14313ed6a3af079c4b771f41ca1dd32c30e4..30ac2c82643dadc328926f86bf346da20bdf498d 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -53,6 +53,36 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
 }
 
 
 }
 
 

+/**
+ * @brief Construct a new ModelAction
+ *
+ * @param type The type of action
+ * @param order The memory order of this action. A "don't care" for non-ATOMIC
+ * actions (e.g., THREAD_* or MODEL_* actions).
+ * @param loc The location that this action acts upon
+ * @param value (optional) A value associated with the action (e.g., the value
+ * read or written). Defaults to a given macro constant, for debugging purposes.
+ * @param thread (optional) The Thread in which this action occurred. If NULL
+ * (default), then a Thread is assigned according to the scheduler.
+ */
+ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value, uint64_t _time) :
+       location(NULL),
+       position(NULL),
+       time(_time),
+       last_fence_release(NULL),
+       uninitaction(NULL),
+       cv(NULL),
+       rf_cv(NULL),
+       value(value),
+       type(type),
+       order(order),
+       original_order(order),
+       seq_number(ACTION_INITIAL_CLOCK)
+{
+       Thread *t = thread_current();
+       this->tid = t!= NULL ? t->get_id() : -1;
+}
+

 /**
  * @brief Construct a new ModelAction
  *
 /**
  * @brief Construct a new ModelAction
  *


@@ -212,6 +242,11 @@ bool ModelAction::is_lock() const
        return type == ATOMIC_LOCK;
 }
 
        return type == ATOMIC_LOCK;
 }
 

+bool ModelAction::is_sleep() const
+{
+       return type == THREAD_SLEEP;
+}
+

 bool ModelAction::is_wait() const {
        return type == ATOMIC_WAIT;
 }
 bool ModelAction::is_wait() const {
        return type == ATOMIC_WAIT;
 }


@@ -645,6 +680,7 @@ const char * ModelAction::get_type_str() const
        case THREAD_YIELD: return "thread yield";
        case THREAD_JOIN: return "thread join";
        case THREAD_FINISH: return "thread finish";
        case THREAD_YIELD: return "thread yield";
        case THREAD_JOIN: return "thread join";
        case THREAD_FINISH: return "thread finish";

+       case THREAD_SLEEP: return "thread sleep";

        case THREADONLY_FINISH: return "pthread_exit finish";
 
        case PTHREAD_CREATE: return "pthread create";
        case THREADONLY_FINISH: return "pthread_exit finish";
 
        case PTHREAD_CREATE: return "pthread create";

diff --git a/action.h b/action.h
index d357066ad5850f2c61ac3115d4cebc1235658d04..00289355be9db60dd14c4cec2eace3381ac2e79a 100644 (file)
--- a/action.h
+++ b/action.h
@@ -55,6 +55,7 @@ typedef enum action_type {
        THREADONLY_FINISH,      // < A thread completion action
        PTHREAD_CREATE, // < A pthread creation action
        PTHREAD_JOIN,   // < A pthread join action
        THREADONLY_FINISH,      // < A thread completion action
        PTHREAD_CREATE, // < A pthread creation action
        PTHREAD_JOIN,   // < A pthread join action

+       THREAD_SLEEP,   // < A sleep operation

        ATOMIC_UNINIT,  // < Represents an uninitialized atomic
        NONATOMIC_WRITE,        // < Represents a non-atomic store
        ATOMIC_INIT,    // < Initialization of an atomic object (e.g., atomic_init())
        ATOMIC_UNINIT,  // < Represents an uninitialized atomic
        NONATOMIC_WRITE,        // < Represents a non-atomic store
        ATOMIC_INIT,    // < Initialization of an atomic object (e.g., atomic_init())


@@ -90,6 +91,7 @@ public:
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, int size);
        ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value, int size);
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, int size);
        ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value, int size);

+       ModelAction(action_type_t type, memory_order order, uint64_t value, uint64_t time);

        ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
        ~ModelAction();
        void print() const;
        ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
        ~ModelAction();
        void print() const;


@@ -107,6 +109,7 @@ public:
        uint64_t get_write_value() const;
        uint64_t get_return_value() const;
        ModelAction * get_reads_from() const { return reads_from; }
        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;}

        cdsc::mutex * get_mutex() const;
 
        void set_read_from(ModelAction *act);
        cdsc::mutex * get_mutex() const;
 
        void set_read_from(ModelAction *act);


@@ -124,6 +127,7 @@ public:
        bool is_thread_join() const;
        bool is_mutex_op() const;
        bool is_lock() const;
        bool is_thread_join() const;
        bool is_mutex_op() const;
        bool is_lock() const;

+       bool is_sleep() const;

        bool is_trylock() const;
        bool is_unlock() const;
        bool is_wait() const;
        bool is_trylock() const;
        bool is_unlock() const;
        bool is_wait() const;


@@ -200,6 +204,7 @@ private:
                 */
                ModelAction *reads_from;
                int size;
                 */
                ModelAction *reads_from;
                int size;

+               uint64_t time;  //used for sleep

        };
 
        /** @brief The last fence release from the same thread */
        };
 
        /** @brief The last fence release from the same thread */

diff --git a/execution.cc b/execution.cc
index 94be82acea20edd255f56fe6312702a89686df41..15c44072a8867881eae08dbc8e6830e1d92a432c 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -153,6 +153,11 @@ 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;
        }

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

        return false;
 }
 
        return false;
 }
 


@@ -650,6 +655,9 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
                if (!blocking->is_complete()) {
                        return false;
                }
                if (!blocking->is_complete()) {
                        return false;
                }

+       } else if (curr->is_sleep()) {
+               if (!fuzzer->shouldSleep(curr))
+                       return false;

        }
 
        return true;
        }
 
        return true;

diff --git a/fuzzer.cc b/fuzzer.cc
index 679b0af448d91dc7ae7863adc007addd99bf054e..5b5be9ff4441942fbfd22461d13b0c3788a9c7d6 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -2,6 +2,7 @@
 #include <stdlib.h>
 #include "threads-model.h"
 #include "model.h"
 #include <stdlib.h>
 #include "threads-model.h"
 #include "model.h"

+#include "action.h"

 
 int Fuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set) {
        int random_index = random() % rf_set->size();
 
 int Fuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set) {
        int random_index = random() % rf_set->size();


@@ -25,3 +26,15 @@ Thread * Fuzzer::selectNotify(action_list_t * waiters) {
        waiters->erase(it);
        return thread;
 }
        waiters->erase(it);
        return thread;
 }

+
+bool Fuzzer::shouldSleep(const ModelAction *sleep) {
+       return true;
+}
+
+bool Fuzzer::shouldWake(const ModelAction *sleep) {
+       struct timespec currtime;
+       clock_gettime(CLOCK_MONOTONIC, &currtime);
+       uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+
+       return ((sleep->get_time()+sleep->get_value()) >= lcurrtime);
+}

diff --git a/fuzzer.h b/fuzzer.h
index 572190e1b35bc4df9437836f96e62667a2dfdf5b..e794d225b70c15d5e8954ab9fed034e37f168d96 100644 (file)
--- a/fuzzer.h
+++ b/fuzzer.h
@@ -10,6 +10,8 @@ public:
        int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
        Thread * selectThread(int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);
        int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
        Thread * selectThread(int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);

+       bool shouldSleep(const ModelAction *sleep);
+       bool shouldWake(const ModelAction *sleep);

        MEMALLOC
 private:
 };
        MEMALLOC
 private:
 };

diff --git a/pthread.cc b/pthread.cc
index efe1033b0c4dbb5b7d203dc6d53092c996e8d556..71c60519d479365fba56a20646e1fdcab2afec28 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -13,6 +13,27 @@
 /* global "model" object */
 #include "model.h"
 #include "execution.h"
 /* global "model" object */
 #include "model.h"
 #include "execution.h"

+extern "C" {
+int nanosleep(const struct timespec *rqtp, struct timespec *rmtp);
+}
+
+int nanosleep(const struct timespec *rqtp, struct timespec *rmtp) {
+       if (model) {
+               uint64_t time = rqtp->tv_sec * 1000000000 + rqtp->tv_nsec;
+               struct timespec currtime;
+               clock_gettime(CLOCK_MONOTONIC, &currtime);
+               uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+               model->switch_to_master(new ModelAction(THREAD_SLEEP, std::memory_order_seq_cst, time, lcurrtime));
+               if (rmtp != NULL) {
+                       clock_gettime(CLOCK_MONOTONIC, &currtime);
+                       uint64_t lendtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+                       uint64_t elapsed = lendtime - lcurrtime;
+                       rmtp->tv_sec = elapsed / 1000000000;
+                       rmtp->tv_nsec = elapsed - rmtp->tv_sec * 1000000000;
+               }
+       }
+       return 0;
+}

 
 int pthread_create(pthread_t *t, const pthread_attr_t * attr,
                                                                         pthread_start_t start_routine, void * arg) {
 
 int pthread_create(pthread_t *t, const pthread_attr_t * attr,
                                                                         pthread_start_t start_routine, void * arg) {


@@ -191,7 +212,7 @@ int pthread_cond_timedwait(pthread_cond_t *p_cond,
                pthread_mutex_init(p_mutex, NULL);
 
        cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
                pthread_mutex_init(p_mutex, NULL);
 
        cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);

-       cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
+       //      cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);

 
        model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v));
 //     v->wait(*m);
 
        model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v));
 //     v->wait(*m);