+void ModelChecker::continueRunExecution(Thread *old)
+{
+
+ if (params.traceminsize != 0 &&
+ execution->get_curr_seq_num() > checkfree) {
+ checkfree += params.checkthreshold;
+ execution->collectActions();
+ }
+
+ thread_chosen = false;
+ curr_thread_num = 1;
+ Thread *thr = getNextThread();
+ if (thr != nullptr) {
+ scheduler->set_current_thread(thr);
+ if (Thread::swap(old, thr) < 0) {
+ perror("swap threads");
+ exit(EXIT_FAILURE);
+ }
+ } else
+ handleChosenThread(old);
+}
+
+void ModelChecker::startRunExecution(ucontext_t *old)
+{
+
+ if (params.traceminsize != 0 &&
+ execution->get_curr_seq_num() > checkfree) {
+ checkfree += params.checkthreshold;
+ execution->collectActions();
+ }
+
+ thread_chosen = false;
+ curr_thread_num = 1;
+ Thread *thr = getNextThread();
+ if (thr != nullptr) {
+ scheduler->set_current_thread(thr);
+ if (Thread::swap(old, thr) < 0) {
+ perror("swap threads");
+ exit(EXIT_FAILURE);
+ }
+ } else
+ handleChosenThread(old);
+}
+
+Thread* ModelChecker::getNextThread()
+{
+ Thread *nextThread = nullptr;
+ for (unsigned int i = curr_thread_num; i < get_num_threads(); i++) {
+ thread_id_t tid = int_to_id(i);
+ Thread *thr = get_thread(tid);
+
+ if (!thr->is_complete() && !thr->get_pending()) {
+ curr_thread_num = i;
+ nextThread = thr;
+ break;
+ }
+ ModelAction *act = thr->get_pending();
+
+ if (act && execution->is_enabled(thr) && !execution->check_action_enabled(act)) {
+ scheduler->sleep(thr);
+ }
+
+ chooseThread(act, thr);
+ }
+ return nextThread;
+}
+
+void ModelChecker::finishRunExecution(Thread *old)
+{
+ scheduler->set_current_thread(NULL);
+ if (Thread::swap(old, &system_context) < 0) {
+ perror("swap threads");
+ exit(EXIT_FAILURE);
+ }
+}
+
+void ModelChecker::finishRunExecution(ucontext_t *old)
+{
+ scheduler->set_current_thread(NULL);
+ break_execution = true;
+}
+
+void ModelChecker::consumeAction()
+{
+ ModelAction *curr = chosen_thread->get_pending();
+ Thread * th = thread_current();
+ if (curr->get_type() == THREAD_FINISH && th != NULL) {
+ // Thread finish must be consumed in the master context
+ scheduler->set_current_thread(NULL);
+ if (Thread::swap(th, &system_context) < 0) {
+ perror("swap threads");
+ exit(EXIT_FAILURE);
+ }
+ } else {
+ chosen_thread->set_pending(NULL);
+ chosen_thread = execution->take_step(curr);
+ }
+}
+
+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;
+ }
+ }
+}
+