model: group snapshottable ModelChecker members in struct

[c11tester.git] / model.h

diff --git a/model.h b/model.h
index 10f84c59ba6710ce1ad3a224d4d9f1784929254c..9762eb0c40ef26c5efc92887c6f4f18864e620a0 100644 (file)
--- a/model.h
+++ b/model.h
@@ -30,6 +30,17 @@ class Promise;
 struct model_params {
 };
 
+/**
+ * Structure for holding small ModelChecker members that should be snapshotted
+ */
+struct model_snapshot_members {
+       ModelAction *current_action;
+       int next_thread_id;
+       modelclock_t used_sequence_numbers;
+       Thread *nextThread;
+       ModelAction *next_backtrack;
+};
+
 /** @brief The central structure for model-checking */
 class ModelChecker {
 public:
@@ -42,8 +53,6 @@ public:
        /** Prints an execution summary with trace information. */
        void print_summary();
 
-       Thread * schedule_next_thread();
-
        void add_thread(Thread *t);
        void remove_thread(Thread *t);
        Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); }
@@ -57,20 +66,25 @@ public:
 
        int switch_to_master(ModelAction *act);
        ClockVector * get_cv(thread_id_t tid);
+       ModelAction * get_parent_action(thread_id_t tid);
        bool next_execution();
        bool isfeasible();
        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;}
 
        MEMALLOC
 private:
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler *scheduler;
 
-       int next_thread_id;
-       modelclock_t used_sequence_numbers;
+       bool has_asserted() {return asserted;}
+       void reset_asserted() {asserted=false;}
        int num_executions;
 
        const model_params params;
@@ -81,32 +95,32 @@ private:
         * data between them.
         * @param act The ModelAction created by the user-thread action
         */
-       void set_current_action(ModelAction *act) { current_action = act; }
-       void check_current_action();
+       void set_current_action(ModelAction *act) { priv->current_action = act; }
+       Thread * check_current_action(ModelAction *curr);
 
        bool take_step();
 
        ModelAction * get_last_conflict(ModelAction *act);
        void set_backtracking(ModelAction *act);
-       thread_id_t get_next_replay_thread();
+       Thread * get_next_replay_thread();
        ModelAction * get_next_backtrack();
        void reset_to_initial_state();
-       void resolve_promises(ModelAction *curr);
+       bool resolve_promises(ModelAction *curr);
        void compute_promises(ModelAction *curr);
 
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid);
-       ModelAction * get_parent_action(thread_id_t tid);
        ModelAction * get_last_seq_cst(const void *location);
        void build_reads_from_past(ModelAction *curr);
-       ModelAction * process_rmw(ModelAction * curr);
-       void post_r_modification_order(ModelAction * curr, const ModelAction *rf);
-       void r_modification_order(ModelAction * curr, const ModelAction *rf);
-       void w_modification_order(ModelAction * curr);
+       ModelAction * process_rmw(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);
+       bool release_seq_head(const ModelAction *rf,
+                       std::vector<const ModelAction *> *release_heads) const;
+       bool resolve_release_sequences(void *location);
 
-       ModelAction *current_action;
        ModelAction *diverge;
-       thread_id_t nextThread;
 
        ucontext_t system_context;
        action_list_t *action_trace;
@@ -117,12 +131,41 @@ private:
        HashTable<const void *, action_list_t, uintptr_t, 4> *obj_map;
 
        HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 > *obj_thrd_map;
-       std::vector<Promise *> * promises;
+       std::vector<Promise *> *promises;
+
+       /**
+        * Collection of lists of objects that might synchronize with one or
+        * more release sequence. Release sequences might be determined lazily
+        * as promises are fulfilled and modification orders are established.
+        * This structure maps its lists by object location. Each ModelAction
+        * in the lists should be an acquire operation.
+        */
+       HashTable<void *, std::list<ModelAction *>, uintptr_t, 4> *lazy_sync_with_release;
+
        std::vector<ModelAction *> *thrd_last_action;
        NodeStack *node_stack;
-       ModelAction *next_backtrack;
+
+       /** Private data members that should be snapshotted. They are grouped
+        * together for efficiency and maintainability. */
+       struct model_snapshot_members *priv;
+
+       /**
+        * @brief The modification order graph
+        *
+        * A directed acyclic graph recording observations of the modification
+        * order on all the atomic objects in the system. This graph should
+        * never contain any cycles, as that represents a violation of the
+        * memory model (total ordering). This graph really consists of many
+        * disjoint (unconnected) subgraphs, each graph corresponding to a
+        * separate ordering on a distinct object.
+        *
+        * The edges in this graph represent the "ordered before" relation,
+        * such that <tt>a --> b</tt> means <tt>a</tt> was ordered before
+        * <tt>b</tt>.
+        */
        CycleGraph *mo_graph;
        bool failed_promise;
+       bool asserted;
 };
 
 extern ModelChecker *model;