int switch_to_master(ModelAction *act);
ClockVector * get_cv(thread_id_t tid);
+ ModelAction * get_parent_action(thread_id_t tid);
bool next_execution();
bool isfeasible();
bool isfinalfeasible();
std::vector<const ModelAction *> *release_heads);
void finish_execution();
+ bool isfeasibleprefix();
+ void set_assert() {asserted=true;}
MEMALLOC
private:
/** The scheduler to use: tracks the running/ready Threads */
Scheduler *scheduler;
+ bool has_asserted() {return asserted;}
+ void reset_asserted() {asserted=false;}
int next_thread_id;
modelclock_t used_sequence_numbers;
int num_executions;
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid);
- ModelAction * get_parent_action(thread_id_t tid);
ModelAction * get_last_seq_cst(const void *location);
void build_reads_from_past(ModelAction *curr);
ModelAction * process_rmw(ModelAction *curr);
/**
* @brief The modification order graph
*
- * A direceted acyclic graph recording observations of the modification
+ * A directed acyclic graph recording observations of the modification
* order on all the atomic objects in the system. This graph should
* never contain any cycles, as that represents a violation of the
* memory model (total ordering). This graph really consists of many
* <tt>b</tt>.
*/
CycleGraph *mo_graph;
-
bool failed_promise;
+ bool asserted;
};
extern ModelChecker *model;