From 74ac6c2fab9f394a9992431079ed2dbede1144c0 Mon Sep 17 00:00:00 2001 From: weiyu Date: Fri, 18 Oct 2019 15:26:41 -0700 Subject: [PATCH 1/1] Modified the implementation of usleep and make ModelExecution process "THREAD SLEEP" actions --- action.h | 5 ++++- execution.cc | 21 +++++++++++++++++---- fuzzer.cc | 2 +- pthread.cc | 27 +++------------------------ sleeps.cc | 30 +++++++++++++++++++++++++++--- 5 files changed, 52 insertions(+), 33 deletions(-) diff --git a/action.h b/action.h index a8233eb7..80ac1fda 100644 --- 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 87dbe69e..870dcb1a 100644 --- 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 * 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 5b5be9ff..12396dd9 100644 --- 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 715f6f6a..d6067eb2 100644 --- 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 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 24e0eeac..0b4d32f6 100644 --- 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; } -- 2.34.1