X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=59a07597bb5bf0436752ad6a4fca2f22d9fa2fe8;hb=507434b53b00f7d32301050dd0ce8466ad42677b;hp=d0043a1f88b1990de8e0fcdee27e21baa387ccd7;hpb=ffc110b3aaa80564dbf85f3c6a9049efd40571f1;p=model-checker.git diff --git a/model.h b/model.h index d0043a1..59a0759 100644 --- a/model.h +++ b/model.h @@ -99,6 +99,7 @@ public: bool isfeasible(); bool isfeasibleotherthanRMW(); bool isfinalfeasible(); + void check_promises_thread_disabled(); 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); @@ -139,7 +140,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);