X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=ab16bf82528ea5ebf30766970b37faca5a6ada1f;hb=3133d403d1abd0ac735b4d4662708fcef1cb5d5f;hp=922a0d60e6daf360360c83852f70ee7e47f3cf4f;hpb=45206350b4022732229f8a48a3c7b08885e874a7;p=model-checker.git

diff --git a/model.cc b/model.cc
index 922a0d6..ab16bf8 100644
--- a/model.cc
+++ b/model.cc
@@ -18,6 +18,20 @@
 
 ModelChecker *model;
 
+struct bug_message {
+	bug_message(const char *str) {
+		const char *fmt = "  [BUG] %s\n";
+		msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
+		sprintf(msg, fmt, str);
+	}
+	~bug_message() { if (msg) snapshot_free(msg); }
+
+	char *msg;
+	void print() { printf("%s", msg); }
+
+	SNAPSHOTALLOC
+};
+
 /**
  * Structure for holding small ModelChecker members that should be snapshotted
  */
@@ -27,6 +41,8 @@ struct model_snapshot_members {
 	modelclock_t used_sequence_numbers;
 	Thread *nextThread;
 	ModelAction *next_backtrack;
+	std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
+	struct execution_stats stats;
 };
 
 /** @brief Constructor */
@@ -34,16 +50,14 @@ 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()),
 	thread_map(new HashTable<int, Thread *, int>()),
-	obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
-	lock_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
-	condvar_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
-	obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
+	obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
+	lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
+	condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
+	obj_thrd_map(new HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 >()),
 	promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
 	futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
 	pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
@@ -56,7 +70,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	bad_synchronization(false)
 {
 	/* Allocate this "size" on the snapshotting heap */
-	priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
+	priv = (struct model_snapshot_members *)snapshot_calloc(1, sizeof(*priv));
 	/* First thread created will have id INITIAL_THREAD_ID */
 	priv->next_thread_id = INITIAL_THREAD_ID;
 
@@ -88,6 +102,29 @@ ModelChecker::~ModelChecker()
 	delete node_stack;
 	delete scheduler;
 	delete mo_graph;
+
+	for (unsigned int i = 0; i < priv->bugs.size(); i++)
+		delete priv->bugs[i];
+	priv->bugs.clear();
+	snapshot_free(priv);
+}
+
+static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
+	action_list_t * tmp=hash->get(ptr);
+	if (tmp==NULL) {
+		tmp=new action_list_t();
+		hash->put(ptr, tmp);
+	}
+	return tmp;
+}
+
+static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr) {
+	std::vector<action_list_t> * tmp=hash->get(ptr);
+	if (tmp==NULL) {
+		tmp=new std::vector<action_list_t>();
+		hash->put(ptr, tmp);
+	}
+	return tmp;
 }
 
 /**
@@ -276,6 +313,114 @@ bool ModelChecker::is_deadlocked() const
 	return blocking_threads;
 }
 
+/**
+ * Check if this is a complete execution. That is, have all thread completed
+ * execution (rather than exiting because sleep sets have forced a redundant
+ * execution).
+ *
+ * @return True if the execution is complete.
+ */
+bool ModelChecker::is_complete_execution() const
+{
+	for (unsigned int i = 0; i < get_num_threads(); i++)
+		if (is_enabled(int_to_id(i)))
+			return false;
+	return true;
+}
+
+/**
+ * @brief Assert a bug in the executing program.
+ *
+ * Use this function to assert any sort of bug in the user program. If the
+ * current trace is feasible (actually, a prefix of some feasible execution),
+ * then this execution will be aborted, printing the appropriate message. If
+ * the current trace is not yet feasible, the error message will be stashed and
+ * printed if the execution ever becomes feasible.
+ *
+ * This function can also be used to immediately trigger the bug; that is, we
+ * don't wait for a feasible execution before aborting. Only use the
+ * "immediate" option when you know that the infeasibility is justified (e.g.,
+ * pending release sequences are not a problem)
+ *
+ * @param msg Descriptive message for the bug (do not include newline char)
+ * @param user_thread Was this assertion triggered from a user thread?
+ * @param immediate Should this bug be triggered immediately?
+ */
+void ModelChecker::assert_bug(const char *msg, bool user_thread, bool immediate)
+{
+	priv->bugs.push_back(new bug_message(msg));
+
+	if (immediate || isfeasibleprefix()) {
+		set_assert();
+		if (user_thread)
+			switch_to_master(NULL);
+	}
+}
+
+/**
+ * @brief Assert a bug in the executing program, with a default message
+ * @see ModelChecker::assert_bug
+ * @param user_thread Was this assertion triggered from a user thread?
+ */
+void ModelChecker::assert_bug(bool user_thread)
+{
+	assert_bug("bug detected", user_thread);
+}
+
+/**
+ * @brief Assert a bug in the executing program immediately
+ * @see ModelChecker::assert_bug
+ * @param msg Descriptive message for the bug (do not include newline char)
+ */
+void ModelChecker::assert_bug_immediate(const char *msg)
+{
+	printf("Feasible: %s\n", isfeasibleprefix() ? "yes" : "no");
+	assert_bug(msg, false, true);
+}
+
+/** @return True, if any bugs have been reported for this execution */
+bool ModelChecker::have_bug_reports() const
+{
+	return priv->bugs.size() != 0;
+}
+
+/** @brief Print bug report listing for this execution (if any bugs exist) */
+void ModelChecker::print_bugs() const
+{
+	if (have_bug_reports()) {
+		printf("Bug report: %zu bugs detected\n", priv->bugs.size());
+		for (unsigned int i = 0; i < priv->bugs.size(); i++)
+			priv->bugs[i]->print();
+	}
+}
+
+/**
+ * @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.
@@ -287,11 +432,9 @@ bool ModelChecker::next_execution()
 {
 	DBG();
 
-	num_executions++;
+	record_stats();
 
-	if (is_deadlocked())
-		printf("ERROR: DEADLOCK\n");
-	if (isfinalfeasible()) {
+	if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
 		printf("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
 			earliest_diverge->print();
@@ -299,15 +442,17 @@ bool ModelChecker::next_execution()
 			printf("(Not set)\n");
 
 		earliest_diverge = NULL;
-		num_feasible_executions++;
-	}
 
-	DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
-			pending_rel_seqs->size());
+		if (is_deadlocked())
+			assert_bug("Deadlock detected");
 
-
-	if (isfinalfeasible() || DBG_ENABLED()) {
+		print_bugs();
 		checkDataRaces();
+		printf("\n");
+		print_stats();
+		print_summary();
+	} else if (DBG_ENABLED()) {
+		printf("\n");
 		print_summary();
 	}
 
@@ -330,7 +475,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -342,7 +487,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 	case ATOMIC_LOCK:
 	case ATOMIC_TRYLOCK: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -353,7 +498,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 	}
 	case ATOMIC_UNLOCK: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -364,7 +509,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 	}
 	case ATOMIC_WAIT: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -379,7 +524,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 	case ATOMIC_NOTIFY_ALL:
 	case ATOMIC_NOTIFY_ONE: {
 		/* linear search: from most recent to oldest */
-		action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
@@ -562,10 +707,8 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 	}
 		//otherwise fall into the lock case
 	case ATOMIC_LOCK: {
-		if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
-			printf("Lock access before initialization\n");
-			set_assert();
-		}
+		if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+			assert_bug("Lock access before initialization");
 		state->islocked = true;
 		ModelAction *unlock = get_last_unlock(curr);
 		//synchronize with the previous unlock statement
@@ -579,7 +722,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 		//unlock the lock
 		state->islocked = false;
 		//wake up the other threads
-		action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
+		action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
 		//activate all the waiting threads
 		for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 			scheduler->wake(get_thread(*rit));
@@ -591,7 +734,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 		//unlock the lock
 		state->islocked = false;
 		//wake up the other threads
-		action_list_t *waiters = lock_waiters_map->get_safe_ptr((void *) curr->get_value());
+		action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
 		//activate all the waiting threads
 		for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 			scheduler->wake(get_thread(*rit));
@@ -599,14 +742,14 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 		waiters->clear();
 		//check whether we should go to sleep or not...simulate spurious failures
 		if (curr->get_node()->get_misc()==0) {
-			condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
+			get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
 			//disable us
 			scheduler->sleep(get_current_thread());
 		}
 		break;
 	}
 	case ATOMIC_NOTIFY_ALL: {
-		action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location());
+		action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
 		//activate all the waiting threads
 		for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 			scheduler->wake(get_thread(*rit));
@@ -615,7 +758,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 		break;
 	}
 	case ATOMIC_NOTIFY_ONE: {
-		action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location());
+		action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
 		int wakeupthread=curr->get_node()->get_misc();
 		action_list_t::iterator it = waiters->begin();
 		advance(it, wakeupthread);
@@ -775,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())
-		set_assert();
+		assert_bug("Data race");
 }
 
 /**
@@ -839,7 +982,7 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
 		else if (newcurr->is_wait())
 			newcurr->get_node()->set_misc_max(2);
 		else if (newcurr->is_notify_one()) {
-			newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
+			newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
 		}
 		return true; /* This was a new ModelAction */
 	}
@@ -861,7 +1004,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 		struct std::mutex_state * state = lock->get_state();
 		if (state->islocked) {
 			//Stick the action in the appropriate waiting queue
-			lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
+			get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
 			return false;
 		}
 	} else if (curr->get_type() == THREAD_JOIN) {
@@ -924,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();
 
@@ -1005,7 +1148,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
 	}
 }
 
-bool ModelChecker::promises_expired() {
+bool ModelChecker::promises_expired() const
+{
 	for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
 		Promise *promise = (*promises)[promise_index];
 		if (promise->get_expiration()<priv->used_sequence_numbers) {
@@ -1017,12 +1161,14 @@ bool ModelChecker::promises_expired() {
 
 /** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
-bool ModelChecker::isfeasibleprefix() {
+bool ModelChecker::isfeasibleprefix() const
+{
 	return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
 }
 
 /** @return whether the current partial trace is feasible. */
-bool ModelChecker::isfeasible() {
+bool ModelChecker::isfeasible() const
+{
 	if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
 		DEBUG("Infeasible: RMW violation\n");
 
@@ -1031,7 +1177,8 @@ bool ModelChecker::isfeasible() {
 
 /** @return whether the current partial trace is feasible other than
  * multiple RMW reading from the same store. */
-bool ModelChecker::isfeasibleotherthanRMW() {
+bool ModelChecker::isfeasibleotherthanRMW() const
+{
 	if (DBG_ENABLED()) {
 		if (mo_graph->checkForCycles())
 			DEBUG("Infeasible: modification order cycles\n");
@@ -1048,7 +1195,8 @@ bool ModelChecker::isfeasibleotherthanRMW() {
 }
 
 /** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() {
+bool ModelChecker::isfinalfeasible() const
+{
 	if (DBG_ENABLED() && promises->size() != 0)
 		DEBUG("Infeasible: unrevolved promises\n");
 
@@ -1086,7 +1234,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
 		//accidentally clear by rolling back
 		if (!isfeasible())
 			return;
-		std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+		std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 		int tid = id_to_int(curr->get_tid());
 
 		/* Skip checks */
@@ -1178,7 +1326,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
  */
 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
 {
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
 	bool added = false;
 	ASSERT(curr->is_read());
@@ -1237,7 +1385,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
  */
 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
 {
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
 	ASSERT(curr->is_read());
 
@@ -1308,7 +1456,7 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
  */
 bool ModelChecker::w_modification_order(ModelAction *curr)
 {
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
 	bool added = false;
 	ASSERT(curr->is_write());
@@ -1430,7 +1578,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  */
 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
 {
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
 	unsigned int i;
 	/* Iterate over all threads */
 	for (i = 0; i < thrd_lists->size(); i++) {
@@ -1522,7 +1670,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 	/* else relaxed write; check modification order for contiguous subsequence
 	 * -> rf must be same thread as release */
 	int tid = id_to_int(rf->get_tid());
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
 	action_list_t *list = &(*thrd_lists)[tid];
 	action_list_t::const_reverse_iterator rit;
 
@@ -1701,9 +1849,8 @@ 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()) {
-		set_assert();
-	}
+	if (checkDataRaces())
+		assert_bug("Data race");
 
 	return updated;
 }
@@ -1720,9 +1867,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 	int tid = id_to_int(act->get_tid());
 	action_trace->push_back(act);
 
-	obj_map->get_safe_ptr(act->get_location())->push_back(act);
+	get_safe_ptr_action(obj_map, act->get_location())->push_back(act);
 
-	std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
+	std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
 	if (tid >= (int)vec->size())
 		vec->resize(priv->next_thread_id);
 	(*vec)[tid].push_back(act);
@@ -1733,9 +1880,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 
 	if (act->is_wait()) {
 		void *mutex_loc=(void *) act->get_value();
-		obj_map->get_safe_ptr(mutex_loc)->push_back(act);
+		get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
 
-		std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
+		std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
 		if (tid >= (int)vec->size())
 			vec->resize(priv->next_thread_id);
 		(*vec)[tid].push_back(act);
@@ -1771,7 +1918,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
 ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
 {
 	void *location = curr->get_location();
-	action_list_t *list = obj_map->get_safe_ptr(location);
+	action_list_t *list = get_safe_ptr_action(obj_map, 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++)
@@ -1791,7 +1938,7 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
 {
 	void *location = curr->get_location();
-	action_list_t *list = obj_map->get_safe_ptr(location);
+	action_list_t *list = get_safe_ptr_action(obj_map, 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++)
@@ -2013,7 +2160,7 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
  */
 void ModelChecker::build_reads_from_past(ModelAction *curr)
 {
-	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
 	ASSERT(curr->is_read());
 
@@ -2062,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");
@@ -2139,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
 
@@ -2266,6 +2405,10 @@ bool ModelChecker::take_step() {
 	/* Infeasible -> don't take any more steps */
 	if (!isfeasible())
 		return false;
+	else if (isfeasibleprefix() && have_bug_reports()) {
+		set_assert();
+		return false;
+	}
 
 	if (params.bound != 0) {
 		if (priv->used_sequence_numbers > params.bound) {