X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=e3d9203eea60ec53010d67bb87da20331cfbf642;hp=8d8944d71ab27e59af1108e2a66debd3d6999596;hb=a27eec056d90e248a071bea6912e5ab09dea8242;hpb=ec80014245d22f726e4d66a89b6bd6d293db177c

diff --git a/model.cc b/model.cc
index 8d8944d..e3d9203 100644
--- a/model.cc
+++ b/model.cc
@@ -178,7 +178,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 	} else {
 		tid = next->get_tid();
 	}
-	DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
+	DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
 	ASSERT(tid != THREAD_ID_T_NONE);
 	return thread_map->get(id_to_int(tid));
 }
@@ -199,7 +199,7 @@ bool ModelChecker::next_execution()
 	if (isfinalfeasible()) {
 		printf("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
-			earliest_diverge->print(false);
+			earliest_diverge->print();
 		else
 			printf("(Not set)\n");
 
@@ -324,7 +324,8 @@ void ModelChecker::set_backtracking(ModelAction *act)
 		if (!node->set_backtrack(tid))
 			continue;
 		DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-					prev->get_tid(), t->get_id());
+					id_to_int(prev->get_tid()),
+					id_to_int(t->get_id()));
 		if (DBG_ENABLED()) {
 			prev->print();
 			act->print();
@@ -794,8 +795,7 @@ bool ModelChecker::isfinalfeasible() {
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
-	int tid = id_to_int(act->get_tid());
-	ModelAction *lastread = get_last_action(tid);
+	ModelAction *lastread = get_last_action(act->get_tid());
 	lastread->process_rmw(act);
 	if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
 		mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
@@ -1176,7 +1176,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * @return true, if the ModelChecker is certain that release_heads is complete;
  * false otherwise
  */
-bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
+bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
 {
 	/* Only check for release sequences if there are no cycles */
 	if (mo_graph->checkForCycles())
@@ -1246,7 +1246,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 
 		ModelAction *last = get_last_action(int_to_id(i));
 		if (last && (rf->happens_before(last) ||
-				last->get_type() == THREAD_FINISH))
+				get_thread(int_to_id(i))->is_complete()))
 			future_ordered = true;
 
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
@@ -1298,13 +1298,13 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
  * @param act The 'acquire' action that may read from a release sequence
  * @param release_heads A pass-by-reference return parameter. Will be filled
  * with the head(s) of the release sequence(s), if they exists with certainty.
- * @see ModelChecker::release_seq_head
+ * @see ModelChecker::release_seq_heads
  */
 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
 {
 	const ModelAction *rf = act->get_reads_from();
 	bool complete;
-	complete = release_seq_head(rf, release_heads);
+	complete = release_seq_heads(rf, release_heads);
 	if (!complete) {
 		/* add act to 'lazy checking' list */
 		pending_acq_rel_seq->push_back(act);
@@ -1340,7 +1340,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 		const ModelAction *rf = act->get_reads_from();
 		rel_heads_list_t release_heads;
 		bool complete;
-		complete = release_seq_head(rf, &release_heads);
+		complete = release_seq_heads(rf, &release_heads);
 		for (unsigned int i = 0; i < release_heads.size(); i++) {
 			if (!act->has_synchronized_with(release_heads[i])) {
 				if (act->synchronize_with(release_heads[i]))
@@ -1776,7 +1776,8 @@ bool ModelChecker::take_step() {
 	if (!isfeasible())
 		return false;
 
-	DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+	DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
+			next ? id_to_int(next->get_id()) : -1);
 
 	/* next == NULL -> don't take any more steps */
 	if (!next)