X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=ab16bf82528ea5ebf30766970b37faca5a6ada1f;hb=3133d403d1abd0ac735b4d4662708fcef1cb5d5f;hp=417252c3f92ceb3a4bb7948612ca3592f1be49de;hpb=1798c510e77f37e3d79cba6a1fdad3b13ccc9674;p=model-checker.git

diff --git a/model.cc b/model.cc
index 417252c..ab16bf8 100644
--- a/model.cc
+++ b/model.cc
@@ -28,6 +28,8 @@ struct bug_message {
 
 	char *msg;
 	void print() { printf("%s", msg); }
+
+	SNAPSHOTALLOC
 };
 
 /**
@@ -40,6 +42,7 @@ struct model_snapshot_members {
 	Thread *nextThread;
 	ModelAction *next_backtrack;
 	std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
+	struct execution_stats stats;
 };
 
 /** @brief Constructor */
@@ -47,8 +50,6 @@ ModelChecker::ModelChecker(struct model_params params) :
 	/* Initialize default scheduler */
 	params(params),
 	scheduler(new Scheduler()),
-	num_executions(0),
-	num_feasible_executions(0),
 	diverge(NULL),
 	earliest_diverge(NULL),
 	action_trace(new action_list_t()),
@@ -393,6 +394,33 @@ void ModelChecker::print_bugs() const
 	}
 }
 
+/**
+ * @brief Record end-of-execution stats
+ *
+ * Must be run when exiting an execution. Records various stats.
+ * @see struct execution_stats
+ */
+void ModelChecker::record_stats()
+{
+	stats.num_total++;
+	if (!isfinalfeasible())
+		stats.num_infeasible++;
+	else if (have_bug_reports())
+		stats.num_buggy_executions++;
+	else if (is_complete_execution())
+		stats.num_complete++;
+}
+
+/** @brief Print execution stats */
+void ModelChecker::print_stats() const
+{
+	printf("Number of complete, bug-free executions: %d\n", stats.num_complete);
+	printf("Number of buggy executions: %d\n", stats.num_buggy_executions);
+	printf("Number of infeasible executions: %d\n", stats.num_infeasible);
+	printf("Total executions: %d\n", stats.num_total);
+	printf("Total nodes created: %d\n", node_stack->get_total_nodes());
+}
+
 /**
  * Queries the model-checker for more executions to explore and, if one
  * exists, resets the model-checker state to execute a new execution.
@@ -404,7 +432,7 @@ bool ModelChecker::next_execution()
 {
 	DBG();
 
-	num_executions++;
+	record_stats();
 
 	if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
 		printf("Earliest divergence point since last feasible execution:\n");
@@ -414,15 +442,17 @@ bool ModelChecker::next_execution()
 			printf("(Not set)\n");
 
 		earliest_diverge = NULL;
-		num_feasible_executions++;
 
 		if (is_deadlocked())
 			assert_bug("Deadlock detected");
 
 		print_bugs();
 		checkDataRaces();
+		printf("\n");
+		print_stats();
 		print_summary();
 	} else if (DBG_ENABLED()) {
+		printf("\n");
 		print_summary();
 	}
 
@@ -888,7 +918,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 
 	/* See if we have realized a data race */
 	if (checkDataRaces())
-		assert_bug("Datarace");
+		assert_bug("Data race");
 }
 
 /**
@@ -1037,7 +1067,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
-	while (!work_queue.empty()) {
+	while (!work_queue.empty() && !has_asserted()) {
 		WorkQueueEntry work = work_queue.front();
 		work_queue.pop_front();
 
@@ -1820,7 +1850,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 
 	// If we resolved promises or data races, see if we have realized a data race.
 	if (checkDataRaces())
-		assert_bug("Datarace");
+		assert_bug("Data race");
 
 	return updated;
 }
@@ -2179,11 +2209,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 		}
 	}
 
-	if (!initialized) {
-		/** @todo Need a more informative way of reporting errors. */
-		printf("ERROR: may read from uninitialized atomic\n");
-		set_assert();
-	}
+	if (!initialized)
+		assert_bug("May read from uninitialized atomic");
 
 	if (DBG_ENABLED() || !initialized) {
 		printf("Reached read action:\n");
@@ -2256,17 +2283,12 @@ void ModelChecker::dumpGraph(char *filename) {
 
 void ModelChecker::print_summary()
 {
-	printf("\n");
-	printf("Number of executions: %d\n", num_executions);
-	printf("Number of feasible executions: %d\n", num_feasible_executions);
-	printf("Total nodes created: %d\n", node_stack->get_total_nodes());
-
 #if SUPPORT_MOD_ORDER_DUMP
 	scheduler->print();
 	char buffername[100];
-	sprintf(buffername, "exec%04u", num_executions);
+	sprintf(buffername, "exec%04u", stats.num_total);
 	mo_graph->dumpGraphToFile(buffername);
-	sprintf(buffername, "graph%04u", num_executions);
+	sprintf(buffername, "graph%04u", stats.num_total);
 	dumpGraph(buffername);
 #endif