model: remove public check_promises() interface

diff --git a/action.cc b/action.cc
index 8384101a4d54581475600aa77fac2a94efa479b3..2750edf13b685e728c946d093e8352c70bfc8151 100644 (file)
--- 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 f0c844cdcb019057cf6c110ad64a9d1d74cf4a4a..afb72b0aae490bda4a0464bb04837b380d81f4ca 100644 (file)
--- 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 3327683e65efb21c2fe716c6ccc6fbef1cc8dc8f..f4961d80cfd70d31ff041c88b747cbc6794ab0da 100644 (file)
--- 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);