X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=9ef071209cbefc9020b662a3ded0d8409b958bf1;hb=HEAD;hp=61d33cb9b629478a4d442bebfbacd155c4383fc6;hpb=448991da4be411c39be8ce3a56615a8eae2811d3;p=c11tester.git

diff --git a/execution.cc b/execution.cc
index 61d33cb9..9ef07120 100644
--- a/execution.cc
+++ b/execution.cc
@@ -14,9 +14,7 @@
 #include "datarace.h"
 #include "threads-model.h"
 #include "bugmessage.h"
-#include "history.h"
 #include "fuzzer.h"
-#include "newfuzzer.h"
 
 #ifdef COLLECT_STAT
 static unsigned int atomic_load_count = 0;
@@ -79,14 +77,12 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
 	thrd_last_fence_release(),
 	priv(new struct model_snapshot_members ()),
 	mo_graph(new CycleGraph()),
-#ifdef NEWFUZZER
-	fuzzer(new NewFuzzer()),
-#else
 	fuzzer(new Fuzzer()),
-#endif
 	isfinished(false)
 {
 	/* Initialize a model-checker thread, for special ModelActions */
+	model_thread = new Thread(get_next_id());
+	add_thread(model_thread);
 	fuzzer->register_engine(m, this);
 	scheduler->register_engine(this);
 #ifdef TLS
@@ -97,7 +93,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
 /** @brief Destructor */
 ModelExecution::~ModelExecution()
 {
-	for (unsigned int i = 0;i < get_num_threads();i++)
+	for (unsigned int i = INITIAL_THREAD_ID;i < get_num_threads();i++)
 		delete get_thread(int_to_id(i));
 
 	delete mo_graph;
@@ -266,7 +262,7 @@ bool ModelExecution::should_wake_up(const ModelAction * asleep) const
 
 void ModelExecution::wake_up_sleeping_actions()
 {
-	for (unsigned int i = 0;i < get_num_threads();i++) {
+	for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {
 		thread_id_t tid = int_to_id(i);
 		if (scheduler->is_sleep_set(tid)) {
 			Thread *thr = get_thread(tid);
@@ -345,7 +341,7 @@ void ModelExecution::set_assert()
 bool ModelExecution::is_deadlocked() const
 {
 	bool blocking_threads = false;
-	for (unsigned int i = 0;i < get_num_threads();i++) {
+	for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {
 		thread_id_t tid = int_to_id(i);
 		if (is_enabled(tid))
 			return false;
@@ -365,7 +361,7 @@ bool ModelExecution::is_deadlocked() const
  */
 bool ModelExecution::is_complete_execution() const
 {
-	for (unsigned int i = 0;i < get_num_threads();i++)
+	for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++)
 		if (is_enabled(int_to_id(i)))
 			return false;
 	return true;
@@ -382,9 +378,6 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
 	add_normal_write_to_lists(act);
 	add_write_to_lists(act);
 	w_modification_order(act);
-#ifdef NEWFUZZER
-	model->get_history()->process_action(act, act->get_tid());
-#endif
 	return act;
 }
 
@@ -494,7 +487,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
 	case ATOMIC_WAIT: {
 		Thread *curr_thrd = get_thread(curr);
 		/* wake up the other threads */
-		for (unsigned int i = 0;i < get_num_threads();i++) {
+		for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {
 			Thread *t = get_thread(int_to_id(i));
 			if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
 				scheduler->wake(t);
@@ -523,7 +516,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
 		}
 
 		/* wake up the other threads */
-		for (unsigned int i = 0;i < get_num_threads();i++) {
+		for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {
 			Thread *t = get_thread(int_to_id(i));
 			if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
 				scheduler->wake(t);
@@ -543,7 +536,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
 		// TODO: lock count for recursive mutexes
 		/* wake up the other threads */
 		Thread *curr_thrd = get_thread(curr);
-		for (unsigned int i = 0;i < get_num_threads();i++) {
+		for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {
 			Thread *t = get_thread(int_to_id(i));
 			if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
 				scheduler->wake(t);
@@ -675,7 +668,7 @@ void ModelExecution::process_thread_action(ModelAction *curr)
 		}
 
 		/* Wake up any joining threads */
-		for (unsigned int i = 0;i < get_num_threads();i++) {
+		for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) {
 			Thread *waiting = get_thread(int_to_id(i));
 			if (waiting->waiting_on() == th &&
 					waiting->get_pending()->is_thread_join())
@@ -1748,9 +1741,6 @@ Thread * ModelExecution::take_step(ModelAction *curr)
 	ASSERT(curr);
 
 	/* Process this action in ModelHistory for records */
-#ifdef NEWFUZZER
-	model->get_history()->process_action( curr, curr->get_tid() );
-#endif
 	if (curr_thrd->is_blocked() || curr_thrd->is_complete())
 		scheduler->remove_thread(curr_thrd);