ModelAction * get_parent_action(thread_id_t tid) const;
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 check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
bool isfeasibleprefix() const;
bool assert_bug(const char *msg);
/** The scheduler to use: tracks the running/ready Threads */
Scheduler *scheduler;
- bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
- bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
- bool mo_may_allow(const ModelAction * writer, const ModelAction *reader);
+ bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
+ bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader);
+ bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
bool has_asserted() const;
void set_assert();
void set_bad_synchronization();
bool promises_expired() const;
void execute_sleep_set();
- void wake_up_sleeping_actions(ModelAction * curr);
+ void wake_up_sleeping_actions(ModelAction *curr);
modelclock_t get_next_seq_num();
bool next_execution();
void compute_promises(ModelAction *curr);
void compute_relseq_breakwrites(ModelAction *curr);
- void check_curr_backtracking(ModelAction * curr);
+ void check_curr_backtracking(ModelAction *curr);
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid) const;
ModelAction * get_last_fence_release(thread_id_t tid) const;
bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
+ ModelAction * new_uninitialized_action(void *location) const;
+
ModelAction *diverge;
ModelAction *earliest_diverge;