model: add get_last_seq_cst_fence
authorBrian Norris <banorris@uci.edu>
Sat, 1 Dec 2012 02:46:28 +0000 (18:46 -0800)
committerBrian Norris <banorris@uci.edu>
Mon, 3 Dec 2012 20:28:45 +0000 (12:28 -0800)
model.cc
model.h

index 39af266..fc86d5c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1997,6 +1997,35 @@ ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
        return NULL;
 }
 
        return NULL;
 }
 
+/**
+ * Gets the last memory_order_seq_cst fence (in the total global sequence)
+ * performed in a particular thread, prior to a particular fence.
+ * @param tid The ID of the thread to check
+ * @param before_fence The fence from which to begin the search; if NULL, then
+ * search for the most recent fence in the thread.
+ * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
+ */
+ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
+{
+       /* All fences should have NULL location */
+       action_list_t *list = get_safe_ptr_action(obj_map, NULL);
+       action_list_t::reverse_iterator rit = list->rbegin();
+
+       if (before_fence) {
+               for (; rit != list->rend(); rit++)
+                       if (*rit == before_fence)
+                               break;
+
+               ASSERT(*rit == before_fence);
+               rit++;
+       }
+
+       for (; rit != list->rend(); rit++)
+               if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
+                       return *rit;
+       return NULL;
+}
+
 /**
  * Gets the last unlock operation performed on a particular mutex (i.e., memory
  * location). This function identifies the mutex according to the current
 /**
  * Gets the last unlock operation performed on a particular mutex (i.e., memory
  * location). This function identifies the mutex according to the current
diff --git a/model.h b/model.h
index d0e47d9..11afba9 100644 (file)
--- a/model.h
+++ b/model.h
@@ -171,6 +171,7 @@ private:
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid) const;
        ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid) const;
        ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
+       ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const;
        ModelAction * get_last_unlock(ModelAction *curr) const;
        void build_reads_from_past(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
        ModelAction * get_last_unlock(ModelAction *curr) const;
        void build_reads_from_past(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);