Modified the implementation of usleep and make ModelExecution process "THREAD SLEEP...

diff --git a/action.h b/action.h
index a8233eb765184ceafb4837ae171c7826fe40d6b8..80ac1fda66eb1eec79ac70eaefe32b8764e8760f 100644 (file)
--- a/action.h
+++ b/action.h
@@ -53,9 +53,11 @@ typedef enum action_type {
        THREAD_JOIN,    // < A thread join action
        THREAD_FINISH,  // < A thread completion action
        THREADONLY_FINISH,      // < A thread completion action
+       THREAD_SLEEP,   // < A sleep operation
+
        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())
@@ -70,6 +72,7 @@ typedef enum action_type {
        ATOMIC_LOCK,    // < A lock action
        ATOMIC_TRYLOCK, // < A trylock action
        ATOMIC_UNLOCK,  // < An unlock action
+
        ATOMIC_NOTIFY_ONE,      // < A notify_one action
        ATOMIC_NOTIFY_ALL,      // < A notify all action
        ATOMIC_WAIT,    // < A wait action

diff --git a/execution.cc b/execution.cc
index 87dbe69eeeea320257cda85dc16b905665502529..870dcb1a9d06bd25614e4d872f6e6c9ae80045a4 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -174,9 +174,12 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
        for (unsigned int i = 0;i < get_num_threads();i++) {
                Thread *thr = get_thread(int_to_id(i));
                if (scheduler->is_sleep_set(thr)) {
-                       if (should_wake_up(curr, thr))
+                       if (should_wake_up(curr, thr)) {
                                /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);
+                               if (thr->get_pending()->is_sleep())
+                                       thr->set_pending(NULL);
+                       }
                }
        }
 }
@@ -565,6 +568,12 @@ void ModelExecution::process_thread_action(ModelAction *curr)
        case THREAD_START: {
                break;
        }
+       case THREAD_SLEEP: {
+               Thread *th = get_thread(curr);
+               th->set_pending(curr);
+               scheduler->add_sleep(th);
+               break;
+       }
        default:
                break;
        }
@@ -702,7 +711,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        wake_up_sleeping_actions(curr);
 
        /* Add uninitialized actions to lists */
-       if (!second_part_of_rmw && curr->get_type() != NOOP)
+       if (!second_part_of_rmw)
                add_uninit_action_to_lists(curr);
 
        SnapVector<ModelAction *> * rf_set = NULL;
@@ -711,15 +720,19 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                rf_set = build_may_read_from(curr);
 
        if (curr->is_read() && !second_part_of_rmw) {
-               bool success = process_read(curr, rf_set);
+               process_read(curr, rf_set);
+               delete rf_set;
+
+/*             bool success = process_read(curr, rf_set);
                delete rf_set;
                if (!success)
                        return curr;    // Do not add action to lists
+*/
        } else
                ASSERT(rf_set == NULL);
 
        /* Add the action to lists */
-       if (!second_part_of_rmw && curr->get_type() != NOOP)
+       if (!second_part_of_rmw)
                add_action_to_lists(curr);
 
        if (curr->is_write())

diff --git a/fuzzer.cc b/fuzzer.cc
index 5b5be9ff4441942fbfd22461d13b0c3788a9c7d6..12396dd9dec0e4e97231fbd5e2dcce82b73f8958 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -36,5 +36,5 @@ bool Fuzzer::shouldWake(const ModelAction *sleep) {
        clock_gettime(CLOCK_MONOTONIC, &currtime);
        uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
 
-       return ((sleep->get_time()+sleep->get_value()) >= lcurrtime);
+       return ((sleep->get_time()+sleep->get_value()) < lcurrtime);
 }

diff --git a/pthread.cc b/pthread.cc
index 715f6f6adf8332556a93e4759e03b98994448daf..d6067eb20fdafb70f04a8378150ba479f3465fd8 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -12,27 +12,7 @@
 /* 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;
-}
+#include <errno.h>
 
 int pthread_create(pthread_t *t, const pthread_attr_t * attr,
         pthread_start_t start_routine, void * arg) {
@@ -169,11 +149,10 @@ int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex,
 
        if (m != NULL) {
                m->lock();
-       } else {
-               return 1;
+               return 0;
        }
 
-       return 0;
+       return 1;
 }
 
 pthread_t pthread_self() {

diff --git a/sleeps.cc b/sleeps.cc
index 24e0eeaca56922d237e545a3101c07188a4e5944..0b4d32f65673285a75951d107aa2007e2c0d4356 100644 (file)
--- a/sleeps.cc
+++ b/sleeps.cc
@@ -4,6 +4,10 @@
 #include "action.h"
 #include "model.h"
 
+extern "C" {
+int nanosleep(const struct timespec *rqtp, struct timespec *rmtp);
+}
+
 unsigned int __sleep (unsigned int seconds)
 {
        model->switch_to_master(
@@ -19,8 +23,28 @@ unsigned int sleep(unsigned int seconds)
 
 int usleep (useconds_t useconds)
 {
-       model->switch_to_master(
-               new ModelAction(NOOP, std::memory_order_seq_cst, NULL)
-               );
+       struct timespec ts = {
+               .tv_sec = (long int) (useconds / 1000000),
+               .tv_nsec = (long int) (useconds % 1000000) * 1000l,
+       };
+       return nanosleep(&ts, NULL);
+}
+
+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;
 }