+ if (act->is_read() && process_read(act, second_part_of_rmw))
+ update = true;
+
+ if (act->is_write() && process_write(act))
+ update = true;
+
+ if (act->is_mutex_op() && process_mutex(act))
+ update_all = true;
+
+ if (update_all)
+ work_queue.push_back(CheckRelSeqWorkEntry(NULL));
+ else if (update)
+ work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
+ break;
+ }
+ case WORK_CHECK_RELEASE_SEQ:
+ resolve_release_sequences(work.location, &work_queue);
+ break;
+ case WORK_CHECK_MO_EDGES: {
+ /** @todo Complete verification of work_queue */
+ ModelAction *act = work.action;
+ bool updated = false;
+
+ if (act->is_read()) {
+ if (r_modification_order(act, act->get_reads_from()))
+ updated = true;
+ }
+ if (act->is_write()) {
+ if (w_modification_order(act))
+ updated = true;
+ }
+ mo_graph->commitChanges();
+
+ if (updated)
+ work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
+ break;
+ }
+ default:
+ ASSERT(false);
+ break;
+ }
+ }
+
+ check_curr_backtracking(curr);
+
+ set_backtracking(curr);
+
+ return get_next_thread(curr);
+}
+
+/**
+ * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
+ * operation from the Thread it is joining with. Must be called after the
+ * completion of the Thread in question.
+ * @param join The THREAD_JOIN action
+ */
+void ModelChecker::do_complete_join(ModelAction *join)
+{
+ Thread *blocking = (Thread *)join->get_location();
+ ModelAction *act = get_last_action(blocking->get_id());
+ join->synchronize_with(act);
+}
+
+void ModelChecker::check_curr_backtracking(ModelAction * curr) {