/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
- nextThread(NULL),
next_backtrack(NULL),
bugs(),
stats(),
ModelAction *current_action;
unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
- Thread *nextThread;
ModelAction *next_backtrack;
std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
struct execution_stats stats;
thr->set_pending(priv->current_action);
}
}
- priv->current_action = NULL;
}
void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
record_stats();
/* Output */
- if (DBG_ENABLED() || params.verbose || have_bug_reports())
+ if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
print_execution(complete);
else
clear_program_output();
continue;
}
/* Cache the latest backtracking point */
- if (!priv->next_backtrack || *prev > *priv->next_backtrack)
- priv->next_backtrack = prev;
+ set_latest_backtrack(prev);
/* If this is a new backtracking point, mark the tree */
if (!node->set_backtrack(tid))
}
}
+/**
+ * @brief Cache the a backtracking point as the "most recent", if eligible
+ *
+ * Note that this does not prepare the NodeStack for this backtracking
+ * operation, it only caches the action on a per-execution basis
+ *
+ * @param act The operation at which we should explore a different next action
+ * (i.e., backtracking point)
+ * @return True, if this action is now the most recent backtracking point;
+ * false otherwise
+ */
+bool ModelChecker::set_latest_backtrack(ModelAction *act)
+{
+ if (!priv->next_backtrack || *act > *priv->next_backtrack) {
+ priv->next_backtrack = act;
+ return true;
+ }
+ return false;
+}
+
/**
* Returns last backtracking point. The model checker will explore a different
* path for this point in the next execution.
for (unsigned int i = 0; i < futurevalues->size(); i++) {
struct PendingFutureValue pfv = (*futurevalues)[i];
//Do more ambitious checks now that mo is more complete
- if (mo_may_allow(pfv.writer, pfv.act)&&
- pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
- (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
- priv->next_backtrack = pfv.act;
+ if (mo_may_allow(pfv.writer, pfv.act) &&
+ pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
+ set_latest_backtrack(pfv.act);
}
futurevalues->resize(0);
}
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
- if ((!parnode->backtrack_empty() ||
+ if (!parnode->backtrack_empty() ||
!currnode->misc_empty() ||
!currnode->read_from_empty() ||
!currnode->future_value_empty() ||
!currnode->promise_empty() ||
- !currnode->relseq_break_empty())
- && (!priv->next_backtrack ||
- *curr > *priv->next_backtrack)) {
- priv->next_backtrack = curr;
+ !currnode->relseq_break_empty()) {
+ set_latest_backtrack(curr);
}
}
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (!reader->happens_before(act))
+ /* Don't disallow due to act == reader */
+ if (!reader->happens_before(act) || reader == act)
break;
else if (act->is_write())
write_after_read = act;
- else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
+ else if (act->is_read() && act->get_reads_from() != NULL)
write_after_read = act->get_reads_from();
- }
}
if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
}
#if SUPPORT_MOD_ORDER_DUMP
-void ModelChecker::dumpGraph(char *filename) {
+void ModelChecker::dumpGraph(char *filename) const
+{
char buffer[200];
sprintf(buffer, "%s.dot",filename);
FILE *file = fopen(buffer, "w");
/**
* Takes the next step in the execution, if possible.
+ * @param curr The current step to take
* @return Returns true (success) if a step was taken and false otherwise.
*/
-bool ModelChecker::take_step() {
+bool ModelChecker::take_step(ModelAction *curr)
+{
if (has_asserted())
return false;
- Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
- if (curr) {
- ASSERT(curr->get_state() == THREAD_READY);
+ Thread *curr_thrd = get_thread(curr);
+ ASSERT(curr_thrd->get_state() == THREAD_READY);
- priv->nextThread = check_current_action(priv->current_action);
- priv->current_action = NULL;
+ Thread *next_thrd = check_current_action(curr);
- if (curr->is_blocked() || curr->is_complete())
- scheduler->remove_thread(curr);
- }
- Thread *next = scheduler->next_thread(priv->nextThread);
+ if (curr_thrd->is_blocked() || curr_thrd->is_complete())
+ scheduler->remove_thread(curr_thrd);
+
+ next_thrd = scheduler->next_thread(next_thrd);
/* Infeasible -> don't take any more steps */
if (is_infeasible())
}
}
- DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
- next ? id_to_int(next->get_id()) : -1);
+ DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
+ next_thrd ? id_to_int(next_thrd->get_id()) : -1);
/*
* Launch end-of-execution release sequence fixups only when there are:
* (3) pending assertions (i.e., data races)
* (4) no pending promises
*/
- if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
+ if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
pending_rel_seqs->size());
return true;
}
- /* next == NULL -> don't take any more steps */
- if (!next)
+ /* next_thrd == NULL -> don't take any more steps */
+ if (!next_thrd)
return false;
- next->set_state(THREAD_RUNNING);
+ next_thrd->set_state(THREAD_RUNNING);
- if (next->get_pending() != NULL) {
+ if (next_thrd->get_pending() != NULL) {
/* restart a pending action */
- set_current_action(next->get_pending());
- next->set_pending(NULL);
- next->set_state(THREAD_READY);
+ set_current_action(next_thrd->get_pending());
+ next_thrd->set_pending(NULL);
+ next_thrd->set_state(THREAD_READY);
return true;
}
/* Return false only if swap fails with an error */
- return (Thread::swap(&system_context, next) == 0);
+ return (Thread::swap(&system_context, next_thrd) == 0);
}
/** Wrapper to run the user's main function, with appropriate arguments */
{
do {
thrd_t user_thread;
+ Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
+
+ add_thread(t);
- /* Start user program */
- add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
+ /* Run user thread up to its first action */
+ scheduler->next_thread(t);
+ Thread::swap(&system_context, t);
/* Wait for all threads to complete */
- while (take_step());
+ while (take_step(priv->current_action));
} while (next_execution());
print_stats();
projects / model-checker.git / blobdiff