- action_list_t *list = &action_trace;
- sllnode<ModelAction *> * rit;
- /* Find X : is_read(X) && X --sb-> curr */
- for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
- ModelAction *act = rit->getVal();
- if (act == curr)
- continue;
- if (act->get_tid() != curr->get_tid())
- continue;
- /* Stop at the beginning of the thread */
- if (act->is_thread_start())
- break;
- /* Stop once we reach a prior fence-acquire */
- if (act->is_fence() && act->is_acquire())
- break;
- if (!act->is_read())
- continue;
- /* read-acquire will find its own release sequences */
- if (act->is_acquire())
- continue;
-
- /* Establish hypothetical release sequences */
- ClockVector *cv = get_hb_from_write(act->get_reads_from());
- if (cv != NULL && curr->get_cv()->merge(cv))
- updated = true;
- }