model: add process_fence()

process_fence() will only handle fence-acquire. Fence-relaxed is a
no-op; fence-release is only logged for later use; and fence-seq-cst
takes release/acquire semantics, plus some mo-graph rules which apply to
reads/reads (see {r,w}_modification_order).

diff --git a/model.cc b/model.cc
index dbca58e7394f5e3eb9a4f7b68a54c67aff4a5346..6120f4d4d688d908fb66c47b848b3db472c9081b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -858,6 +858,54 @@ 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->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 (!act->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 +1221,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;
 

diff --git a/model.h b/model.h
index b078939da637f6297d5383b50d21a3bb507698db..5543eb8a0f79af705301c9201eb1b656a74b7cb6 100644 (file)
--- a/model.h
+++ b/model.h
@@ -152,6 +152,7 @@ private:
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, bool second_part_of_rmw);
        bool process_write(ModelAction *curr);
+       bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
        bool process_thread_action(ModelAction *curr);
        void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue);