From: weiyu Date: Tue, 28 May 2019 23:48:28 +0000 (-0700) Subject: change the namespace of mutex from std to cdsc X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=0229244d21ca78bf781e41684810e9fb6d5ca56c change the namespace of mutex from std to cdsc --- diff --git a/action.cc b/action.cc index eecf23ca..14160052 100644 --- a/action.cc +++ b/action.cc @@ -668,12 +668,12 @@ bool ModelAction::may_read_from(const Promise *promise) const * Only valid for LOCK, TRY_LOCK, UNLOCK, and WAIT operations. * @return The mutex operated on by this action, if any; otherwise NULL */ -std::mutex * ModelAction::get_mutex() const +cdsc::mutex * ModelAction::get_mutex() const { if (is_trylock() || is_lock() || is_unlock()) - return (std::mutex *)get_location(); + return (cdsc::mutex *)get_location(); else if (is_wait()) - return (std::mutex *)get_value(); + return (cdsc::mutex *)get_value(); else return NULL; } diff --git a/action.h b/action.h index 1b3ccfbd..8f44c7cb 100644 --- a/action.h +++ b/action.h @@ -18,7 +18,7 @@ class ClockVector; class Thread; class Promise; -namespace std { +namespace cdsc { class mutex; } @@ -111,7 +111,7 @@ public: uint64_t get_return_value() const; const ModelAction * get_reads_from() const { return reads_from; } Promise * get_reads_from_promise() const { return reads_from_promise; } - std::mutex * get_mutex() const; + cdsc::mutex * get_mutex() const; Node * get_node() const; void set_node(Node *n) { node = n; } diff --git a/conditionvariable.cc b/conditionvariable.cc index 75af879f..d5d0fc83 100644 --- a/conditionvariable.cc +++ b/conditionvariable.cc @@ -1,9 +1,9 @@ -#include +#include "mutex.h" #include "model.h" #include #include "action.h" -namespace std { +namespace cdsc { condition_variable::condition_variable() { diff --git a/execution.cc b/execution.cc index e21fc8aa..f6b59cd9 100644 --- a/execution.cc +++ b/execution.cc @@ -687,8 +687,8 @@ bool ModelExecution::process_read(ModelAction *curr) */ bool ModelExecution::process_mutex(ModelAction *curr) { - std::mutex *mutex = curr->get_mutex(); - struct std::mutex_state *state = NULL; + cdsc::mutex *mutex = curr->get_mutex(); + struct cdsc::mutex_state *state = NULL; if (mutex) state = mutex->get_state(); @@ -1248,8 +1248,8 @@ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *wai */ bool ModelExecution::check_action_enabled(ModelAction *curr) { if (curr->is_lock()) { - std::mutex *lock = curr->get_mutex(); - struct std::mutex_state *state = lock->get_state(); + cdsc::mutex *lock = curr->get_mutex(); + struct cdsc::mutex_state *state = lock->get_state(); if (state->locked) return false; } else if (curr->is_thread_join()) { diff --git a/execution.h b/execution.h index 090be717..fdc226b4 100644 --- a/execution.h +++ b/execution.h @@ -16,7 +16,7 @@ #include "stl-model.h" #include "params.h" -#include +#include "mutex.h" #include /* Forward declaration */ @@ -126,8 +126,8 @@ public: CycleGraph * const get_mo_graph() { return mo_graph; } - HashTable mutex_map; - HashTable cond_map; + HashTable mutex_map; + HashTable cond_map; SNAPSHOTALLOC private: @@ -220,7 +220,7 @@ private: HashTable *, uintptr_t, 4> obj_thrd_map; -// HashTable mutex_map; +// HashTable mutex_map; /** * @brief List of currently-pending promises diff --git a/include/atomic b/include/atomic deleted file mode 100644 index 5984e722..00000000 --- a/include/atomic +++ /dev/null @@ -1,11 +0,0 @@ -/** - * @file atomic - * @brief C++11 atomic interface header - */ - -#ifndef __CXX_ATOMIC__ -#define __CXX_ATOMIC__ - -#include "impatomic.h" - -#endif /* __CXX_ATOMIC__ */ diff --git a/include/atomic2 b/include/atomic2 new file mode 100644 index 00000000..5984e722 --- /dev/null +++ b/include/atomic2 @@ -0,0 +1,11 @@ +/** + * @file atomic + * @brief C++11 atomic interface header + */ + +#ifndef __CXX_ATOMIC__ +#define __CXX_ATOMIC__ + +#include "impatomic.h" + +#endif /* __CXX_ATOMIC__ */ diff --git a/include/condition_variable b/include/condition_variable index 2a7447b7..d6a70d47 100644 --- a/include/condition_variable +++ b/include/condition_variable @@ -1,7 +1,7 @@ #ifndef __CXX_CONDITION_VARIABLE__ #define __CXX_CONDITION_VARIABLE__ -namespace std { +namespace cdsc { class mutex; struct condition_variable_state { diff --git a/include/mutex b/include/mutex deleted file mode 100644 index 734ec124..00000000 --- a/include/mutex +++ /dev/null @@ -1,34 +0,0 @@ -/** - * @file mutex - * @brief C++11 mutex interface header - */ - -#ifndef __CXX_MUTEX__ -#define __CXX_MUTEX__ - -#include "modeltypes.h" - -namespace std { - struct mutex_state { - void *locked; /* Thread holding the lock */ - thread_id_t alloc_tid; - modelclock_t alloc_clock; - int init; // WL - }; - - class mutex { - public: - mutex(); - ~mutex() {} - void lock(); - bool try_lock(); - void unlock(); - struct mutex_state * get_state() {return &state;} - void initialize() { state.init = 1; } // WL - bool is_initialized() { return state.init == 1; } - - private: - struct mutex_state state; - }; -} -#endif /* __CXX_MUTEX__ */ diff --git a/include/mutex.h b/include/mutex.h new file mode 100644 index 00000000..e015ea59 --- /dev/null +++ b/include/mutex.h @@ -0,0 +1,35 @@ +/** + * @file mutex + * @brief C++11 mutex interface header + */ + +#ifndef __CXX_MUTEX__ +#define __CXX_MUTEX__ + +#include "modeltypes.h" +//#include + +namespace cdsc { + struct mutex_state { + void *locked; /* Thread holding the lock */ + thread_id_t alloc_tid; + modelclock_t alloc_clock; + int init; // WL + }; + + class mutex { + public: + mutex(); + ~mutex() {} + void lock(); + bool try_lock(); + void unlock(); + struct mutex_state * get_state() {return &state;} + void initialize() { state.init = 1; } // WL + bool is_initialized() { return state.init == 1; } + + private: + struct mutex_state state; + }; +} +#endif /* __CXX_MUTEX__ */ diff --git a/include/pthread.h b/include/pthread.h index 32f4e1b1..8e0a6908 100644 --- a/include/pthread.h +++ b/include/pthread.h @@ -10,6 +10,26 @@ #include #include +/* Mutex types. */ +enum +{ + PTHREAD_MUTEX_TIMED_NP, + PTHREAD_MUTEX_RECURSIVE_NP, + PTHREAD_MUTEX_ERRORCHECK_NP, + PTHREAD_MUTEX_ADAPTIVE_NP +#if defined __USE_UNIX98 || defined __USE_XOPEN2K8 + , + PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP, + PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP, + PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP, + PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL +#endif +#ifdef __USE_GNU + /* For compatibility. */ + , PTHREAD_MUTEX_FAST_NP = PTHREAD_MUTEX_TIMED_NP +#endif +}; + typedef void *(*pthread_start_t)(void *); struct pthread_params { @@ -38,6 +58,8 @@ int pthread_cond_timedwait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex, const struct timespec *abstime); int pthread_cond_signal(pthread_cond_t *); +void pthread_cleanup_push(void (*routine)(void*), void *arg ); + int user_main(int, char**); // --- not implemented yet --- diff --git a/mutex.cc b/mutex.cc index d5ec40ff..a431321e 100644 --- a/mutex.cc +++ b/mutex.cc @@ -1,4 +1,4 @@ -#include +#include "mutex.h" #include "model.h" #include "execution.h" @@ -6,7 +6,7 @@ #include "clockvector.h" #include "action.h" -namespace std { +namespace cdsc { mutex::mutex() { diff --git a/pthread.cc b/pthread.cc index 06e293de..3f642951 100644 --- a/pthread.cc +++ b/pthread.cc @@ -2,7 +2,11 @@ #include "threads-model.h" #include "action.h" #include "pthread.h" -#include + +#include "snapshot-interface.h" +#include "datarace.h" + +#include "mutex.h" #include #include @@ -10,6 +14,45 @@ #include "model.h" #include "execution.h" +static void param_defaults(struct model_params *params) +{ + params->maxreads = 0; + params->maxfuturedelay = 6; + params->fairwindow = 0; + params->yieldon = false; + params->yieldblock = false; + params->enabledcount = 1; + params->bound = 0; + params->maxfuturevalues = 0; + params->expireslop = 4; + params->verbose = !!DBG_ENABLED(); + params->uninitvalue = 0; + params->maxexecutions = 0; +} + +static void model_main() +{ + struct model_params params; + + param_defaults(¶ms); + + //parse_options(¶ms, main_argc, main_argv); + + //Initialize race detector + initRaceDetector(); + + snapshot_stack_init(); + + model = new ModelChecker(params); // L: Model thread is created +// install_trace_analyses(model->get_execution()); L: disable plugin + + snapshot_record(0); + model->run(); + delete model; + + DEBUG("Exiting\n"); +} + int pthread_create(pthread_t *t, const pthread_attr_t * attr, pthread_start_t start_routine, void * arg) { struct pthread_params params = { start_routine, arg }; @@ -43,7 +86,11 @@ void pthread_exit(void *value_ptr) { } int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { - std::mutex *m = new std::mutex(); + if (!model) { + snapshot_system_init(10000, 1024, 1024, 40000, &model_main); + } + + cdsc::mutex *m = new cdsc::mutex(); ModelExecution *execution = model->get_execution(); execution->mutex_map.put(p_mutex, m); @@ -52,28 +99,62 @@ int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { int pthread_mutex_lock(pthread_mutex_t *p_mutex) { ModelExecution *execution = model->get_execution(); - std::mutex *m = execution->mutex_map.get(p_mutex); - m->lock(); - /* error message? */ + + /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used + instead of pthread_mutex_init, or where *p_mutex is not stored + in the execution->mutex_map for some reason. */ + if (!execution->mutex_map.contains(p_mutex)) { + pthread_mutex_init(p_mutex, NULL); + } + + cdsc::mutex *m = execution->mutex_map.get(p_mutex); + + if (m != NULL) { + m->lock(); + } else { + printf("ah\n"); + } + return 0; } + int pthread_mutex_trylock(pthread_mutex_t *p_mutex) { ModelExecution *execution = model->get_execution(); - std::mutex *m = execution->mutex_map.get(p_mutex); + cdsc::mutex *m = execution->mutex_map.get(p_mutex); return m->try_lock(); } int pthread_mutex_unlock(pthread_mutex_t *p_mutex) { ModelExecution *execution = model->get_execution(); - std::mutex *m = execution->mutex_map.get(p_mutex); - m->unlock(); + cdsc::mutex *m = execution->mutex_map.get(p_mutex); + + if (m != NULL) { + m->unlock(); + } else { + printf("try to unlock an untracked pthread_mutex\n"); + } + return 0; } int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex, const struct timespec *__restrict abstime) { +// timedlock just gives the option of giving up the lock, so return and let the scheduler decide which thread goes next + +/* ModelExecution *execution = model->get_execution(); - std::mutex *m = execution->mutex_map.get(p_mutex); - m->lock(); + if (!execution->mutex_map.contains(p_mutex)) { + pthread_mutex_init(p_mutex, NULL); + } + cdsc::mutex *m = execution->mutex_map.get(p_mutex); + + if (m != NULL) { + m->lock(); + } else { + printf("something is wrong with pthread_mutex_timedlock\n"); + } + + printf("pthread_mutex_timedlock is called. It is currently implemented as a normal lock operation without no timeout\n"); +*/ return 0; } @@ -88,7 +169,7 @@ int pthread_key_delete(pthread_key_t) { } int pthread_cond_init(pthread_cond_t *p_cond, const pthread_condattr_t *attr) { - std::condition_variable *v = new std::condition_variable(); + cdsc::condition_variable *v = new cdsc::condition_variable(); ModelExecution *execution = model->get_execution(); execution->cond_map.put(p_cond, v); @@ -97,29 +178,54 @@ int pthread_cond_init(pthread_cond_t *p_cond, const pthread_condattr_t *attr) { int pthread_cond_wait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex) { ModelExecution *execution = model->get_execution(); - std::condition_variable *v = execution->cond_map.get(p_cond); - std::mutex *m = execution->mutex_map.get(p_mutex); + if ( !execution->cond_map.contains(p_cond) ) + pthread_cond_init(p_cond, NULL); + + cdsc::condition_variable *v = execution->cond_map.get(p_cond); + cdsc::mutex *m = execution->mutex_map.get(p_mutex); v->wait(*m); return 0; - } int pthread_cond_timedwait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex, const struct timespec *abstime) { +// implement cond_timedwait as a noop and let the scheduler decide which thread goes next ModelExecution *execution = model->get_execution(); - std::condition_variable *v = execution->cond_map.get(p_cond); - std::mutex *m = execution->mutex_map.get(p_mutex); - v->wait(*m); + if ( !execution->cond_map.contains(p_cond) ) + pthread_cond_init(p_cond, NULL); + if ( !execution->mutex_map.contains(p_mutex) ) + pthread_mutex_init(p_mutex, NULL); + + cdsc::condition_variable *v = execution->cond_map.get(p_cond); + cdsc::mutex *m = execution->mutex_map.get(p_mutex); + + model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v, NULL)); +// v->wait(*m); +// printf("timed_wait called\n"); return 0; } int pthread_cond_signal(pthread_cond_t *p_cond) { // notify only one blocked thread ModelExecution *execution = model->get_execution(); - std::condition_variable *v = execution->cond_map.get(p_cond); + if ( !execution->cond_map.contains(p_cond) ) + pthread_cond_init(p_cond, NULL); + + cdsc::condition_variable *v = execution->cond_map.get(p_cond); v->notify_one(); return 0; } + +void pthread_cleanup_push(void (*routine)(void*), void *arg ) { + printf("pthrea cleanup push called\n"); +} + +int pthread_once (pthread_once_t *__once_control, + void (*__init_routine)) { + printf("pthread once is called\n"); +} + + diff --git a/threads.cc b/threads.cc index 1a83283a..d1929cd7 100644 --- a/threads.cc +++ b/threads.cc @@ -5,7 +5,7 @@ #include #include -#include +#include "mutex.h" #include "common.h" #include "threads-model.h" #include "action.h"