From 20f8e2bc8677046c4bd7cb0bb80696ced41301f2 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 4 Dec 2012 15:14:29 -0800 Subject: [PATCH] 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. --- model.cc | 41 +++++++++++++++++++++++++---------------- model.h | 8 ++++++-- 2 files changed, 31 insertions(+), 18 deletions(-) diff --git a/model.cc b/model.cc index a9ea7b04..dbca58e7 100644 --- 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 >::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 a2bbab2e..b078939d 100644 --- 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); -- 2.34.1