model: privatize a few interfaces
authorBrian Norris <banorris@uci.edu>
Tue, 4 Dec 2012 02:23:22 +0000 (18:23 -0800)
committerBrian Norris <banorris@uci.edu>
Tue, 4 Dec 2012 02:26:48 +0000 (18:26 -0800)
These functions were only public for ModelAction::read_from, which has
now been internalized into ModelChecker.

model.cc
model.h

index 2f9ec63..8c88a05 100644 (file)
--- 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
  * 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 (file)
--- 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 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);
 
        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;
 
        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();
        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);
        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 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);
 
        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);