From: Brian Norris <banorris@uci.edu>
Date: Sat, 15 Dec 2012 01:28:40 +0000 (-0800)
Subject: clean up some DEBUG() messages
X-Git-Tag: oopsla2013~409
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=9d9c0f4e9909c2f58889e198a065479003f7bced;hp=ac8e176cd4a8756244c12dbbcaf961d27bfc8a74

clean up some DEBUG() messages

We were printing may_read_from info twice.

Printing the current action when we get to check_current_action() is
helpful.

Printing scheduling based on priority is also useful, as we recently had
a "bug" involving fairness/priority.

Include the file name in DEBUG() prints, since we may have the same
function names in different files/classes.
---

diff --git a/common.h b/common.h
index 9c1e1ed..c861285 100644
--- a/common.h
+++ b/common.h
@@ -13,7 +13,7 @@ extern FILE *model_out;
 #define model_print(fmt, ...) do { fprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
 
 #ifdef CONFIG_DEBUG
-#define DEBUG(fmt, ...) do { model_print("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0)
+#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0)
 #define DBG() DEBUG("\n")
 #define DBG_ENABLED() (1)
 #else
diff --git a/libthreads.cc b/libthreads.cc
index 05cca86..fce87da 100644
--- a/libthreads.cc
+++ b/libthreads.cc
@@ -11,10 +11,8 @@
 int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
 {
 	Thread *thread;
-	DBG();
 	thread = new Thread(t, start_routine, arg);
 	model->add_thread(thread);
-	DEBUG("create thread %d\n", id_to_int(thrd_to_id(*t)));
 	/* seq_cst is just a 'don't care' parameter */
 	model->switch_to_master(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, thread, VALUE_NONE));
 	return 0;
diff --git a/model.cc b/model.cc
index 843034d..1fe7126 100644
--- a/model.cc
+++ b/model.cc
@@ -1211,6 +1211,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	bool newly_explored = initialize_curr_action(&curr);
 
+	DBG();
+	if (DBG_ENABLED())
+		curr->print();
+
 	wake_up_sleeping_actions(curr);
 
 	/* Add the action to lists before any other model-checking tasks */
@@ -2504,14 +2508,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 			else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
 				allow_read = false;
 
-			if (allow_read) {
-				DEBUG("Adding action to may_read_from:\n");
-				if (DBG_ENABLED()) {
-					act->print();
-					curr->print();
-				}
+			if (allow_read)
 				curr->get_node()->add_read_from(act);
-			}
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr))
diff --git a/schedule.cc b/schedule.cc
index 9f69272..444e1a8 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -168,6 +168,7 @@ Thread * Scheduler::next_thread(Thread *t)
 		for (int i = 0; i < enabled_len; i++) {
 			thread_id_t tid = int_to_id(i);
 			if (n->has_priority(tid)) {
+				DEBUG("Node (tid %d) has priority\n", i);
 				//Have a thread with priority
 				if (enabled[i] != THREAD_DISABLED)
 					have_enabled_thread_with_priority = true;