notes: fence: add release/acquire fence notes

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index dbca58e7394f5e3eb9a4f7b68a54c67aff4a5346..715a2584f36a1538528489d60f987142ad0f2a77 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -858,6 +858,56 @@ bool ModelChecker::process_write(ModelAction *curr)
        return updated_mod_order || updated_promises;
 }
 
+/**
+ * Process a fence ModelAction
+ * @param curr The ModelAction to process
+ * @return True if synchronization was updated
+ */
+bool ModelChecker::process_fence(ModelAction *curr)
+{
+       /*
+        * fence-relaxed: no-op
+        * fence-release: only log the occurence (not in this function), for
+        *   use in later synchronization
+        * fence-acquire (this function): search for hypothetical release
+        *   sequences
+        */
+       bool updated = false;
+       if (curr->is_acquire()) {
+               action_list_t *list = action_trace;
+               action_list_t::reverse_iterator rit;
+               /* Find X : is_read(X) && X --sb-> curr */
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *act = *rit;
+                       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 */
+                       rel_heads_list_t release_heads;
+                       get_release_seq_heads(curr, act, &release_heads);
+                       for (unsigned int i = 0; i < release_heads.size(); i++)
+                               if (!curr->synchronize_with(release_heads[i]))
+                                       set_bad_synchronization();
+                       if (release_heads.size() != 0)
+                               updated = true;
+               }
+       }
+       return updated;
+}
+
 /**
  * @brief Process the current action for thread-related activity
  *
@@ -1173,6 +1223,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        if (act->is_write() && process_write(act))
                                update = true;
 
+                       if (act->is_fence() && process_fence(act))
+                               update_all = true;
+
                        if (act->is_mutex_op() && process_mutex(act))
                                update_all = true;
 
@@ -1464,18 +1517,21 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
                                                *act < *last_sc_fence_thread_local) {
                                        mo_graph->addEdge(act, rf);
                                        added = true;
+                                       break;
                                }
                                /* C++, Section 29.3 statement 4 */
                                else if (act->is_seqcst() && last_sc_fence_local &&
                                                *act < *last_sc_fence_local) {
                                        mo_graph->addEdge(act, rf);
                                        added = true;
+                                       break;
                                }
                                /* C++, Section 29.3 statement 6 */
                                else if (last_sc_fence_thread_before &&
                                                *act < *last_sc_fence_thread_before) {
                                        mo_graph->addEdge(act, rf);
                                        added = true;
+                                       break;
                                }
                        }
 
@@ -1652,6 +1708,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                        *act < *last_sc_fence_thread_before) {
                                mo_graph->addEdge(act, curr);
                                added = true;
+                               break;
                        }
 
                        /*