last_fence_release(NULL),
node(NULL),
seq_number(ACTION_INITIAL_CLOCK),
- cv(NULL),
- sleep_flag(false)
+ cv(NULL)
{
/* References to NULL atomic variables can end up here */
ASSERT(loc || type == ATOMIC_FENCE);
void process_rmw(ModelAction * act);
void copy_typeandorder(ModelAction * act);
- void set_sleep_flag() { sleep_flag=true; }
- bool get_sleep_flag() { return sleep_flag; }
unsigned int hash() const;
bool equals(const ModelAction *x) const { return this == x; }
* vectors for all operations.
*/
ClockVector *cv;
-
- bool sleep_flag;
};
#endif /* __ACTION_H__ */
return scheduler->select_next_thread(node_stack->get_head());
}
-/**
- * We need to know what the next actions of all threads in the sleep
- * set will be. This method computes them and stores the actions at
- * the corresponding thread object's pending action.
- */
-void ModelChecker::execute_sleep_set()
-{
- for (unsigned int i = 0; i < get_num_threads(); i++) {
- thread_id_t tid = int_to_id(i);
- Thread *thr = get_thread(tid);
- if (scheduler->is_sleep_set(thr) && thr->get_pending()) {
- thr->get_pending()->set_sleep_flag();
- }
- }
-}
-
/**
* @brief Assert a bug in the executing program.
*
unsigned int get_num_threads() const;
- void execute_sleep_set();
-
bool next_execution();
bool should_terminate_execution();