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 9c1e1ed384e199fd5e8761d8a37a34ab6787ad61..c861285a8ab12c3c73720e357679ec84d4bc8269 100644 (file)
--- 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 05cca8646a3daf69db7c2992e70e540c893dccf2..fce87daf5bc0d8969d4546ce6837a30dda4019eb 100644 (file)
--- 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 843034d31acec815eb8c8943d6910eb074103f0b..1fe7126c66b2f974c6c6d38602aeb521a7d67743 100644 (file)
--- 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 9f692728aa916d820d3d9c38d80f8c591aee9396..444e1a82982535339f241d5eb203fddf1d00a15a 100644 (file)
--- 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;