X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=38f40e5cd1ee55b47103883fa9677b6ad7ea7e6d;hp=9dc1d37c71bb6ac93844d057efd7928818d7e053;hb=7c77391dff9f4cf3166d47015494f0af276963f0;hpb=2e343f1ee60e801cb17ef75fb915f44a389eb6c7

diff --git a/model.cc b/model.cc
index 9dc1d37..38f40e5 100644
--- a/model.cc
+++ b/model.cc
@@ -25,6 +25,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	num_executions(0),
 	num_feasible_executions(0),
 	diverge(NULL),
+	earliest_diverge(NULL),
 	action_trace(new action_list_t()),
 	thread_map(new HashTable<int, Thread *, int>()),
 	obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
@@ -138,6 +139,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 	ModelAction *next = node_stack->get_next()->get_action();
 
 	if (next == diverge) {
+		if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+			earliest_diverge=diverge;
+
 		Node *nextnode = next->get_node();
 		/* Reached divergence point */
 		if (nextnode->increment_promise()) {
@@ -157,8 +161,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			Node *node = nextnode->get_parent();
 			tid = node->get_next_backtrack();
 			node_stack->pop_restofstack(1);
+			if (diverge==earliest_diverge) {
+				earliest_diverge=node->get_action();
+			}
 		}
 		DEBUG("*** Divergence point ***\n");
+
 		diverge = NULL;
 	} else {
 		tid = next->get_tid();
@@ -180,8 +188,16 @@ bool ModelChecker::next_execution()
 	DBG();
 
 	num_executions++;
-	if (isfinalfeasible())
+	if (isfinalfeasible()) {
+		printf("Earliest divergence point since last feasible execution:\n");
+		if (earliest_diverge)
+			earliest_diverge->print(false);
+		else
+			printf("(Not set)\n");
+
+		earliest_diverge = NULL;
 		num_feasible_executions++;
+	}
 
 	if (isfinalfeasible() || DBG_ENABLED())
 		print_summary();
@@ -414,7 +430,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 		action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
 		//activate all the waiting threads
 		for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
-			scheduler->add_thread(get_thread((*rit)->get_tid()));
+			scheduler->wake(get_thread(*rit));
 		}
 		waiters->clear();
 		break;
@@ -459,11 +475,11 @@ bool ModelChecker::process_write(ModelAction *curr)
  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
  *
  * @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated or a thread completed
  */
 bool ModelChecker::process_thread_action(ModelAction *curr)
 {
-	bool synchronized = false;
+	bool updated = false;
 
 	switch (curr->get_type()) {
 	case THREAD_CREATE: {
@@ -472,28 +488,20 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		break;
 	}
 	case THREAD_JOIN: {
-		Thread *waiting, *blocking;
-		waiting = get_thread(curr);
-		blocking = (Thread *)curr->get_location();
-		if (!blocking->is_complete()) {
-			blocking->push_wait_list(curr);
-			scheduler->sleep(waiting);
-		} else {
-			do_complete_join(curr);
-			synchronized = true;
-		}
+		Thread *blocking = (Thread *)curr->get_location();
+		ModelAction *act = get_last_action(blocking->get_id());
+		curr->synchronize_with(act);
+		updated = true; /* trigger rel-seq checks */
 		break;
 	}
 	case THREAD_FINISH: {
 		Thread *th = get_thread(curr);
 		while (!th->wait_list_empty()) {
 			ModelAction *act = th->pop_wait_list();
-			Thread *wake = get_thread(act);
-			scheduler->wake(wake);
-			do_complete_join(act);
-			synchronized = true;
+			scheduler->wake(get_thread(act));
 		}
 		th->complete();
+		updated = true; /* trigger rel-seq checks */
 		break;
 	}
 	case THREAD_START: {
@@ -504,7 +512,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		break;
 	}
 
-	return synchronized;
+	return updated;
 }
 
 /**
@@ -531,6 +539,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		return newcurr;
 	}
 
+	curr->set_seq_number(get_next_seq_num());
+
 	newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
 	if (newcurr) {
 		/* First restore type and order in case of RMW operation */
@@ -561,9 +571,12 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 }
 
 /**
- * This method checks whether a model action is enabled at the given point.
- * At this point, it checks whether a lock operation would be successful at this point.
- * If not, it puts the thread in a waiter list.
+ * @brief Check whether a model action is enabled.
+ *
+ * Checks whether a lock or join operation would be successful (i.e., is the
+ * lock already locked, or is the joined thread already complete). If not, put
+ * the action in a waiter list.
+ *
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
  */
@@ -576,6 +589,12 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 			lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
 			return false;
 		}
+	} else if (curr->get_type() == THREAD_JOIN) {
+		Thread *blocking = (Thread *)curr->get_location();
+		if (!blocking->is_complete()) {
+			blocking->push_wait_list(curr);
+			return false;
+		}
 	}
 
 	return true;
@@ -601,9 +620,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	if (!check_action_enabled(curr)) {
 		/* Make the execution look like we chose to run this action
-		 * much later, when a lock is actually available to release */
+		 * much later, when a lock/join can succeed */
 		get_current_thread()->set_pending(curr);
-		remove_thread(get_current_thread());
+		scheduler->sleep(get_current_thread());
 		return get_next_thread(NULL);
 	}
 
@@ -658,7 +677,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			bool updated = false;
 
 			if (act->is_read()) {
-				if (r_modification_order(act, act->get_reads_from()))
+				const ModelAction *rf = act->get_reads_from();
+				if (rf != NULL && r_modification_order(act, rf))
 					updated = true;
 			}
 			if (act->is_write()) {
@@ -684,19 +704,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	return get_next_thread(curr);
 }
 
-/**
- * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
- * operation from the Thread it is joining with. Must be called after the
- * completion of the Thread in question.
- * @param join The THREAD_JOIN action
- */
-void ModelChecker::do_complete_join(ModelAction *join)
-{
-	Thread *blocking = (Thread *)join->get_location();
-	ModelAction *act = get_last_action(blocking->get_id());
-	join->synchronize_with(act);
-}
-
 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
@@ -1304,6 +1311,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 		}
 
 		if (updated) {
+			/* Re-check all pending release sequences */
+			work_queue->push_back(CheckRelSeqWorkEntry(NULL));
 			/* Re-check act for mo_graph edges */
 			work_queue->push_back(MOEdgeWorkEntry(act));
 
@@ -1588,6 +1597,33 @@ static void print_list(action_list_t *list)
 	printf("---------------------------------------------------------------------\n");
 }
 
+#if SUPPORT_MOD_ORDER_DUMP
+void ModelChecker::dumpGraph(char *filename) {
+	char buffer[200];
+  sprintf(buffer, "%s.dot",filename);
+  FILE *file=fopen(buffer, "w");
+  fprintf(file, "digraph %s {\n",filename);
+	mo_graph->dumpNodes(file);
+	ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
+	
+	for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
+		ModelAction *action=*it;
+		if (action->is_read()) {
+			fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
+			fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+		}
+		if (thread_array[action->get_tid()] != NULL) {
+			fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
+		}
+		
+		thread_array[action->get_tid()]=action;
+	}
+  fprintf(file,"}\n");
+	model_free(thread_array);
+  fclose(file);	
+}
+#endif
+
 void ModelChecker::print_summary()
 {
 	printf("\n");
@@ -1600,6 +1636,8 @@ void ModelChecker::print_summary()
 	char buffername[100];
 	sprintf(buffername, "exec%04u", num_executions);
 	mo_graph->dumpGraphToFile(buffername);
+	sprintf(buffername, "graph%04u", num_executions);
+  dumpGraph(buffername);
 #endif
 
 	if (!isfinalfeasible())