- Promise * pop_promise_to_resolve(const ModelAction *curr);
- bool resolve_promise(ModelAction *curr, Promise *promise);
- void compute_promises(ModelAction *curr);
- void compute_relseq_breakwrites(ModelAction *curr);
-
- void mo_check_promises(const ModelAction *act, bool is_read_check);
- void thread_blocking_check_promises(Thread *blocker, Thread *waiting);
-
- 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;
- ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
- ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const;
- ModelAction * get_last_unlock(ModelAction *curr) const;
- void build_may_read_from(ModelAction *curr);
- ModelAction * process_rmw(ModelAction *curr);
-
- template <typename rf_type>
- bool r_modification_order(ModelAction *curr, const rf_type *rf);
-
- bool w_modification_order(ModelAction *curr, ModelVector<ModelAction *> *send_fv);
- void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
- 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);
- void add_future_value(const ModelAction *writer, ModelAction *reader);
-
- ModelAction * get_uninitialized_action(const ModelAction *curr) const;
-
- ModelAction *diverge;
- ModelAction *earliest_diverge;