X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=8ff9d375838b193bec751f9b7f0d419a89f07a8d;hb=ed57a438e07bae54e5ce1862c830461ddda626f2;hp=d6c033725dedf36bed645f5615f19d45444b2f07;hpb=1b793f0683aff025afe2e19519572e3599575a19;p=model-checker.git diff --git a/model.h b/model.h index d6c0337..8ff9d37 100644 --- a/model.h +++ b/model.h @@ -139,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); @@ -187,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;