X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=a74147be4bbe7e068a9ddd05a58ff459ccb1a7c8;hb=3a4e118d45bf83a3b4c3a0a73d1071fa8fe5476d;hp=8b507718ee2d3579b7bab555d7c424b6d2a4083b;hpb=20956d81209b12a99ced78f51dd4294a0638343f;p=model-checker.git

diff --git a/execution.cc b/execution.cc
index 8b50771..a74147b 100644
--- a/execution.cc
+++ b/execution.cc
@@ -65,8 +65,8 @@ ModelExecution::ModelExecution(ModelChecker *m,
 	params(params),
 	scheduler(scheduler),
 	action_trace(),
-	thread_map(),
-	obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
+	thread_map(2), /* We'll always need at least 2 threads */
+	obj_map(),
 	condvar_waiters_map(),
 	obj_thrd_map(),
 	promises(),
@@ -80,17 +80,16 @@ ModelExecution::ModelExecution(ModelChecker *m,
 {
 	/* Initialize a model-checker thread, for special ModelActions */
 	model_thread = new Thread(get_next_id());
-	thread_map.put(id_to_int(model_thread->get_id()), model_thread);
+	add_thread(model_thread);
 	scheduler->register_engine(this);
+	node_stack->register_engine(this);
 }
 
 /** @brief Destructor */
 ModelExecution::~ModelExecution()
 {
 	for (unsigned int i = 0; i < get_num_threads(); i++)
-		delete thread_map.get(i);
-
-	delete obj_map;
+		delete get_thread(int_to_id(i));
 
 	for (unsigned int i = 0; i < promises.size(); i++)
 		delete promises[i];
@@ -367,17 +366,22 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
 ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 {
 	switch (act->get_type()) {
-	/* case ATOMIC_FENCE: fences don't directly cause backtracking */
+	case ATOMIC_FENCE:
+		/* Only seq-cst fences can (directly) cause backtracking */
+		if (!act->is_seqcst())
+			break;
 	case ATOMIC_READ:
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {
 		ModelAction *ret = NULL;
 
 		/* linear search: from most recent to oldest */
-		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+		action_list_t *list = obj_map.get(act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
+			if (prev == act)
+				continue;
 			if (prev->could_synchronize_with(act)) {
 				ret = prev;
 				break;
@@ -396,7 +400,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 	case ATOMIC_LOCK:
 	case ATOMIC_TRYLOCK: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+		action_list_t *list = obj_map.get(act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -407,7 +411,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 	}
 	case ATOMIC_UNLOCK: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+		action_list_t *list = obj_map.get(act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -418,7 +422,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 	}
 	case ATOMIC_WAIT: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+		action_list_t *list = obj_map.get(act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -433,7 +437,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 	case ATOMIC_NOTIFY_ALL:
 	case ATOMIC_NOTIFY_ONE: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+		action_list_t *list = obj_map.get(act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -1210,7 +1214,7 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
  *
  * @param curr The current action to process
  * @return The ModelAction that is actually executed; may be different than
- * curr; may be NULL, if the current action is not enabled to run
+ * curr
  */
 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 {
@@ -2112,7 +2116,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 	int tid = id_to_int(act->get_tid());
 	ModelAction *uninit = NULL;
 	int uninit_id = -1;
-	action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+	action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
 	if (list->empty() && act->is_atomic_var()) {
 		uninit = get_uninitialized_action(act);
 		uninit_id = id_to_int(uninit->get_tid());
@@ -2145,7 +2149,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 
 	if (act->is_wait()) {
 		void *mutex_loc = (void *) act->get_value();
-		get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
+		get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
 
 		SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
 		if (tid >= (int)vec->size())
@@ -2193,7 +2197,7 @@ ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
 {
 	void *location = curr->get_location();
-	action_list_t *list = get_safe_ptr_action(obj_map, location);
+	action_list_t *list = obj_map.get(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) != curr; rit++)
@@ -2215,8 +2219,12 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
  */
 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
 {
-	/* All fences should have NULL location */
-	action_list_t *list = get_safe_ptr_action(obj_map, NULL);
+	/* All fences should have location FENCE_LOCATION */
+	action_list_t *list = obj_map.get(FENCE_LOCATION);
+
+	if (!list)
+		return NULL;
+
 	action_list_t::reverse_iterator rit = list->rbegin();
 
 	if (before_fence) {
@@ -2245,7 +2253,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode
 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
 {
 	void *location = curr->get_location();
-	action_list_t *list = get_safe_ptr_action(obj_map, location);
+	action_list_t *list = obj_map.get(location);
 	/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
 	action_list_t::reverse_iterator rit;
 	for (rit = list->rbegin(); rit != list->rend(); rit++)
@@ -2675,7 +2683,10 @@ void ModelExecution::print_summary() const
  */
 void ModelExecution::add_thread(Thread *t)
 {
-	thread_map.put(id_to_int(t->get_id()), t);
+	unsigned int i = id_to_int(t->get_id());
+	if (i >= thread_map.size())
+		thread_map.resize(i + 1);
+	thread_map[i] = t;
 	if (!t->is_model_thread())
 		scheduler->add_thread(t);
 }
@@ -2687,7 +2698,10 @@ void ModelExecution::add_thread(Thread *t)
  */
 Thread * ModelExecution::get_thread(thread_id_t tid) const
 {
-	return thread_map.get(id_to_int(tid));
+	unsigned int i = id_to_int(tid);
+	if (i < thread_map.size())
+		return thread_map[i];
+	return NULL;
 }
 
 /**