*/
struct model_snapshot_members {
ModelAction *current_action;
- int next_thread_id;
+ unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
Thread *nextThread;
ModelAction *next_backtrack;
};
+/** @brief Records information regarding a single pending release sequence */
+struct release_seq {
+ /** @brief The acquire operation */
+ ModelAction *acquire;
+ /** @brief The head of the RMW chain from which 'acquire' reads; may be
+ * equal to 'release' */
+ const ModelAction *rf;
+ /** @brief The head of the potential longest release sequence chain */
+ const ModelAction *release;
+ /** @brief The write(s) that may break the release sequence */
+ std::vector<const ModelAction *> writes;
+};
+
/** @brief The central structure for model-checking */
class ModelChecker {
public:
void add_thread(Thread *t);
void remove_thread(Thread *t);
- Thread * get_thread(thread_id_t tid);
- Thread * get_thread(ModelAction *act);
+ Thread * get_thread(thread_id_t tid) const;
+ Thread * get_thread(ModelAction *act) const;
thread_id_t get_next_id();
- int get_num_threads();
+ unsigned int get_num_threads();
Thread * get_current_thread();
int switch_to_master(ModelAction *act);
bool isfeasible();
bool isfeasibleotherthanRMW();
bool isfinalfeasible();
- void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
+ 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);
void finish_execution();
bool isfeasibleprefix();
void set_bad_synchronization() { bad_synchronization = true; }
const model_params params;
+ Scheduler * get_scheduler() { return scheduler;}
MEMALLOC
private:
void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
bool r_modification_order(ModelAction *curr, const ModelAction *rf);
bool w_modification_order(ModelAction *curr);
- bool release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+ bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
void do_complete_join(ModelAction *join);