X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=8ff9d375838b193bec751f9b7f0d419a89f07a8d;hb=79f51bf7df7ed2c8095b0c2d7f730db6ccb9394a;hp=01dd35b03752504dc9416543f38588018297adf6;hpb=075d78a2e09fd11b8b78b6c7b3852a42a279c4f2;p=model-checker.git diff --git a/model.h b/model.h index 01dd35b..8ff9d37 100644 --- a/model.h +++ b/model.h @@ -112,6 +112,7 @@ public: const model_params params; Scheduler * get_scheduler() { return scheduler;} + Node * get_curr_node(); MEMALLOC private: @@ -138,7 +139,7 @@ private: */ void set_current_action(ModelAction *act) { priv->current_action = act; } Thread * check_current_action(ModelAction *curr); - ModelAction * initialize_curr_action(ModelAction *curr); + bool initialize_curr_action(ModelAction **curr); bool process_read(ModelAction *curr, bool second_part_of_rmw); bool process_write(ModelAction *curr); bool process_mutex(ModelAction *curr); @@ -186,6 +187,10 @@ private: * to a trace of all actions performed on the object. */ HashTable *lock_waiters_map; + /** Per-object list of actions. Maps an object (i.e., memory location) + * to a trace of all actions performed on the object. */ + HashTable *condvar_waiters_map; + HashTable, uintptr_t, 4 > *obj_thrd_map; std::vector< Promise *, SnapshotAlloc > *promises; std::vector< struct PendingFutureValue, SnapshotAlloc > *futurevalues;