move pthread_map and mutex_map inside of execution.h

diff --git a/action.cc b/action.cc
index 359316d12a196e2c2d18c10e62685e1c1cf503a6..eecf23ca4e2486c3c2d14c219c5e1b5498b3188f 100644 (file)
--- 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 f54c9d2aeb9b03d784d6c0762b037e765000d23b..2ca1429aeffc460878de5cf3c9dc578593051fcd 100644 (file)
--- 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 887e2efa03df0f31832ff6ee260a1a8b1ed9794d..e21fc8aa87bad1a1bc572490acf87f574ba9fb23 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1,6 +1,5 @@
 #include <stdio.h>
 #include <algorithm>
-#include <mutex>
 #include <new>
 #include <stdarg.h>
 
@@ -17,8 +16,6 @@
 #include "threads-model.h"
 #include "bugmessage.h"
 
-#include <pthread.h>
-
 #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 9322f55b4c3e0de4ab37502e328d812bf479be68..5f5fd0a2b54c1b02f8b2efb86bce45f37f2f802c 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -16,6 +16,8 @@
 #include "stl-model.h"
 #include "params.h"
 
+#include <mutex>
+
 /* 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<pthread_mutex_t *, std::mutex *, uintptr_t, 4> 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 *> thread_map;
+       SnapVector<Thread *> 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<void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
 
+//     HashTable<pthread_mutex_t *, std::mutex *, uintptr_t, 4> mutex_map;
+
        /**
         * @brief List of currently-pending promises
         *

diff --git a/model.cc b/model.cc
index 39f0c694e9b7e440ee5ffa952ded7b4b06f0a7ca..c4bcaf9b1c257ec7ec8707f506d5a35c44cf8e64 100644 (file)
--- 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 7e651561a79740af75910d2f7fd1251691644b49..f73f4fa23b08dbb247c7347609fa7cfe9c6ec398 100644 (file)
--- a/model.h
+++ b/model.h
@@ -16,9 +16,6 @@
 #include "context.h"
 #include "params.h"
 
-#include <map>
-#include <mutex>
-
 /* 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_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;
@@ -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 d811ffef6a00279ee05e2ff657e0138020e6e509..750a302ceb454439306403805e0fceb287e652b1 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -1,24 +1,18 @@
 #include "common.h"
 #include "threads-model.h"
 #include "action.h"
-#include <pthread.h>
+#include "pthread.h"
 #include <mutex>
 
 /* 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)&params);
-       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<pthread_t, ModelAction*>::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;
 }