action/model: backtrack for seq-cst and release/acquire fences

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 700f25c017b1d44aa310eee2f4518c7e051abf1c..e92cd4b32e3bcc77e8f2389f03f89108ab97537d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -172,7 +172,7 @@ unsigned int ModelChecker::get_num_threads() const
 }
 
 /** @return The currently executing Thread. */
-Thread * ModelChecker::get_current_thread()
+Thread * ModelChecker::get_current_thread() const
 {
        return scheduler->get_current_thread();
 }
@@ -183,7 +183,8 @@ modelclock_t ModelChecker::get_next_seq_num()
        return ++priv->used_sequence_numbers;
 }
 
-Node * ModelChecker::get_curr_node() {
+Node * ModelChecker::get_curr_node() const
+{
        return node_stack->get_head();
 }
 
@@ -520,6 +521,7 @@ bool ModelChecker::next_execution()
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
        switch (act->get_type()) {
+       case ATOMIC_FENCE:
        case ATOMIC_READ:
        case ATOMIC_WRITE:
        case ATOMIC_RMW: {
@@ -1534,7 +1536,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
        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);
+               ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
                if (last_seq_cst != NULL) {
                        mo_graph->addEdge(last_seq_cst, curr);
                        added = true;
@@ -1984,7 +1986,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
  * check
  * @return The last seq_cst write
  */
-ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
+ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
 {
        void *location = curr->get_location();
        action_list_t *list = get_safe_ptr_action(obj_map, location);
@@ -1996,6 +1998,35 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
        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
@@ -2016,7 +2047,7 @@ ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
        return NULL;
 }
 
-ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
+ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
 {
        ModelAction *parent = get_last_action(tid);
        if (!parent)
@@ -2029,7 +2060,7 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
  * @param tid The thread whose clock vector we want
  * @return Desired clock vector
  */
-ClockVector * ModelChecker::get_cv(thread_id_t tid)
+ClockVector * ModelChecker::get_cv(thread_id_t tid) const
 {
        return get_parent_action(tid)->get_cv();
 }
@@ -2233,16 +2264,16 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        unsigned int i;
        ASSERT(curr->is_read());
 
-       ModelAction *last_seq_cst = NULL;
+       ModelAction *last_sc_write = NULL;
 
        /* Track whether this object has been initialized */
        bool initialized = false;
 
        if (curr->is_seqcst()) {
-               last_seq_cst = get_last_seq_cst(curr);
+               last_sc_write = get_last_seq_cst_write(curr);
                /* We have to at least see the last sequentially consistent write,
                         so we are initialized. */
-               if (last_seq_cst != NULL)
+               if (last_sc_write != NULL)
                        initialized = true;
        }
 
@@ -2259,15 +2290,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                continue;
 
                        /* Don't consider more than one seq_cst write if we are a seq_cst read. */
-                       if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
-                               if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
-                                       DEBUG("Adding action to may_read_from:\n");
-                                       if (DBG_ENABLED()) {
-                                               act->print();
-                                               curr->print();
-                                       }
-                                       curr->get_node()->add_read_from(act);
+                       bool allow_read = true;
+
+                       if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
+                               allow_read = false;
+                       else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
+                               allow_read = false;
+
+                       if (allow_read) {
+                               DEBUG("Adding action to may_read_from:\n");
+                               if (DBG_ENABLED()) {
+                                       act->print();
+                                       curr->print();
                                }
+                               curr->get_node()->add_read_from(act);
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */