From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Dec 2012 02:23:22 +0000 (-0800)
Subject: model: privatize a few interfaces
X-Git-Tag: oopsla2013~477
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=67e374f0a24b266f2ea81913770e89a4aac68ff3;p=model-checker.git

model: privatize a few interfaces

These functions were only public for ModelAction::read_from, which has
now been internalized into ModelChecker.
---

diff --git a/model.cc b/model.cc
index 2f9ec63..8c88a05 100644
--- a/model.cc
+++ b/model.cc
@@ -1913,7 +1913,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 }
 
 /**
- * A public interface for getting the release sequence head(s) with which a
+ * An interface for getting the release sequence head(s) with which a
  * given ModelAction must synchronize. This function only returns a non-empty
  * result when it can locate a release sequence head with certainty. Otherwise,
  * it may mark the internal state of the ModelChecker so that it will handle
diff --git a/model.h b/model.h
index 6bb4788..a2bbab2 100644
--- a/model.h
+++ b/model.h
@@ -118,14 +118,11 @@ public:
 	void check_promises_thread_disabled();
 	void mo_check_promises(thread_id_t tid, const ModelAction *write);
 	void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
-	void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
 	bool isfeasibleprefix() const;
 
 	bool assert_bug(const char *msg);
 	void assert_user_bug(const char *msg);
 
-	void set_bad_synchronization();
-
 	const model_params params;
 	Node * get_curr_node() const;
 
@@ -139,6 +136,7 @@ private:
 	bool mo_may_allow(const ModelAction * writer, const ModelAction *reader);
 	bool has_asserted() const;
 	void set_assert();
+	void set_bad_synchronization();
 	bool promises_expired() const;
 	void execute_sleep_set();
 	void wake_up_sleeping_actions(ModelAction * curr);
@@ -180,6 +178,7 @@ private:
 	void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
 	bool r_modification_order(ModelAction *curr, const ModelAction *rf);
 	bool w_modification_order(ModelAction *curr);
+	void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
 	bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
 	bool resolve_release_sequences(void *location, work_queue_t *work_queue);