From f297a4e3dc814290c43671fea54a85c7a1a2aeee Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 1 Oct 2012 18:15:12 -0700 Subject: [PATCH] model: debug print - pending release sequences --- model.cc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/model.cc b/model.cc index d0dc0271..4d6d7634 100644 --- a/model.cc +++ b/model.cc @@ -188,6 +188,7 @@ bool ModelChecker::next_execution() DBG(); num_executions++; + 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++; } + DEBUG("Number of acquires waiting on pending release sequences: %lu\n", + pending_acq_rel_seq->size()); + if (isfinalfeasible() || DBG_ENABLED()) print_summary(); -- 2.34.1