X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=25f85d0ee4403ebb1b6ef00531cf872bbdd29892;hb=3519c47202090f3c4a69de0e89aaa2617b17ff75;hp=4cbcd4fd96b215ddf1440b9a20212b01fb4579d5;hpb=1ff648af632c0ccc8e5319a077791bd6e49011f6;p=model-checker.git

diff --git a/model.cc b/model.cc
index 4cbcd4f..25f85d0 100644
--- a/model.cc
+++ b/model.cc
@@ -200,7 +200,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 			return NULL;
 	}
 	/* linear search: from most recent to oldest */
-	action_list_t *list = obj_map->ensureptr(act->get_location());
+	action_list_t *list = obj_map->get_safe_ptr(act->get_location());
 	action_list_t::reverse_iterator rit;
 	for (rit = list->rbegin(); rit != list->rend(); rit++) {
 		ModelAction *prev = *rit;
@@ -384,7 +384,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction * act) {
  * @param rf The action that curr reads from. Must be a write.
  */
 void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 	unsigned int i;
 	ASSERT(curr->is_read());
 
@@ -414,7 +414,7 @@ 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());
+	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 	unsigned int i;
 	ASSERT(curr->is_read());
 
@@ -453,7 +453,7 @@ void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelActi
  * @param curr The current action. Must be a write.
  */
 void ModelChecker::w_modification_order(ModelAction * curr) {
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 	unsigned int i;
 	ASSERT(curr->is_write());
 
@@ -475,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;
 			}
 		}
 	}
@@ -511,9 +510,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 	int tid = id_to_int(act->get_tid());
 	action_trace->push_back(act);
 
-	obj_map->ensureptr(act->get_location())->push_back(act);
+	obj_map->get_safe_ptr(act->get_location())->push_back(act);
 
-	std::vector<action_list_t> *vec = obj_thrd_map->ensureptr(act->get_location());
+	std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
 	if (tid >= (int)vec->size())
 		vec->resize(next_thread_id);
 	(*vec)[tid].push_back(act);
@@ -539,7 +538,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid)
  */
 ModelAction * ModelChecker::get_last_seq_cst(const void *location)
 {
-	action_list_t *list = obj_map->ensureptr(location);
+	action_list_t *list = obj_map->get_safe_ptr(location);
 	/* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
 	action_list_t::reverse_iterator rit;
 	for (rit = list->rbegin(); rit != list->rend(); rit++)
@@ -627,7 +626,7 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) {
  */
 void ModelChecker::build_reads_from_past(ModelAction *curr)
 {
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 	unsigned int i;
 	ASSERT(curr->is_read());
 
@@ -717,11 +716,15 @@ void ModelChecker::print_summary()
 	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)
@@ -746,5 +749,48 @@ int ModelChecker::switch_to_master(ModelAction *act)
 	Thread * old = thread_current();
 	set_current_action(act);
 	old->set_state(THREAD_READY);
-	return Thread::swap(old, get_system_context());
+	return Thread::swap(old, &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(&system_context, next) == 0);
+}
+
+/** Runs the current execution until threre are no more steps to take. */
+void ModelChecker::finish_execution() {
+	DBG();
+
+	while (take_step());
 }