We don't want a global 'current_action' for saving the next action to
run; we want to stash the 'current action' for each thread. So just use
the 'pending' action in each Thread.
Note that this kinda breaks sleep sets for now. We'll have to redo this.
*/
struct model_snapshot_members {
model_snapshot_members() :
*/
struct model_snapshot_members {
model_snapshot_members() :
/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
- ModelAction *current_action;
unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
- priv->current_action->set_sleep_flag();
- thr->set_pending(priv->current_action);
+ thr->get_pending()->set_sleep_flag();
-/**
- * Stores the ModelAction for the current thread action. Call this
- * immediately before switching from user- to system-context to pass
- * data between them.
- * @param act The ModelAction created by the user-thread action
- */
-void ModelChecker::set_current_action(ModelAction *act) {
- priv->current_action = act;
-}
-
/**
* This is the heart of the model checker routine. It performs model-checking
* actions corresponding to a given "current action." Among other processes, it
/**
* This is the heart of the model checker routine. It performs model-checking
* actions corresponding to a given "current action." Among other processes, it
{
DBG();
Thread *old = thread_current();
{
DBG();
Thread *old = thread_current();
- set_current_action(act);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
exit(EXIT_FAILURE);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
exit(EXIT_FAILURE);
ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
std::memory_order_seq_cst, NULL, VALUE_NONE,
model_thread);
ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
std::memory_order_seq_cst, NULL, VALUE_NONE,
model_thread);
- set_current_action(fixup);
+ model_thread->set_pending(fixup);
if (!next_thrd)
return NULL;
if (!next_thrd)
return NULL;
- if (next_thrd->get_pending() != NULL) {
- /* restart a pending action */
- set_current_action(next_thrd->get_pending());
- next_thrd->set_pending(NULL);
- return next_thrd;
- }
-
do {
scheduler->next_thread(t);
Thread::swap(&system_context, t);
do {
scheduler->next_thread(t);
Thread::swap(&system_context, t);
- t = take_step(priv->current_action);
+
+ /* Consume the next action for a Thread */
+ ModelAction *curr = t->get_pending();
+ t->set_pending(NULL);
+ t = take_step(curr);
} while (t && !t->is_model_thread());
/** @TODO Re-write release sequence fixups here */
} while (next_execution());
} while (t && !t->is_model_thread());
/** @TODO Re-write release sequence fixups here */
} while (next_execution());
modelclock_t get_next_seq_num();
bool next_execution();
modelclock_t get_next_seq_num();
bool next_execution();
- void set_current_action(ModelAction *act);
ModelAction * check_current_action(ModelAction *curr);
bool initialize_curr_action(ModelAction **curr);
bool process_read(ModelAction *curr, bool second_part_of_rmw);
ModelAction * check_current_action(ModelAction *curr);
bool initialize_curr_action(ModelAction **curr);
bool process_read(ModelAction *curr, bool second_part_of_rmw);