missing changes

[c11tester.git] / model.h

diff --git a/model.h b/model.h
index 19143d36d4f433c5c734652fbd8fe7ae35a51853..fec8d1f1ea55bf331017f9817515cae7e0d93c34 100644 (file)
--- a/model.h
+++ b/model.h
@@ -29,6 +29,7 @@ class Promise;
  */
 struct model_params {
        int maxreads;
+       int maxfuturedelay;
 };
 
 /**
@@ -74,11 +75,11 @@ public:
        ModelAction * get_parent_action(thread_id_t tid);
        bool next_execution();
        bool isfeasible();
+       bool isfeasibleotherthanRMW();
        bool isfinalfeasible();
        void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
        void get_release_seq_heads(ModelAction *act,
                        std::vector<const ModelAction *> *release_heads);
-
        void finish_execution();
        bool isfeasibleprefix();
        void set_assert() {asserted=true;}
@@ -87,11 +88,12 @@ public:
 private:
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler *scheduler;
-
+       
+       bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
        bool has_asserted() {return asserted;}
        void reset_asserted() {asserted=false;}
        int num_executions;
-
+       bool promises_expired();
        const model_params params;
 
        /**
@@ -115,6 +117,8 @@ private:
        bool resolve_promises(ModelAction *curr);
        void compute_promises(ModelAction *curr);
 
+
+       void check_curr_backtracking(ModelAction * curr);
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid);
        ModelAction * get_last_seq_cst(const void *location);