model: debug print - pending release sequences
authorBrian Norris <banorris@uci.edu>
Tue, 2 Oct 2012 01:15:12 +0000 (18:15 -0700)
committerBrian Norris <banorris@uci.edu>
Wed, 3 Oct 2012 02:02:05 +0000 (19:02 -0700)
model.cc

index d0dc027..4d6d763 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -188,6 +188,7 @@ bool ModelChecker::next_execution()
        DBG();
 
        num_executions++;
        DBG();
 
        num_executions++;
+
        if (isfinalfeasible()) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
        if (isfinalfeasible()) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
@@ -199,6 +200,9 @@ bool ModelChecker::next_execution()
                num_feasible_executions++;
        }
 
                num_feasible_executions++;
        }
 
+       DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+                       pending_acq_rel_seq->size());
+
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
 
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();