X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=a4f7e90fc332b39c8be422a8eef450f3d4368aca;hb=4730dd573ad7a28d875c31b6aa633f7bce420054;hp=02a4a6a29206b34b8b3b22308439807b1b7c1188;hpb=72fd87546b318a6fe8016fb06c8a9015949450bb;p=model-checker.git

diff --git a/model.cc b/model.cc
index 02a4a6a..a4f7e90 100644
--- a/model.cc
+++ b/model.cc
@@ -15,14 +15,14 @@
 ModelChecker *model;
 
 /** @brief Constructor */
-ModelChecker::ModelChecker()
-	:
+ModelChecker::ModelChecker(struct model_params params) :
 	/* Initialize default scheduler */
 	scheduler(new Scheduler()),
 	/* First thread created will have id INITIAL_THREAD_ID */
 	next_thread_id(INITIAL_THREAD_ID),
 	used_sequence_numbers(0),
 	num_executions(0),
+	params(params),
 	current_action(NULL),
 	diverge(NULL),
 	nextThread(THREAD_ID_T_NONE),
@@ -42,9 +42,8 @@ ModelChecker::ModelChecker()
 /** @brief Destructor */
 ModelChecker::~ModelChecker()
 {
-	/*	std::map<int, Thread *>::iterator it;
-	for (it = thread_map->begin(); it != thread_map->end(); it++)
-	delete (*it).second;*/
+	for (int i = 0; i < get_num_threads(); i++)
+		delete thread_map->get(i);
 	delete thread_map;
 
 	delete obj_thrd_map;
@@ -267,11 +266,11 @@ void ModelChecker::check_current_action(void)
 		return;
 	}
 
-	if (curr->is_rmwc()||curr->is_rmw()) {
-		ModelAction *tmp=process_rmw(curr);
+	if (curr->is_rmwc() || curr->is_rmw()) {
+		ModelAction *tmp = process_rmw(curr);
 		already_added = true;
 		delete curr;
-		curr=tmp;
+		curr = tmp;
 	} else {
 		ModelAction * tmp = node_stack->explore_action(curr);
 		if (tmp) {
@@ -281,10 +280,9 @@ void ModelChecker::check_current_action(void)
 				tmp->copy_typeandorder(curr);
 
 			/* If we have diverged, we need to reset the clock vector. */
-			if (diverge==NULL) {
+			if (diverge == NULL)
 				tmp->create_cv(get_parent_action(tmp->get_tid()));
-			}
-			
+
 			delete curr;
 			curr = tmp;
 		} else {
@@ -308,16 +306,15 @@ void ModelChecker::check_current_action(void)
 	}
 
 	/* Deal with new thread */
-	if (curr->get_type() == THREAD_START) {
+	if (curr->get_type() == THREAD_START)
 		check_promises(NULL, curr->get_cv());
-	}
 
 	/* Assign reads_from values */
 	Thread *th = get_thread(curr->get_tid());
 	uint64_t value = VALUE_NONE;
 	if (curr->is_read()) {
 		const ModelAction *reads_from = curr->get_node()->get_read_from();
-		if (reads_from!=NULL) {
+		if (reads_from != NULL) {
 			value = reads_from->get_value();
 			/* Assign reads_from, perform release/acquire synchronization */
 			curr->read_from(reads_from);
@@ -326,7 +323,7 @@ void ModelChecker::check_current_action(void)
 			/* Read from future value */
 			value = curr->get_node()->get_future_value();
 			curr->read_from(NULL);
-			Promise * valuepromise=new Promise(curr, value);
+			Promise * valuepromise = new Promise(curr, value);
 			promises->push_back(valuepromise);
 		}
 	} else if (curr->is_write()) {
@@ -340,24 +337,24 @@ void ModelChecker::check_current_action(void)
 	if (!already_added)
 		add_action_to_lists(curr);
 
-	/* Is there a better interface for setting the next thread rather
+	/** @todo Is there a better interface for setting the next thread rather
 		 than this field/convoluted approach?  Perhaps like just returning
 		 it or something? */
 
 	/* Do not split atomic actions. */
-	if (curr->is_rmwr()) {
+	if (curr->is_rmwr())
 		nextThread = thread_current()->get_id();
-	} else {
+	else
 		nextThread = get_next_replay_thread();
-	}
 
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
 
-	if (!parnode->backtrack_empty()||!currnode->read_from_empty()||!currnode->future_value_empty()||!currnode->promise_empty())
+	if (!parnode->backtrack_empty() || !currnode->read_from_empty() ||
+	          !currnode->future_value_empty() || !currnode->promise_empty())
 		if (!next_backtrack || *curr > *next_backtrack)
 			next_backtrack = curr;
-	
+
 	set_backtracking(curr);
 }
 
@@ -368,13 +365,13 @@ bool ModelChecker::isfeasible() {
 
 /** Returns whether the current completed trace is feasible. */
 bool ModelChecker::isfinalfeasible() {
-	return isfeasible() && promises->size()==0;
+	return isfeasible() && promises->size() == 0;
 }
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction * act) {
 	int tid = id_to_int(act->get_tid());
-	ModelAction *lastread=get_last_action(tid);
+	ModelAction *lastread = get_last_action(tid);
 	lastread->process_rmw(act);
 	if (act->is_rmw())
 		cyclegraph->addRMWEdge(lastread, lastread->get_reads_from());
@@ -402,10 +399,10 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr)) {
 				if (act->is_read()) {
-					const ModelAction * prevreadfrom=act->get_reads_from();
-					if (rf!=prevreadfrom)
+					const ModelAction * prevreadfrom = act->get_reads_from();
+					if (prevreadfrom != NULL && rf != prevreadfrom)
 						cyclegraph->addEdge(rf, prevreadfrom);
-				} else if (rf!=act) {
+				} else if (rf != act) {
 					cyclegraph->addEdge(rf, act);
 				}
 				break;
@@ -414,6 +411,43 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r
 	}
 }
 
+/** Updates the cyclegraph with the constraints imposed from the
+ *  current read. */
+void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelAction *rf) {
+	std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+	unsigned int i;
+	ASSERT(curr->is_read());
+
+	/* Iterate over all threads */
+	for (i = 0; i < thrd_lists->size(); i++) {
+		/* Iterate over actions in thread, starting from most recent */
+		action_list_t *list = &(*thrd_lists)[i];
+		action_list_t::reverse_iterator rit;
+		ModelAction *lastact = NULL;
+
+		/* Find last action that happens after curr */
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *act = *rit;
+			if (curr->happens_before(act)) {
+				lastact = act;
+			} else
+				break;
+		}
+
+			/* Include at most one act per-thread that "happens before" curr */
+		if (lastact != NULL) {
+			if (lastact->is_read()) {
+				const ModelAction * postreadfrom = lastact->get_reads_from();
+				if (postreadfrom != NULL&&rf != postreadfrom)
+					cyclegraph->addEdge(postreadfrom, rf);
+			} else if (rf != lastact) {
+				cyclegraph->addEdge(lastact, rf);
+			}
+			break;
+		}
+	}
+}
+
 /**
  * Updates the cyclegraph with the constraints imposed from the current write.
  * @param curr The current action. Must be a write.
@@ -426,8 +460,8 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
 	if (curr->is_seqcst()) {
 		/* We have to at least see the last sequentially consistent write,
 			 so we are initialized. */
-		ModelAction * last_seq_cst=get_last_seq_cst(curr->get_location());
-		if (last_seq_cst!=NULL)
+		ModelAction * last_seq_cst = get_last_seq_cst(curr->get_location());
+		if (last_seq_cst != NULL)
 			cyclegraph->addEdge(curr, last_seq_cst);
 	}
 
@@ -441,25 +475,24 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr)) {
-				if (act->is_read()) {
+				if (act->is_read())
 					cyclegraph->addEdge(curr, act->get_reads_from());
-				} else
+				else
 					cyclegraph->addEdge(curr, act);
 				break;
-			} else {
-				if (act->is_read()&&!act->is_synchronizing(curr)&&!act->same_thread(curr)) {
-					/* We have an action that:
-						 (1) did not happen before us
-						 (2) is a read and we are a write
-						 (3) cannot synchronize with us
-						 (4) is in a different thread 
-						 =>
-						 that read could potentially read from our write.
-					*/
-					if (act->get_node()->add_future_value(curr->get_value())&&
-							(!next_backtrack || *act > * next_backtrack))
-						next_backtrack = act;
-				}
+			} else if (act->is_read() && !act->is_synchronizing(curr) &&
+			                             !act->same_thread(curr)) {
+				/* We have an action that:
+				   (1) did not happen before us
+				   (2) is a read and we are a write
+				   (3) cannot synchronize with us
+				   (4) is in a different thread
+				   =>
+				   that read could potentially read from our write.
+				 */
+				if (act->get_node()->add_future_value(curr->get_value()) &&
+						(!next_backtrack || *act > *next_backtrack))
+					next_backtrack = act;
 			}
 		}
 	}
@@ -535,12 +568,13 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
 /** Resolve the given promises. */
 
 void ModelChecker::resolve_promises(ModelAction *write) {
-	for(unsigned int i=0, promise_index=0;promise_index<promises->size(); i++) {
-		Promise * promise=(*promises)[promise_index];
+	for (unsigned int i = 0, promise_index = 0;promise_index<promises->size(); i++) {
+		Promise * promise = (*promises)[promise_index];
 		if (write->get_node()->get_promise(i)) {
-			ModelAction * read=promise->get_action();
+			ModelAction * read = promise->get_action();
 			read->read_from(write);
 			r_modification_order(read, write);
+			post_r_modification_order(read, write);
 			promises->erase(promises->begin()+promise_index);
 		} else
 			promise_index++;
@@ -551,14 +585,14 @@ void ModelChecker::resolve_promises(ModelAction *write) {
  *  this action. */
 
 void ModelChecker::compute_promises(ModelAction *curr) {
-	for(unsigned int i=0;i<promises->size();i++) {
-		Promise * promise=(*promises)[i];
-		const ModelAction * act=promise->get_action();
+	for (unsigned int i = 0;i<promises->size();i++) {
+		Promise * promise = (*promises)[i];
+		const ModelAction * act = promise->get_action();
 		if (!act->happens_before(curr)&&
 				act->is_read()&&
 				!act->is_synchronizing(curr)&&
 				!act->same_thread(curr)&&
-				promise->get_value()==curr->get_value()) {
+				promise->get_value() == curr->get_value()) {
 			curr->get_node()->set_promise(i);
 		}
 	}
@@ -567,14 +601,14 @@ void ModelChecker::compute_promises(ModelAction *curr) {
 /** Checks promises in response to change in ClockVector Threads. */
 
 void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) {
-	for(unsigned int i=0;i<promises->size();i++) {
-		Promise * promise=(*promises)[i];
-		const ModelAction * act=promise->get_action();
-		if ((old_cv==NULL||!old_cv->synchronized_since(act))&&
+	for (unsigned int i = 0;i<promises->size();i++) {
+		Promise * promise = (*promises)[i];
+		const ModelAction * act = promise->get_action();
+		if ((old_cv == NULL||!old_cv->synchronized_since(act))&&
 				merge_cv->synchronized_since(act)) {
 			//This thread is no longer able to send values back to satisfy the promise
-			int num_synchronized_threads=promise->increment_threads();
-			if (num_synchronized_threads==model->get_num_threads()) {
+			int num_synchronized_threads = promise->increment_threads();
+			if (num_synchronized_threads == model->get_num_threads()) {
 				//Promise has failed
 				failed_promise = true;
 				return;
@@ -616,7 +650,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *act = *rit;
-			
+
 			/* Only consider 'write' actions */
 			if (!act->is_write())
 				continue;
@@ -668,7 +702,7 @@ static void print_list(action_list_t *list)
 	printf("---------------------------------------------------------------------\n");
 }
 
-void ModelChecker::print_summary(void)
+void ModelChecker::print_summary()
 {
 	printf("\n");
 	printf("Number of executions: %d\n", num_executions);
@@ -682,11 +716,15 @@ void ModelChecker::print_summary(void)
 	printf("\n");
 }
 
-int ModelChecker::add_thread(Thread *t)
+/**
+ * Add a Thread to the system for the first time. Should only be called once
+ * per thread.
+ * @param t The Thread to add
+ */
+void ModelChecker::add_thread(Thread *t)
 {
 	thread_map->put(id_to_int(t->get_id()), t);
 	scheduler->add_thread(t);
-	return 0;
 }
 
 void ModelChecker::remove_thread(Thread *t)
@@ -713,3 +751,46 @@ int ModelChecker::switch_to_master(ModelAction *act)
 	old->set_state(THREAD_READY);
 	return Thread::swap(old, get_system_context());
 }
+
+/**
+ * Takes the next step in the execution, if possible.
+ * @return Returns true (success) if a step was taken and false otherwise.
+ */
+bool ModelChecker::take_step() {
+	Thread *curr, *next;
+
+	curr = thread_current();
+	if (curr) {
+		if (curr->get_state() == THREAD_READY) {
+			check_current_action();
+			scheduler->add_thread(curr);
+		} else if (curr->get_state() == THREAD_RUNNING) {
+			/* Stopped while running; i.e., completed */
+			curr->complete();
+		} else {
+			ASSERT(false);
+		}
+	}
+	next = scheduler->next_thread();
+
+	/* Infeasible -> don't take any more steps */
+	if (!isfeasible())
+		return false;
+
+	if (next)
+		next->set_state(THREAD_RUNNING);
+	DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+
+	/* next == NULL -> don't take any more steps */
+	if (!next)
+		return false;
+	/* Return false only if swap fails with an error */
+	return (Thread::swap(get_system_context(), next) == 0);
+}
+
+/** Runs the current execution until threre are no more steps to take. */
+void ModelChecker::finish_execution() {
+	DBG();
+
+	while (take_step());
+}