X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=ae9706b124067e18e5098e0fbd7e7859fce05d73;hb=e6789461057e3395ba78575b85c114b553f4ed19;hp=3f4ca001aa8c85d85564cf012d10bf37b6182614;hpb=745b71256a4b96ddf4843c7f66b11d0cb3daa3cb;p=c11tester.git diff --git a/model.h b/model.h index 3f4ca001..ae9706b1 100644 --- a/model.h +++ b/model.h @@ -38,6 +38,7 @@ typedef std::list< ModelAction *, SnapshotAlloc > action_list_t; struct model_params { int maxreads; int maxfuturedelay; + bool yieldon; unsigned int fairwindow; unsigned int enabledcount; unsigned int bound; @@ -167,15 +168,17 @@ private: Thread * take_step(ModelAction *curr); - bool check_recency(ModelAction *curr, const ModelAction *rf) const; - template - bool should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const; + bool check_recency(ModelAction *curr, const T *rf) const; + + template + bool should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const; ModelAction * get_last_fence_conflict(ModelAction *act) const; ModelAction * get_last_conflict(ModelAction *act) const; void set_backtracking(ModelAction *act); - Thread * get_next_thread(ModelAction *curr); + Thread * action_select_next_thread(const ModelAction *curr) const; + Thread * get_next_thread(); bool set_latest_backtrack(ModelAction *act); ModelAction * get_next_backtrack(); void reset_to_initial_state(); @@ -206,7 +209,7 @@ private: 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; + ModelAction * get_uninitialized_action(const ModelAction *curr) const; ModelAction *diverge; ModelAction *earliest_diverge; @@ -275,6 +278,7 @@ private: bool is_feasible_prefix_ignore_relseq() const; bool is_infeasible() const; bool is_deadlocked() const; + bool is_circular_wait(const Thread *t) const; bool is_complete_execution() const; bool have_bug_reports() const; void print_bugs() const;