From: weiyu Date: Fri, 15 Feb 2019 01:42:08 +0000 (-0800) Subject: move pthread_map and mutex_map inside of execution.h X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=6b12232a5e3db3bc7f4cbcfa772ba86f1de04cc9 move pthread_map and mutex_map inside of execution.h --- diff --git a/action.cc b/action.cc index 359316d1..eecf23ca 100644 --- a/action.cc +++ b/action.cc @@ -285,6 +285,8 @@ Thread * ModelAction::get_thread_operand() const /* THREAD_JOIN uses (Thread *) for location */ return (Thread *)get_location(); } else if (type == PTHREAD_JOIN) { + // return NULL; + // thread_operand is stored in execution::pthread_map; return (Thread *)get_location(); } else return NULL; diff --git a/action.h b/action.h index f54c9d2a..2ca1429a 100644 --- a/action.h +++ b/action.h @@ -11,6 +11,7 @@ #include "mymemory.h" #include "memoryorder.h" #include "modeltypes.h" +#include "pthread.h" /* Forward declarations */ class ClockVector; @@ -59,6 +60,7 @@ typedef enum action_type { THREAD_FINISH, /**< A thread completion action */ PTHREAD_CREATE, /**< A pthread creation action */ PTHREAD_JOIN, /**< A pthread join action */ + ATOMIC_UNINIT, /**< Represents an uninitialized atomic */ ATOMIC_READ, /**< An atomic read action */ ATOMIC_WRITE, /**< An atomic write action */ @@ -102,6 +104,7 @@ public: memory_order get_original_mo() const { return original_order; } void set_mo(memory_order order) { this->order = order; } void * get_location() const { return location; } + void * get_mutex_location() const { return location_mutex; } modelclock_t get_seq_number() const { return seq_number; } uint64_t get_value() const { return value; } uint64_t get_reads_from_value() const; @@ -211,6 +214,9 @@ private: /** @brief A pointer to the memory location for this action. */ void *location; + /** @brief A pointer to the memory location for mutex. */ + void *location_mutex; + /** @brief The thread id that performed this action. */ thread_id_t tid; diff --git a/execution.cc b/execution.cc index 887e2efa..e21fc8aa 100644 --- a/execution.cc +++ b/execution.cc @@ -1,6 +1,5 @@ #include #include -#include #include #include @@ -17,8 +16,6 @@ #include "threads-model.h" #include "bugmessage.h" -#include - #define INITIAL_THREAD_ID 0 /** @@ -72,9 +69,12 @@ ModelExecution::ModelExecution(ModelChecker *m, scheduler(scheduler), action_trace(), thread_map(2), /* We'll always need at least 2 threads */ + pthread_map(0), + pthread_counter(0), obj_map(), condvar_waiters_map(), obj_thrd_map(), + mutex_map(), promises(), futurevalues(), pending_rel_seqs(), @@ -961,18 +961,25 @@ bool ModelExecution::process_thread_action(ModelAction *curr) break; } case PTHREAD_CREATE: { - thrd_t *thrd = (thrd_t *)curr->get_location(); + (*(pthread_t *)curr->get_location()) = pthread_counter++; + struct pthread_params *params = (struct pthread_params *)curr->get_value(); - Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr)); + Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr)); curr->set_thread_operand(th); add_thread(th); th->set_creation(curr); + + if ( pthread_map.size() < pthread_counter ) + pthread_map.resize( pthread_counter ); + pthread_map[ pthread_counter-1 ] = th; + /* Promises can be satisfied by children */ for (unsigned int i = 0; i < promises.size(); i++) { Promise *promise = promises[i]; if (promise->thread_is_available(curr->get_tid())) promise->add_thread(th->get_id()); } + break; } case THREAD_JOIN: { @@ -2374,6 +2381,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); + action_list_t *list = obj_map.get(location); /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; @@ -2848,6 +2856,16 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const return get_thread(act->get_tid()); } +/** + * @brief Get a Thread reference by its pthread ID + * @param index The pthread's ID + * @return A Thread reference + */ +Thread * ModelExecution::get_pthread(pthread_t pid) { + if (pid < pthread_counter + 1) return pthread_map[pid]; + else return NULL; +} + /** * @brief Get a Promise's "promise number" * diff --git a/execution.h b/execution.h index 9322f55b..5f5fd0a2 100644 --- a/execution.h +++ b/execution.h @@ -16,6 +16,8 @@ #include "stl-model.h" #include "params.h" +#include + /* Forward declaration */ class Node; class NodeStack; @@ -79,6 +81,11 @@ public: void add_thread(Thread *t); Thread * get_thread(thread_id_t tid) const; Thread * get_thread(const ModelAction *act) const; + + pthread_t get_pthread_counter() { return pthread_counter; } + void incr_pthread_counter() { pthread_counter++; } + Thread * get_pthread(pthread_t pid); + int get_promise_number(const Promise *promise) const; bool is_enabled(Thread *t) const; @@ -118,9 +125,12 @@ public: CycleGraph * const get_mo_graph() { return mo_graph; } + HashTable mutex_map; + SNAPSHOTALLOC private: int get_execution_number() const; + pthread_t pthread_counter; ModelChecker *model; @@ -147,6 +157,7 @@ private: bool process_write(ModelAction *curr, work_queue_t *work); bool process_fence(ModelAction *curr); bool process_mutex(ModelAction *curr); + bool process_thread_action(ModelAction *curr); void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue); bool read_from(ModelAction *act, const ModelAction *rf); @@ -195,6 +206,7 @@ private: action_list_t action_trace; SnapVector thread_map; + SnapVector pthread_map; /** Per-object list of actions. Maps an object (i.e., memory location) * to a trace of all actions performed on the object. */ @@ -206,6 +218,8 @@ private: HashTable *, uintptr_t, 4> obj_thrd_map; +// HashTable mutex_map; + /** * @brief List of currently-pending promises * diff --git a/model.cc b/model.cc index 39f0c694..c4bcaf9b 100644 --- a/model.cc +++ b/model.cc @@ -542,10 +542,8 @@ void ModelChecker::run() } while (!should_terminate_execution()); has_next = next_execution(); - pthread_map.clear(); - mutex_map.clear(); i++; - } while (i<100); // while (has_next); + } while (i<2); // while (has_next); execution->fixup_release_sequences(); diff --git a/model.h b/model.h index 7e651561..f73f4fa2 100644 --- a/model.h +++ b/model.h @@ -16,9 +16,6 @@ #include "context.h" #include "params.h" -#include -#include - /* Forward declaration */ class Node; class NodeStack; @@ -68,6 +65,7 @@ public: Thread * get_thread(thread_id_t tid) const; Thread * get_thread(const ModelAction *act) const; + Thread * get_pthread(pthread_t pid); Thread * get_current_thread() const; @@ -81,8 +79,6 @@ public: void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); } 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; @@ -106,7 +102,6 @@ private: Thread * get_next_thread(); void reset_to_initial_state(); - ModelAction *diverge; ModelAction *earliest_diverge; diff --git a/pthread.cc b/pthread.cc index d811ffef..750a302c 100644 --- a/pthread.cc +++ b/pthread.cc @@ -1,24 +1,18 @@ #include "common.h" #include "threads-model.h" #include "action.h" -#include +#include "pthread.h" #include /* global "model" object */ #include "model.h" - -unsigned int counter = 0; // counter does not to be reset to zero. It is - // find as long as it is unique. +#include "execution.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 }; - *t = counter; - counter++; - 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); @@ -27,15 +21,17 @@ int pthread_create(pthread_t *t, const pthread_attr_t * attr, } int pthread_join(pthread_t t, void **value_ptr) { - ModelAction *act = model->pthread_map[t]; - Thread *th = act->get_thread_operand(); +// Thread *th = model->get_pthread(t); + ModelExecution *execution = model->get_execution(); + Thread *th = execution->get_pthread(t); model->switch_to_master(new ModelAction(PTHREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(th->get_id()))); - // store return value - void *rtval = th->get_pthread_return(); - *value_ptr = rtval; - + if ( value_ptr ) { + // store return value + void *rtval = th->get_pthread_return(); + *value_ptr = rtval; + } return 0; } @@ -45,36 +41,41 @@ void pthread_exit(void *value_ptr) { } int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { - if (model->mutex_map.find(p_mutex) != model->mutex_map.end() ) { - 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; + + ModelExecution *execution = model->get_execution(); + execution->mutex_map.put(p_mutex, m); return 0; } int pthread_mutex_lock(pthread_mutex_t *p_mutex) { - std::mutex *m = model->mutex_map[p_mutex]; + ModelExecution *execution = model->get_execution(); + std::mutex *m = execution->mutex_map.get(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]; + ModelExecution *execution = model->get_execution(); + std::mutex *m = execution->mutex_map.get(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(); + ModelExecution *execution = model->get_execution(); + std::mutex *m = execution->mutex_map.get(p_mutex); + m->unlock(); + return 0; } -void check() { - for (std::map::iterator it = model->pthread_map.begin(); it != model->pthread_map.end(); it++) { - model_print("id: %d\n", it->first); - } +pthread_t pthread_self() { + Thread* th = model->get_current_thread(); + return th->get_id(); +} + +int pthread_key_delete(pthread_key_t) { + model_print("key_delete is called\n"); + return 0; }