add support for pthread_create (in progress)

diff --git a/Makefile b/Makefile
index 3c5128545481c917983c17750d421590f5520bc8..a7d2b5264c36c0fe7f5357ae82fd684995526f27 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -4,7 +4,7 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
           nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
           datarace.o impatomic.o cmodelint.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \
-          context.o execution.o libannotate.o
+          context.o execution.o libannotate.o pthread.o
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic
@@ -62,7 +62,8 @@ tags:
        ctags -R
 
 PHONY += tests
-tests: $(LIB_SO)       # $(MAKE) -C $(TESTS_DIR)
+tests: $(LIB_SO)
+       $(MAKE) -C $(TESTS_DIR)
 
 BENCH_DIR := benchmarks
 

diff --git a/model.cc b/model.cc
index 8c384c14888c5bd5f60018dd955a80f4ae875503..ccc109a7be96594f395c2ccd0f6ab56cf230a88f 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -518,7 +518,6 @@ void ModelChecker::run()
                                                        break;
                                                }
                                        } else if (act->get_type() == THREAD_CREATE || \
-                                                       act->get_type() == PTHREAD_CREATE || \ // WL
                                                        act->get_type() == THREAD_START || \
                                                        act->get_type() == THREAD_FINISH) {
                                                t = th;
@@ -543,7 +542,7 @@ void ModelChecker::run()
 
                has_next = next_execution();
                i++;
-       } while (i<1); // while (has_next);
+       } while (i<100); // while (has_next);
 
        execution->fixup_release_sequences();
 

diff --git a/model.h b/model.h
index 94483536cf4e7468346417c7d7ad87887ecaac9e..1d032e1b1e0727113f8167d6e0f09a84ed93fbc1 100644 (file)
--- a/model.h
+++ b/model.h
@@ -16,6 +16,8 @@
 #include "context.h"
 #include "params.h"
 
+#include <map>
+
 /* Forward declaration */
 class Node;
 class NodeStack;
@@ -78,6 +80,7 @@ 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;
 private:
        /** Flag indicates whether to restart the model checker. */
        bool restart_flag;

diff --git a/threads-model.h b/threads-model.h
index 11f2d547233119dc165d86eb62f0de8a5f438df5..f088bace5632a41487f071e1f1c61f2fa8d50e4e 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -43,6 +43,7 @@ public:
        Thread(thread_id_t tid);
        Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread *parent);
        Thread(thread_id_t tid, thrd_t *t, void *(*func)(void *), void *a, Thread *parent);
+
        ~Thread();
        void complete();
 
@@ -133,6 +134,7 @@ private:
 
        void (*start_routine)(void *);
        void *(*pstart_routine)(void *);
+
        void *arg;
        ucontext_t context;
        void *stack;

diff --git a/threads.cc b/threads.cc
index 3d10f4533bd10e320b17523cdf7affbcb07a476c..d7034e93e0d5d34afcfe0377dda9b4688dce91f5 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -51,10 +51,7 @@ void thread_startup()
        model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
 
        /* Call the actual thread function */
-       if ( !curr_thread->start_routine )
-               curr_thread->start_routine(curr_thread->arg);
-       else
-               curr_thread->pstart_routine(curr_thread->arg);
+       curr_thread->start_routine(curr_thread->arg);
        /* Finish thread properly */
        model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread));
 }
@@ -172,17 +169,16 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread
        if (ret)
                model_print("Error in create_context\n");
 
-       user_thread->priv = this;
+       // user_thread->priv = this; // WL
 }
 
-/** 
- * to be modified
- * Construct a new thread for pthread_create.
+/**
+ * Construct a new thread for pthread.
  * @param t The thread identifier of the newly created thread.
  * @param func The function that the thread will call.
  * @param a The parameter to pass to this function.
  */
-Thread::Thread(thread_id_t tid, thrd_t *t, void* (*func)(void *), void *a, Thread *parent) :
+Thread::Thread(thread_id_t tid, thrd_t *t, void *(*func)(void *), void *a, Thread *parent) :
        parent(parent),
        creation(NULL),
        pending(NULL),
@@ -201,10 +197,9 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void* (*func)(void *), void *a, Threa
        ret = create_context();
        if (ret)
                model_print("Error in create_context\n");
-
-       user_thread->priv = this;
 }
 
+
 /** Destructor */
 Thread::~Thread()
 {