/** Prints an execution summary with trace information. */
void print_summary();
- Thread * schedule_next_thread();
-
void add_thread(Thread *t);
void remove_thread(Thread *t);
Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); }
int switch_to_master(ModelAction *act);
ClockVector * get_cv(thread_id_t tid);
+ ModelAction * get_parent_action(thread_id_t tid);
bool next_execution();
bool isfeasible();
bool isfinalfeasible();
* @param act The ModelAction created by the user-thread action
*/
void set_current_action(ModelAction *act) { current_action = act; }
- void check_current_action();
+ Thread * check_current_action(ModelAction *curr);
bool take_step();
ModelAction * get_last_conflict(ModelAction *act);
void set_backtracking(ModelAction *act);
- thread_id_t get_next_replay_thread();
+ Thread * get_next_replay_thread();
ModelAction * get_next_backtrack();
void reset_to_initial_state();
bool resolve_promises(ModelAction *curr);
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid);
- ModelAction * get_parent_action(thread_id_t tid);
ModelAction * get_last_seq_cst(const void *location);
void build_reads_from_past(ModelAction *curr);
ModelAction * process_rmw(ModelAction *curr);
bool w_modification_order(ModelAction *curr);
bool release_seq_head(const ModelAction *rf,
std::vector<const ModelAction *> *release_heads) const;
+ bool resolve_release_sequences(void *location);
ModelAction *current_action;
ModelAction *diverge;
- thread_id_t nextThread;
+ Thread *nextThread;
ucontext_t system_context;
action_list_t *action_trace;