+ add_action_to_lists(newcurr);
+
+ /* Build may_read_from set for newly-created actions */
+ if (curr == newcurr && curr->is_read())
+ build_reads_from_past(curr);
+ curr = 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();
+
+ switch (work.type) {
+ case WORK_CHECK_CURR_ACTION: {
+ ModelAction *act = work.action;
+ bool update = false; /* update this location's release seq's */
+ bool update_all = false; /* update all release seq's */
+
+ if (process_thread_action(curr))
+ update_all = true;
+
+ 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()) {
+ const ModelAction *rf = act->get_reads_from();
+ if (rf != NULL && r_modification_order(act, rf))
+ 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;
+ }
+ }