projects
/
c11tester.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model, nodestack: bugfix - retain UNINIT actions across executions
[c11tester.git]
/
model.h
diff --git
a/model.h
b/model.h
index 115d94455c23737d949bcab4667a8bede791e037..ae9706b124067e18e5098e0fbd7e7859fce05d73 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-38,6
+38,7
@@
typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;
struct model_params {
int maxreads;
int maxfuturedelay;
struct model_params {
int maxreads;
int maxfuturedelay;
+ bool yieldon;
unsigned int fairwindow;
unsigned int enabledcount;
unsigned int bound;
unsigned int fairwindow;
unsigned int enabledcount;
unsigned int bound;
@@
-167,11
+168,17
@@
private:
Thread * take_step(ModelAction *curr);
Thread * take_step(ModelAction *curr);
- bool check_recency(ModelAction *curr, const ModelAction *rf) const;
+ template <typename T>
+ bool check_recency(ModelAction *curr, const T *rf) const;
+
+ template <typename T, typename U>
+ 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);
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();
bool set_latest_backtrack(ModelAction *act);
ModelAction * get_next_backtrack();
void reset_to_initial_state();
@@
-202,7
+209,7
@@
private:
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
void add_future_value(const ModelAction *writer, ModelAction *reader);
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;
ModelAction *diverge;
ModelAction *earliest_diverge;
@@
-271,6
+278,7
@@
private:
bool is_feasible_prefix_ignore_relseq() const;
bool is_infeasible() const;
bool is_deadlocked() const;
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;
bool is_complete_execution() const;
bool have_bug_reports() const;
void print_bugs() const;