+/** Updates the cyclegraph with the constraints imposed from the
+ * current read. */
+void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelAction *rf) {
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ unsigned int i;
+ ASSERT(curr->is_read());
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ ModelAction *lastact = NULL;
+
+ /* Find last action that happens after curr */
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+ if (curr->happens_before(act)) {
+ lastact = act;
+ } else
+ break;
+ }
+
+ /* Include at most one act per-thread that "happens before" curr */
+ if (lastact != NULL) {
+ if (lastact->is_read()) {
+ const ModelAction * postreadfrom = lastact->get_reads_from();
+ if (postreadfrom != NULL&&rf != postreadfrom)
+ cyclegraph->addEdge(postreadfrom, rf);
+ } else if (rf != lastact) {
+ cyclegraph->addEdge(lastact, rf);
+ }
+ break;
+ }
+ }
+}
+
+/**
+ * Updates the cyclegraph with the constraints imposed from the current write.
+ * @param curr The current action. Must be a write.
+ */
+void ModelChecker::w_modification_order(ModelAction * curr) {
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ unsigned int i;
+ ASSERT(curr->is_write());
+
+ if (curr->is_seqcst()) {
+ /* We have to at least see the last sequentially consistent write,
+ so we are initialized. */
+ ModelAction * last_seq_cst = get_last_seq_cst(curr->get_location());
+ if (last_seq_cst != NULL)
+ cyclegraph->addEdge(curr, last_seq_cst);
+ }
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+
+ /* Include at most one act per-thread that "happens before" curr */
+ if (act->happens_before(curr)) {
+ if (act->is_read())
+ cyclegraph->addEdge(curr, act->get_reads_from());
+ else
+ cyclegraph->addEdge(curr, act);
+ break;
+ } else if (act->is_read() && !act->is_synchronizing(curr) &&
+ !act->same_thread(curr)) {
+ /* We have an action that:
+ (1) did not happen before us
+ (2) is a read and we are a write
+ (3) cannot synchronize with us
+ (4) is in a different thread
+ =>
+ that read could potentially read from our write.
+ */
+ if (act->get_node()->add_future_value(curr->get_value()) &&
+ (!next_backtrack || *act > *next_backtrack))
+ next_backtrack = act;
+ }
+ }
+ }
+}
+
+/**
+ * Performs various bookkeeping operations for the current ModelAction. For
+ * instance, adds action to the per-object, per-thread action vector and to the
+ * action trace list of all thread actions.
+ *
+ * @param act is the ModelAction to add.
+ */