From: Brian Norris <banorris@uci.edu>
Date: Tue, 2 Oct 2012 01:15:12 +0000 (-0700)
Subject: model: debug print - pending release sequences
X-Git-Tag: pldi2013~116
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=f297a4e3dc814290c43671fea54a85c7a1a2aeee;ds=sidebyside

model: debug print - pending release sequences
---

diff --git a/model.cc b/model.cc
index d0dc027..4d6d763 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();