add support for pthread_mutex

diff --git a/execution.cc b/execution.cc
index fb72e8186aab8ad1feaf7837fbff1194b89bef6f..887e2efa03df0f31832ff6ee260a1a8b1ed9794d 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -2719,7 +2719,7 @@ static void print_list(const action_list_t *list)
        action_list_t::const_iterator it;
 
        model_print("------------------------------------------------------------------------------------\n");
        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;
        model_print("------------------------------------------------------------------------------------\n");
 
        unsigned int hash = 0;

diff --git a/include/mutex b/include/mutex
index bd65a78a57647200dcc7e49a64dabcf3ffd41a4a..734ec124502a496c9871527deccacd30deaa3109 100644 (file)
--- a/include/mutex
+++ b/include/mutex
@@ -13,6 +13,7 @@ namespace std {
                void *locked; /* Thread holding the lock */
                thread_id_t alloc_tid;
                modelclock_t alloc_clock;
                void *locked; /* Thread holding the lock */
                thread_id_t alloc_tid;
                modelclock_t alloc_clock;

+               int init; // WL

        };
 
        class mutex {
        };
 
        class mutex {


@@ -23,6 +24,8 @@ namespace std {
                bool try_lock();
                void unlock();
                struct mutex_state * get_state() {return &state;}
                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;
                
        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
+++ b/include/pthread.h
@@ -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

diff --git a/model.cc b/model.cc
index 9d147dfcc92e95ddd2e12284cbb486cb0018f430..39f0c694e9b7e440ee5ffa952ded7b4b06f0a7ca 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -543,6 +543,7 @@ void ModelChecker::run()
 
                has_next = next_execution();
                pthread_map.clear();
 
                has_next = next_execution();
                pthread_map.clear();

+               mutex_map.clear();

                i++;
        } while (i<100); // while (has_next);
 
                i++;
        } while (i<100); // while (has_next);
 

diff --git a/model.h b/model.h
index 1d032e1b1e0727113f8167d6e0f09a84ed93fbc1..7e651561a79740af75910d2f7fd1251691644b49 100644 (file)
--- a/model.h
+++ b/model.h
@@ -17,6 +17,7 @@
 #include "params.h"
 
 #include <map>
 #include "params.h"
 
 #include <map>

+#include <mutex>

 
 /* Forward declaration */
 class Node;
 
 /* 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;
        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;
 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
+++ b/pthread.cc
@@ -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;
+}