model/schedule: revise 'nextThread' data flow

[model-checker.git] / model.h

diff --git a/model.h b/model.h
index 0666472d9a2ca9a441db9e3195943ad0b6158e9a..bc827fa378e6bc260d30f49def8c67420e589d58 100644 (file)
--- a/model.h
+++ b/model.h
@@ -42,8 +42,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)); }
@@ -90,7 +88,7 @@ private:
 
        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();
        bool resolve_promises(ModelAction *curr);
@@ -103,14 +101,15 @@ private:
        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);
+       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;
+       Thread *nextThread;
 
        ucontext_t system_context;
        action_list_t *action_trace;
@@ -122,6 +121,16 @@ private:
 
        HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 > *obj_thrd_map;
        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;