model: distinguish between 'read' and 'acquire' in release sequences

When using fences, we may have a fence-acquire preceded by a non-acquire
load, where the load takes part in a "hypothetical release sequence" (as
named by Mathematizing C++). So, I add a parameter to
get_release_seq_heads() and to struct release_seq so that we record the
'acquire' operation separately from the 'read'.

For our traditional release sequences, 'acquire' and 'read' will be the
same ModelAction. But fence-acquire support will utilize distinct
actions.

diff --git a/model.cc b/model.cc
index a9ea7b0493071eebac0b034e7d84d23f3cd21d8f..dbca58e7394f5e3eb9a4f7b68a54c67aff4a5346 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1063,7 +1063,7 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
        act->set_read_from(rf);
        if (rf != NULL && act->is_acquire()) {
                rel_heads_list_t release_heads;
-               get_release_seq_heads(act, &release_heads);
+               get_release_seq_heads(act, act, &release_heads);
                int num_heads = release_heads.size();
                for (unsigned int i = 0; i < release_heads.size(); i++)
                        if (!act->synchronize_with(release_heads[i])) {
@@ -1935,18 +1935,25 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
  * given ModelAction must synchronize. This function only returns a non-empty
  * result when it can locate a release sequence head with certainty. Otherwise,
  * it may mark the internal state of the ModelChecker so that it will handle
- * the release sequence at a later time, causing @a act to update its
+ * the release sequence at a later time, causing @a acquire to update its
  * synchronization at some later point in execution.
- * @param act The 'acquire' action that may read from a release sequence
+ *
+ * @param acquire The 'acquire' action that may synchronize with a release
+ * sequence
+ * @param read The read action that may read from a release sequence; this may
+ * be the same as acquire, or else an earlier action in the same thread (i.e.,
+ * when 'acquire' is a fence-acquire)
  * @param release_heads A pass-by-reference return parameter. Will be filled
  * with the head(s) of the release sequence(s), if they exists with certainty.
  * @see ModelChecker::release_seq_heads
  */
-void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
+void ModelChecker::get_release_seq_heads(ModelAction *acquire,
+               ModelAction *read, rel_heads_list_t *release_heads)
 {
-       const ModelAction *rf = act->get_reads_from();
+       const ModelAction *rf = read->get_reads_from();
        struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
-       sequence->acquire = act;
+       sequence->acquire = acquire;
+       sequence->read = read;
 
        if (!release_seq_heads(rf, release_heads, sequence)) {
                /* add act to 'lazy checking' list */
@@ -1975,21 +1982,22 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
        std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
        while (it != pending_rel_seqs->end()) {
                struct release_seq *pending = *it;
-               ModelAction *act = pending->acquire;
+               ModelAction *acquire = pending->acquire;
+               const ModelAction *read = pending->read;
 
                /* Only resolve sequences on the given location, if provided */
-               if (location && act->get_location() != location) {
+               if (location && read->get_location() != location) {
                        it++;
                        continue;
                }
 
-               const ModelAction *rf = act->get_reads_from();
+               const ModelAction *rf = read->get_reads_from();
                rel_heads_list_t release_heads;
                bool complete;
                complete = release_seq_heads(rf, &release_heads, pending);
                for (unsigned int i = 0; i < release_heads.size(); i++) {
-                       if (!act->has_synchronized_with(release_heads[i])) {
-                               if (act->synchronize_with(release_heads[i]))
+                       if (!acquire->has_synchronized_with(release_heads[i])) {
+                               if (acquire->synchronize_with(release_heads[i]))
                                        updated = true;
                                else
                                        set_bad_synchronization();
@@ -1999,15 +2007,16 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                if (updated) {
                        /* Re-check all pending release sequences */
                        work_queue->push_back(CheckRelSeqWorkEntry(NULL));
-                       /* Re-check act for mo_graph edges */
-                       work_queue->push_back(MOEdgeWorkEntry(act));
+                       /* Re-check read-acquire for mo_graph edges */
+                       if (acquire->is_read())
+                               work_queue->push_back(MOEdgeWorkEntry(acquire));
 
                        /* propagate synchronization to later actions */
                        action_list_t::reverse_iterator rit = action_trace->rbegin();
-                       for (; (*rit) != act; rit++) {
+                       for (; (*rit) != acquire; rit++) {
                                ModelAction *propagate = *rit;
-                               if (act->happens_before(propagate)) {
-                                       propagate->synchronize_with(act);
+                               if (acquire->happens_before(propagate)) {
+                                       propagate->synchronize_with(acquire);
                                        /* Re-check 'propagate' for mo_graph edges */
                                        work_queue->push_back(MOEdgeWorkEntry(propagate));
                                }

diff --git a/model.h b/model.h
index a2bbab2eee0aef821ae9e7ef1e79820a71da958c..b078939da637f6297d5383b50d21a3bb507698db 100644 (file)
--- a/model.h
+++ b/model.h
@@ -75,7 +75,11 @@ struct PendingFutureValue {
 struct release_seq {
        /** @brief The acquire operation */
        ModelAction *acquire;
-       /** @brief The head of the RMW chain from which 'acquire' reads; may be
+       /** @brief The read operation that may read from a release sequence;
+        *  may be the same as acquire, or else an earlier action in the same
+        *  thread (i.e., when 'acquire' is a fence-acquire) */
+       const ModelAction *read;
+       /** @brief The head of the RMW chain from which 'read' reads; may be
         *  equal to 'release' */
        const ModelAction *rf;
        /** @brief The head of the potential longest release sequence chain */
@@ -178,7 +182,7 @@ private:
        void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
        bool r_modification_order(ModelAction *curr, const ModelAction *rf);
        bool w_modification_order(ModelAction *curr);
-       void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
+       void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
        bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);