X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=a5262d2b5c46e18e697cedf646cb0eb539fed3d6;hb=09c3eb5539455e82dcb357fbce82bf5974c3a37c;hp=c97cbf1a05f905fb79087c21b91401548b5ecf2e;hpb=8d0922f803ba8e3c093f20e5243135ea53b619f0;p=model-checker.git diff --git a/model.h b/model.h index c97cbf1..a5262d2 100644 --- a/model.h +++ b/model.h @@ -67,7 +67,8 @@ struct execution_stats { }; struct PendingFutureValue { - ModelAction *writer; + PendingFutureValue(ModelAction *writer, ModelAction *act) : writer(writer), act(act) { } + const ModelAction *writer; ModelAction *act; }; @@ -107,7 +108,7 @@ public: void add_thread(Thread *t); void remove_thread(Thread *t); Thread * get_thread(thread_id_t tid) const; - Thread * get_thread(ModelAction *act) const; + Thread * get_thread(const ModelAction *act) const; bool is_enabled(Thread *t) const; bool is_enabled(thread_id_t tid) const; @@ -120,7 +121,7 @@ public: ClockVector * get_cv(thread_id_t tid) const; 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 mo_check_promises(const ModelAction *act, bool is_read_check); void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv); bool isfeasibleprefix() const; @@ -147,7 +148,6 @@ private: modelclock_t get_next_seq_num(); bool next_execution(); - void set_current_action(ModelAction *act); ModelAction * check_current_action(ModelAction *curr); bool initialize_curr_action(ModelAction **curr); bool process_read(ModelAction *curr, bool second_part_of_rmw); @@ -159,7 +159,7 @@ private: bool read_from(ModelAction *act, const ModelAction *rf); bool check_action_enabled(ModelAction *curr); - bool take_step(ModelAction *curr); + Thread * take_step(ModelAction *curr); void check_recency(ModelAction *curr, const ModelAction *rf); ModelAction * get_last_conflict(ModelAction *act); @@ -181,12 +181,15 @@ private: ModelAction * get_last_unlock(ModelAction *curr) const; void build_reads_from_past(ModelAction *curr); ModelAction * process_rmw(ModelAction *curr); - void post_r_modification_order(ModelAction *curr, const ModelAction *rf); - bool r_modification_order(ModelAction *curr, const ModelAction *rf); + + template + bool r_modification_order(ModelAction *curr, const rf_type *rf); + bool w_modification_order(ModelAction *curr); 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 * new_uninitialized_action(void *location) const; @@ -253,8 +256,8 @@ private: struct execution_stats stats; void record_stats(); + void print_infeasibility(const char *prefix) const; bool is_feasible_prefix_ignore_relseq() const; - bool is_infeasible_ignoreRMW() const; bool is_infeasible() const; bool is_deadlocked() const; bool is_complete_execution() const;