From e4b59e52989269c529e94bea1cd1b9dfe418a0ce Mon Sep 17 00:00:00 2001 From: weiyu Date: Thu, 24 Jan 2019 13:31:35 -0800 Subject: [PATCH] add support for pthread_mutex --- execution.cc | 2 +- include/mutex | 3 +++ include/pthread.h | 29 ++++++++++++++++++++++ model.cc | 1 + model.h | 2 ++ pthread.cc | 63 +++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 99 insertions(+), 1 deletion(-) create mode 100644 include/pthread.h create mode 100644 pthread.cc diff --git a/execution.cc b/execution.cc index fb72e818..887e2efa 100644 --- 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"); - 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; diff --git a/include/mutex b/include/mutex index bd65a78a..734ec124 100644 --- 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; + 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 index 00000000..0e05788e --- /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 + +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 9d147dfc..39f0c694 100644 --- 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 1d032e1b..7e651561 100644 --- a/model.h +++ b/model.h @@ -17,6 +17,7 @@ #include "params.h" #include +#include /* Forward declaration */ class Node; @@ -81,6 +82,7 @@ public: void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; } MEMALLOC std::map pthread_map; + std::map 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 index 00000000..39c7cfbd --- /dev/null +++ b/pthread.cc @@ -0,0 +1,63 @@ +#include "common.h" +#include "threads-model.h" +#include "action.h" +#include +#include +#include + +/* 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)¶ms); + 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; +} -- 2.34.1