change the namespace of mutex from std to cdsc
authorweiyu <weiyuluo1232@gmail.com>
Tue, 28 May 2019 23:48:28 +0000 (16:48 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Tue, 28 May 2019 23:48:28 +0000 (16:48 -0700)
14 files changed:
action.cc
action.h
conditionvariable.cc
execution.cc
execution.h
include/atomic [deleted file]
include/atomic2 [new file with mode: 0644]
include/condition_variable
include/mutex [deleted file]
include/mutex.h [new file with mode: 0644]
include/pthread.h
mutex.cc
pthread.cc
threads.cc

index eecf23c..1416005 100644 (file)
--- 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;
 }
index 1b3ccfb..8f44c7c 100644 (file)
--- 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; }
index 75af879..d5d0fc8 100644 (file)
@@ -1,9 +1,9 @@
-#include <mutex>
+#include "mutex.h"
 #include "model.h"
 #include <condition_variable>
 #include "action.h"
 
-namespace std {
+namespace cdsc {
 
 condition_variable::condition_variable() {
                
index e21fc8a..f6b59cd 100644 (file)
@@ -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()) {
index 090be71..fdc226b 100644 (file)
@@ -16,7 +16,7 @@
 #include "stl-model.h"
 #include "params.h"
 
-#include <mutex>
+#include "mutex.h"
 #include <condition_variable>
 
 /* Forward declaration */
@@ -126,8 +126,8 @@ public:
 
        CycleGraph * const get_mo_graph() { return mo_graph; }
 
-       HashTable<pthread_mutex_t *, std::mutex *, uintptr_t, 4> mutex_map;
-       HashTable<pthread_cond_t *, std::condition_variable *, uintptr_t, 4> cond_map;
+       HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
+       HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> cond_map;
 
        SNAPSHOTALLOC
 private:
@@ -220,7 +220,7 @@ private:
 
        HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
 
-//     HashTable<pthread_mutex_t *, std::mutex *, uintptr_t, 4> mutex_map;
+//     HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
 
        /**
         * @brief List of currently-pending promises
diff --git a/include/atomic b/include/atomic
deleted file mode 100644 (file)
index 5984e72..0000000
+++ /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 (file)
index 0000000..5984e72
--- /dev/null
@@ -0,0 +1,11 @@
+/**
+ * @file atomic
+ * @brief C++11 atomic interface header
+ */
+
+#ifndef __CXX_ATOMIC__
+#define __CXX_ATOMIC__
+
+#include "impatomic.h"
+
+#endif /* __CXX_ATOMIC__ */
index 2a7447b..d6a70d4 100644 (file)
@@ -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 (file)
index 734ec12..0000000
+++ /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 (file)
index 0000000..e015ea5
--- /dev/null
@@ -0,0 +1,35 @@
+/**
+ * @file mutex
+ * @brief C++11 mutex interface header
+ */
+
+#ifndef __CXX_MUTEX__
+#define __CXX_MUTEX__
+
+#include "modeltypes.h"
+//#include <mutex>
+
+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__ */
index 32f4e1b..8e0a690 100644 (file)
 #include <bits/pthreadtypes.h>
 #include <pthread.h>
 
+/* 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 ---
index d5ec40f..a431321 100644 (file)
--- a/mutex.cc
+++ b/mutex.cc
@@ -1,4 +1,4 @@
-#include <mutex>
+#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()
 {
index 06e293d..3f64295 100644 (file)
@@ -2,7 +2,11 @@
 #include "threads-model.h"
 #include "action.h"
 #include "pthread.h"
-#include <mutex>
+
+#include "snapshot-interface.h"
+#include "datarace.h"
+
+#include "mutex.h"
 #include <condition_variable>
 #include <assert.h>
 
 #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(&params);
+
+        //parse_options(&params, 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");
+}
+
+
index 1a83283..d1929cd 100644 (file)
@@ -5,7 +5,7 @@
 #include <string.h>
 
 #include <threads.h>
-#include <mutex>
+#include "mutex.h"
 #include "common.h"
 #include "threads-model.h"
 #include "action.h"