X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=71b8b7ac0b97b2dcf4990de667f2418f29c41d94;hb=fa36db2da01d7da10e0cd375fda3c2db4ce3a05b;hp=d8c1be495075f2e276c770acab49cd7bbe29ea89;hpb=57f11820dd7dc4c3b95459a8de99305ac31f88bf;p=model-checker.git diff --git a/model.h b/model.h index d8c1be4..71b8b7a 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; @@ -176,7 +177,8 @@ private: 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(); @@ -276,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;