add support for pthread_mutex
authorweiyu <weiyuluo1232@gmail.com>
Thu, 24 Jan 2019 21:31:35 +0000 (13:31 -0800)
committerweiyu <weiyuluo1232@gmail.com>
Thu, 24 Jan 2019 21:31:35 +0000 (13:31 -0800)
execution.cc
include/mutex
include/pthread.h [new file with mode: 0644]
model.cc
model.h
pthread.cc [new file with mode: 0644]

index fb72e81..887e2ef 100644 (file)
@@ -2719,7 +2719,7 @@ static void print_list(const action_list_t *list)
        action_list_t::const_iterator it;
 
        model_print("------------------------------------------------------------------------------------\n");
-       model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
+       model_print("#    t     Action type     MO       Location         Value               Rf  CV\n");
        model_print("------------------------------------------------------------------------------------\n");
 
        unsigned int hash = 0;
index bd65a78..734ec12 100644 (file)
@@ -13,6 +13,7 @@ namespace std {
                void *locked; /* Thread holding the lock */
                thread_id_t alloc_tid;
                modelclock_t alloc_clock;
+               int init; // WL
        };
 
        class mutex {
@@ -23,6 +24,8 @@ namespace std {
                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;
diff --git a/include/pthread.h b/include/pthread.h
new file mode 100644 (file)
index 0000000..0e05788
--- /dev/null
@@ -0,0 +1,29 @@
+/**
+ * @file pthread.h
+ * @brief C11 pthread.h interface header
+ */
+#ifndef PTHREAD_H
+#define PTHREAD_H 1
+
+#include <threads.h>
+
+typedef void *(*pthread_start_t)(void *);
+
+struct pthread_params {
+    pthread_start_t func;
+    void *arg;
+};
+
+int pthread_create(pthread_t *, const pthread_attr_t *,
+          void *(*start_routine) (void *), void * arg);
+void pthread_exit(void *);
+int pthread_join(pthread_t, void **);
+
+int pthread_mutex_init(pthread_mutex_t *, const pthread_mutexattr_t *);
+int pthread_mutex_lock(pthread_mutex_t *);
+int pthread_mutex_trylock(pthread_mutex_t *);
+int pthread_mutex_unlock(pthread_mutex_t *);
+
+int user_main(int, char**);
+
+#endif
index 9d147df..39f0c69 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -543,6 +543,7 @@ void ModelChecker::run()
 
                has_next = next_execution();
                pthread_map.clear();
+               mutex_map.clear();
                i++;
        } while (i<100); // while (has_next);
 
diff --git a/model.h b/model.h
index 1d032e1..7e65156 100644 (file)
--- a/model.h
+++ b/model.h
@@ -17,6 +17,7 @@
 #include "params.h"
 
 #include <map>
+#include <mutex>
 
 /* Forward declaration */
 class Node;
@@ -81,6 +82,7 @@ public:
        void set_inspect_plugin(TraceAnalysis *a) {     inspect_plugin=a;       }
        MEMALLOC
        std::map<pthread_t, ModelAction*> pthread_map;
+       std::map<pthread_mutex_t *, std::mutex*> mutex_map;
 private:
        /** Flag indicates whether to restart the model checker. */
        bool restart_flag;
diff --git a/pthread.cc b/pthread.cc
new file mode 100644 (file)
index 0000000..39c7cfb
--- /dev/null
@@ -0,0 +1,63 @@
+#include "common.h"
+#include "threads-model.h"
+#include "action.h"
+#include <pthread.h>
+#include <mutex>
+#include <vector>
+
+/* global "model" object */
+#include "model.h"
+
+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 };
+
+       ModelAction *act = new ModelAction(PTHREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params);
+       model->pthread_map[*t] = act;
+
+       /* seq_cst is just a 'don't care' parameter */
+       model->switch_to_master(act);
+
+       return 0;
+}
+
+int pthread_join(pthread_t t, void **value_ptr) {
+       ModelAction *act = model->pthread_map[t];
+       Thread *th = act->get_thread_operand();
+       model->switch_to_master(new ModelAction(PTHREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(th->get_id())));
+       return 0;
+}
+
+void pthread_exit(void *value_ptr) {
+       Thread * th = thread_current();
+       model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, th));
+}
+
+int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
+       if (model->mutex_map.find(p_mutex) != model->mutex_map.end() /*&& table[p_mutex]->is_initialized()*/ ) {
+               model_print("Reinitialize a lock\n");
+               // return 1;    // 0 means success; 1 means failure
+       }
+
+       std::mutex *m = new std::mutex();
+       m->initialize();
+       model->mutex_map[p_mutex] = m;
+       return 0;
+}
+
+int pthread_mutex_lock(pthread_mutex_t *p_mutex) {
+       std::mutex *m = model->mutex_map[p_mutex];
+       m->lock();
+       /* error message? */
+       return 0;
+}
+int pthread_mutex_trylock(pthread_mutex_t *p_mutex) {
+       std::mutex *m = model->mutex_map[p_mutex];
+       return m->try_lock();
+       /* error message?  */
+}
+int pthread_mutex_unlock(pthread_mutex_t *p_mutex) {   
+       std::mutex *m = model->mutex_map[p_mutex];
+        m->unlock();
+       return 0;
+}