-/**
- * Switch from a user-context to the "master thread" context (a.k.a. system
- * context). This switch is made with the intention of exploring a particular
- * model-checking action (described by a ModelAction object). Must be called
- * from a user-thread context.
- *
- * @param act The current action that will be explored. May be NULL only if
- * trace is exiting via an assertion (see ModelExecution::set_assert and
- * ModelExecution::has_asserted).
- * @return Return the value returned by the current action
- */
-uint64_t ModelChecker::switch_to_master(ModelAction *act)
+/* Swap back to system_context and terminate this execution */
+void ModelChecker::finishRunExecution(Thread *old)
+{
+ scheduler->set_current_thread(NULL);
+
+ /** If we have more executions, we won't make it past this call. */
+ finish_execution(execution_number < params.maxexecutions);
+
+
+ /** We finished the final execution. Print stuff and exit. */
+ model_print("******* Model-checking complete: *******\n");
+ print_stats();
+
+ /* Have the trace analyses dump their output. */
+ for (unsigned int i = 0;i < trace_analyses.size();i++)
+ trace_analyses[i]->finish();
+
+ /* unlink tmp file created by last child process */
+ char filename[256];
+ snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
+ unlink(filename);
+
+ /* Exit. */
+ _Exit(0);
+}
+
+void ModelChecker::consumeAction()
+{
+ ModelAction *curr = chosen_thread->get_pending();
+ chosen_thread->set_pending(NULL);
+ chosen_thread = execution->take_step(curr);
+}
+
+/* Allow pending relaxed/release stores or thread actions to perform first */
+void ModelChecker::chooseThread(ModelAction *act, Thread *thr)
+{
+ if (!thread_chosen && act && execution->is_enabled(thr) && (thr->get_state() != THREAD_BLOCKED) ) {
+ if (act->is_write()) {
+ std::memory_order order = act->get_mo();
+ if (order == std::memory_order_relaxed || \
+ order == std::memory_order_release) {
+ chosen_thread = thr;
+ thread_chosen = true;
+ }
+ } else if (act->get_type() == THREAD_CREATE || \
+ act->get_type() == PTHREAD_CREATE || \
+ act->get_type() == THREAD_START || \
+ act->get_type() == THREAD_FINISH) {
+ chosen_thread = thr;
+ thread_chosen = true;
+ }
+ }
+}
+
+uint64_t ModelChecker::switch_thread(ModelAction *act)