From 53504d64f6149c5309577ecaed42450a02e27293 Mon Sep 17 00:00:00 2001
From: weiyu <weiyuluo1232@gmail.com>
Date: Thu, 17 Jan 2019 19:06:30 -0800
Subject: [PATCH] add support for pthread_create (in progress)

---
 Makefile        |  5 +++--
 model.cc        |  3 +--
 model.h         |  3 +++
 threads-model.h |  2 ++
 threads.cc      | 17 ++++++-----------
 5 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Makefile b/Makefile
index 3c512854..a7d2b526 100644
--- 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 8c384c14..ccc109a7 100644
--- 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 94483536..1d032e1b 100644
--- 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 11f2d547..f088bace 100644
--- 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 3d10f453..d7034e93 100644
--- 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()
 {
-- 
2.34.1