+void ModelChecker::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;
+ 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()) {
+ const ModelAction * prevreadfrom = act->get_reads_from();
+ if (prevreadfrom != NULL && rf != prevreadfrom)
+ cyclegraph->addEdge(rf, prevreadfrom);
+ } else if (rf != act) {
+ cyclegraph->addEdge(rf, act);
+ }
+ break;
+ }
+ }
+ }
+}
+
+/** 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;
+ }
+ }
+}