};
struct PendingFutureValue {
- PendingFutureValue(ModelAction *writer, ModelAction *act) : writer(writer), act(act) { }
+ PendingFutureValue(ModelAction *writer, ModelAction *reader) :
+ writer(writer), reader(reader)
+ { }
const ModelAction *writer;
- ModelAction *act;
+ ModelAction *reader;
};
/** @brief Records information regarding a single pending release sequence */
void dumpGraph(char *filename) const;
#endif
- void add_thread(Thread *t);
- void remove_thread(Thread *t);
Thread * get_thread(thread_id_t tid) const;
Thread * get_thread(const ModelAction *act) const;
int get_promise_number(const Promise *promise) const;
/** The scheduler to use: tracks the running/ready Threads */
Scheduler * const scheduler;
+ void add_thread(Thread *t);
+
bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
- bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader);
+ bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const;
bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
+ bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
bool has_asserted() const;
void set_assert();
void set_bad_synchronization();
bool set_latest_backtrack(ModelAction *act);
ModelAction * get_next_backtrack();
void reset_to_initial_state();
- int get_promise_to_resolve(const ModelAction *curr) const;
- bool resolve_promise(ModelAction *curr, unsigned int promise_idx);
+ Promise * pop_promise_to_resolve(const ModelAction *curr);
+ bool resolve_promise(ModelAction *curr, Promise *promise);
void compute_promises(ModelAction *curr);
void compute_relseq_breakwrites(ModelAction *curr);