local commit... bug that prunes too many executions

[cdsspec-compiler.git] / model.h

diff --git a/model.h b/model.h
index 23c42ebb199a6ce30b5859b80ca8d5537038d0a3..dfc8e36c2be5e775ec82dab1e81a8adcfdaa2697 100644 (file)
--- a/model.h
+++ b/model.h
@@ -11,19 +11,18 @@
 #include <ucontext.h>
 
 #include "mymemory.h"
-#include "libthreads.h"
-#include "threads.h"
 #include "action.h"
-#include "clockvector.h"
 #include "hashtable.h"
 #include "workqueue.h"
 #include "config.h"
+#include "modeltypes.h"
 
 /* Forward declaration */
 class NodeStack;
 class CycleGraph;
 class Promise;
 class Scheduler;
+class Thread;
 
 /** @brief Shorthand for a list of release sequence heads */
 typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
@@ -50,7 +49,7 @@ struct PendingFutureValue {
  */
 struct model_snapshot_members {
        ModelAction *current_action;
-       int next_thread_id;
+       unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
        Thread *nextThread;
        ModelAction *next_backtrack;
@@ -73,11 +72,11 @@ public:
 
        void add_thread(Thread *t);
        void remove_thread(Thread *t);
-       Thread * get_thread(thread_id_t tid);
-       Thread * get_thread(ModelAction *act);
+       Thread * get_thread(thread_id_t tid) const;
+       Thread * get_thread(ModelAction *act) const;
 
        thread_id_t get_next_id();
-       int get_num_threads();
+       unsigned int get_num_threads();
        Thread * get_current_thread();
 
        int switch_to_master(ModelAction *act);
@@ -87,7 +86,8 @@ public:
        bool isfeasible();
        bool isfeasibleotherthanRMW();
        bool isfinalfeasible();
-       void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
+       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);
        void finish_execution();
        bool isfeasibleprefix();
@@ -98,6 +98,7 @@ public:
        void set_bad_synchronization() { bad_synchronization = true; }
 
        const model_params params;
+       Scheduler * get_scheduler() { return scheduler;}
 
        MEMALLOC
 private:
@@ -149,7 +150,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);
-       bool release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+       bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
        void do_complete_join(ModelAction *join);