priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
/* First thread created will have id INITIAL_THREAD_ID */
priv->next_thread_id = INITIAL_THREAD_ID;
+
+ /* Initialize a model-checker thread, for special ModelActions */
+ model_thread = new Thread(get_next_id());
+ thread_map->put(id_to_int(model_thread->get_id()), model_thread);
}
/** @brief Destructor */
earliest_diverge=diverge;
Node *nextnode = next->get_node();
+ Node *prevnode = nextnode->get_parent();
+ scheduler->update_sleep_set(prevnode);
+
/* Reached divergence point */
if (nextnode->increment_promise()) {
/* The next node will try to satisfy a different set of promises. */
node_stack->pop_restofstack(2);
} else {
/* Make a different thread execute for next step */
- Node *node = nextnode->get_parent();
- tid = node->get_next_backtrack();
+ scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
+ tid = prevnode->get_next_backtrack();
+ /* Make sure the backtracked thread isn't sleeping. */
+ scheduler->remove_sleep(thread_map->get(id_to_int(tid)));
node_stack->pop_restofstack(1);
if (diverge==earliest_diverge) {
- earliest_diverge=node->get_action();
+ earliest_diverge=prevnode->get_action();
}
}
+ /* The correct sleep set is in the parent node. */
+ execute_sleep_set();
+
DEBUG("*** Divergence point ***\n");
diverge = NULL;
return thread_map->get(id_to_int(tid));
}
+/**
+ * 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->get_enabled(thr) == THREAD_SLEEP_SET ) {
+ thr->set_state(THREAD_RUNNING);
+ scheduler->next_thread(thr);
+ Thread::swap(&system_context, thr);
+ thr->set_pending(priv->current_action);
+ }
+ }
+ priv->current_action = NULL;
+}
+
+void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
+ 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->get_enabled(thr) == THREAD_SLEEP_SET ) {
+ ModelAction *pending_act=thr->get_pending();
+ if (pending_act->could_synchronize_with(curr)) {
+ //Remove this thread from sleep set
+ scheduler->remove_sleep(thr);
+ }
+ }
+ }
+}
+
/**
* Queries the model-checker for more executions to explore and, if one
* exists, resets the model-checker state to execute a new execution.
return NULL;
}
-/** This method find backtracking points where we should try to
+/** This method finds backtracking points where we should try to
* reorder the parameter ModelAction against.
*
* @param the ModelAction to find backtracking points for.
for(int i = low_tid; i < high_tid; i++) {
thread_id_t tid = int_to_id(i);
+
if (!node->is_enabled(tid))
continue;
-
+
/* Check if this has been explored already */
if (node->has_been_explored(tid))
continue;
if (unfair)
continue;
}
-
/* Cache the latest backtracking point */
if (!priv->next_backtrack || *prev > *priv->next_backtrack)
priv->next_backtrack = prev;
ASSERT(release->same_thread(rf));
if (write == NULL) {
+ /**
+ * @todo Forcing a synchronization requires that we set
+ * modification order constraints. For instance, we can't allow
+ * a fixup sequence in which two separate read-acquire
+ * operations read from the same sequence, where the first one
+ * synchronizes and the other doesn't. Essentially, we can't
+ * allow any writes to insert themselves between 'release' and
+ * 'rf'
+ */
+
/* Must synchronize */
if (!acquire->synchronize_with(release)) {
set_bad_synchronization();
mo_graph->addEdge(release, write);
mo_graph->addEdge(write, rf);
}
+
+ /* See if we have realized a data race */
+ if (checkDataRaces())
+ set_assert();
}
/**
Thread * ModelChecker::check_current_action(ModelAction *curr)
{
ASSERT(curr);
-
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
if (!check_action_enabled(curr)) {
return get_next_thread(NULL);
}
+ wake_up_sleeping_actions(curr);
+
ModelAction *newcurr = initialize_curr_action(curr);
+
/* Add the action to lists before any other model-checking tasks */
if (!second_part_of_rmw)
add_action_to_lists(newcurr);
/* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
-
while (!work_queue.empty()) {
WorkQueueEntry work = work_queue.front();
work_queue.pop_front();
}
check_curr_backtracking(curr);
-
set_backtracking(curr);
-
return get_next_thread(curr);
}
th->is_complete())
future_ordered = true;
+ ASSERT(!th->is_model_thread() || future_ordered);
+
for (rit = list->rbegin(); rit != list->rend(); rit++) {
const ModelAction *act = *rit;
/* Reach synchronization -> this thread is complete */
if (has_asserted())
return false;
- Thread *curr = thread_current();
+ Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
if (curr) {
if (curr->get_state() == THREAD_READY) {
ASSERT(priv->current_action);
DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
next ? id_to_int(next->get_id()) : -1);
+ /*
+ * Launch end-of-execution release sequence fixups only when there are:
+ *
+ * (1) no more user threads to run (or when execution replay chooses
+ * the 'model_thread')
+ * (2) pending release sequences
+ * (3) pending assertions (i.e., data races)
+ * (4) no pending promises
+ */
+ if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
+ isfinalfeasible() && !unrealizedraces.empty()) {
+ printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+ pending_rel_seqs->size());
+ ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
+ std::memory_order_seq_cst, NULL, VALUE_NONE,
+ model_thread);
+ set_current_action(fixup);
+ return true;
+ }
+
/* next == NULL -> don't take any more steps */
if (!next)
return false;
projects / model-checker.git / blobdiff