X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=62c762711bcb8300765483ee075ec9747d412d5f;hb=12b1a10eeff58161619bafcfd8e288b3e2c76621;hp=6f082c66a71653f7240fcf8102223f60845e870f;hpb=eb3b6cccf71b9eeee035e2c98566dfa279e402ae;p=model-checker.git diff --git a/model.h b/model.h index 6f082c6..62c7627 100644 --- a/model.h +++ b/model.h @@ -10,23 +10,22 @@ #include #include -#include "schedule.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 *, MyAlloc > rel_heads_list_t; +typedef std::vector< const ModelAction *, ModelAlloc > rel_heads_list_t; /** * Model checker parameter structure. Holds run-time configuration options for @@ -73,15 +72,12 @@ public: 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)); } - Thread * get_thread(ModelAction *act) { return get_thread(act->get_tid()); } + Thread * get_thread(thread_id_t tid); + Thread * get_thread(ModelAction *act); thread_id_t get_next_id(); int get_num_threads(); - modelclock_t get_next_seq_num(); - - /** @return The currently executing Thread. */ - Thread * get_current_thread() { return scheduler->get_current_thread(); } + Thread * get_current_thread(); int switch_to_master(ModelAction *act); ClockVector * get_cv(thread_id_t tid); @@ -114,6 +110,8 @@ private: int num_feasible_executions; bool promises_expired(); + modelclock_t get_next_seq_num(); + /** * Stores the ModelAction for the current thread action. Call this * immediately before switching from user- to system-context to pass