From: Brian Norris <banorris@uci.edu>
Date: Tue, 16 Apr 2013 00:38:45 +0000 (-0700)
Subject: model: remove public check_promises() interface
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=07b041c2dd6958bb3a52ffcba07e8e642130548c

model: remove public check_promises() interface
---

diff --git a/action.cc b/action.cc
index 8384101..2750edf 100644
--- a/action.cc
+++ b/action.cc
@@ -501,7 +501,6 @@ bool ModelAction::synchronize_with(const ModelAction *act)
 {
 	if (*this < *act)
 		return false;
-	model->check_promises(act->get_tid(), cv, act->cv);
 	cv->merge(act->cv);
 	return true;
 }
diff --git a/model.cc b/model.cc
index f0c844c..afb72b0 100644
--- a/model.cc
+++ b/model.cc
@@ -1446,11 +1446,12 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
  */
 bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second)
 {
-	if (!second->synchronize_with(first)) {
+	if (*second < *first) {
 		set_bad_synchronization();
 		return false;
 	}
-	return true;
+	check_promises(first->get_tid(), second->get_cv(), first->get_cv());
+	return second->synchronize_with(first);
 }
 
 /**
diff --git a/model.h b/model.h
index 3327683..f4961d8 100644
--- a/model.h
+++ b/model.h
@@ -98,7 +98,6 @@ public:
 	ClockVector * get_cv(thread_id_t tid) const;
 	ModelAction * get_parent_action(thread_id_t tid) const;
 	void check_promises_thread_disabled();
-	void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
 	bool isfeasibleprefix() const;
 
 	bool assert_bug(const char *msg, ...);
@@ -168,6 +167,7 @@ private:
 	void compute_promises(ModelAction *curr);
 	void compute_relseq_breakwrites(ModelAction *curr);
 
+	void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
 	void mo_check_promises(const ModelAction *act, bool is_read_check);
 	void thread_blocking_check_promises(Thread *blocker, Thread *waiting);