From 9a7d3d251c12b66783d242a78b288f4b0f414cf7 Mon Sep 17 00:00:00 2001
From: weiyu <weiyuluo1232@gmail.com>
Date: Tue, 22 Jan 2019 11:22:57 -0800
Subject: [PATCH] pthread_create is working now

---
 action.cc    | 14 ++++++++++++--
 execution.cc | 28 ++++++++++++++++++++++++++++
 model.cc     |  5 +++--
 3 files changed, 43 insertions(+), 4 deletions(-)

diff --git a/action.cc b/action.cc
index c913b74c..ea492105 100644
--- a/action.cc
+++ b/action.cc
@@ -280,10 +280,16 @@ Thread * ModelAction::get_thread_operand() const
 		/* THREAD_CREATE stores its (Thread *) in a thrd_t::priv */
 		thrd_t *thrd = (thrd_t *)get_location();
 		return thrd->priv;
-	} else if (type == THREAD_JOIN)
+	} else if (type == PTHREAD_CREATE) {
+		// not implemented
+		return NULL;
+	} else if (type == THREAD_JOIN) {
 		/* THREAD_JOIN uses (Thread *) for location */
 		return (Thread *)get_location();
-	else
+	} else if (type == PTHREAD_JOIN) {
+		// WL: to be added (modified)
+		return (Thread *)get_location();
+	} else
 		return NULL;
 }
 
@@ -551,6 +557,10 @@ const char * ModelAction::get_type_str() const
 		case THREAD_YIELD: return "thread yield";
 		case THREAD_JOIN: return "thread join";
 		case THREAD_FINISH: return "thread finish";
+
+		case PTHREAD_CREATE: return "pthread create";
+		case PTHREAD_JOIN: return "pthread join";
+
 		case ATOMIC_UNINIT: return "uninitialized";
 		case ATOMIC_READ: return "atomic read";
 		case ATOMIC_WRITE: return "atomic write";
diff --git a/execution.cc b/execution.cc
index 869833c2..87e54252 100644
--- a/execution.cc
+++ b/execution.cc
@@ -17,6 +17,8 @@
 #include "threads-model.h"
 #include "bugmessage.h"
 
+#include <pthread.h>
+
 #define INITIAL_THREAD_ID	0
 
 /**
@@ -957,6 +959,20 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
 		}
 		break;
 	}
+	case PTHREAD_CREATE: {
+		thrd_t *thrd = (thrd_t *)curr->get_location();
+		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));
+		add_thread(th);
+		th->set_creation(curr);
+		/* 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: {
 		Thread *blocking = curr->get_thread_operand();
 		ModelAction *act = get_last_action(blocking->get_id());
@@ -964,6 +980,14 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
 		updated = true; /* trigger rel-seq checks */
 		break;
 	}
+	case PTHREAD_JOIN: {
+		break; // WL: to be add (modified)
+		Thread *blocking = curr->get_thread_operand();
+		ModelAction *act = get_last_action(blocking->get_id());
+		synchronize(act, curr);
+		updated = true; /* trigger rel-seq checks */
+	}
+
 	case THREAD_FINISH: {
 		Thread *th = get_thread(curr);
 		/* Wake up any joining threads */
@@ -2892,8 +2916,12 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons
 	}
 
 	/* Follow CREATE with the created thread */
+	/* which is not needed, because model.cc takes care of this */
 	if (curr->get_type() == THREAD_CREATE)
+		return curr->get_thread_operand(); 
+	if (curr->get_type() == PTHREAD_CREATE) {
 		return curr->get_thread_operand();
+	}
 	return NULL;
 }
 
diff --git a/model.cc b/model.cc
index ccc109a7..64bef579 100644
--- a/model.cc
+++ b/model.cc
@@ -503,8 +503,6 @@ void ModelChecker::run()
 					scheduler->sleep(th);
 				}
 			}
-			/* Catch assertions from prior take_step or from
-			 * between-ModelAction bugs (e.g., data races) */
 
 			for (unsigned int i = 1; i < get_num_threads(); i++) {
 				Thread *th = get_thread(int_to_id(i));
@@ -518,6 +516,7 @@ void ModelChecker::run()
 							break;
 						}
 					} else if (act->get_type() == THREAD_CREATE || \
+							act->get_type() == PTHREAD_CREATE || \
 							act->get_type() == THREAD_START || \
 							act->get_type() == THREAD_FINISH) {
 						t = th;
@@ -526,6 +525,8 @@ void ModelChecker::run()
 				}
 			}
 
+			/* Catch assertions from prior take_step or from
+			 * between-ModelAction bugs (e.g., data races) */
 
 			if (execution->has_asserted())
 				break;
-- 
2.34.1