From: Brian Demsky Date: Fri, 5 Oct 2012 00:37:38 +0000 (-0700) Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker X-Git-Tag: pldi2013~102 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6f8de9e0f5697652fd20b2ecf149f96bfb572538;hp=2fbddccbb035e45db7da1f5e23df14f4d0fcda9f;p=model-checker.git Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker --- diff --git a/model.cc b/model.cc index dd72fdb..bcc4298 100644 --- a/model.cc +++ b/model.cc @@ -34,7 +34,7 @@ ModelChecker::ModelChecker(struct model_params params) : obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), - pending_acq_rel_seq(new std::vector()), + pending_rel_seqs(new std::vector()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), @@ -65,7 +65,7 @@ ModelChecker::~ModelChecker() delete (*promises)[i]; delete promises; - delete pending_acq_rel_seq; + delete pending_rel_seqs; delete thrd_last_action; delete node_stack; @@ -208,7 +208,7 @@ bool ModelChecker::next_execution() } DEBUG("Number of acquires waiting on pending release sequences: %lu\n", - pending_acq_rel_seq->size()); + pending_rel_seqs->size()); if (isfinalfeasible() || DBG_ENABLED()) print_summary(); @@ -760,7 +760,7 @@ bool ModelChecker::promises_expired() { /** @return whether the current partial trace must be a prefix of a * feasible trace. */ bool ModelChecker::isfeasibleprefix() { - return promises->size() == 0 && pending_acq_rel_seq->size() == 0; + return promises->size() == 0 && pending_rel_seqs->size() == 0; } /** @return whether the current partial trace is feasible. */ @@ -1174,13 +1174,19 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * @todo Finish lazy updating, when promises are fulfilled in the future * @param rf The action that might be part of a release sequence. Must be a * write. - * @param release_heads A pass-by-reference style return parameter. After + * @param release_heads A pass-by-reference style return parameter. After * execution of this function, release_heads will contain the heads of all the - * relevant release sequences, if any exists + * relevant release sequences, if any exists with certainty + * @param pending A pass-by-reference style return parameter which is only used + * when returning false (i.e., uncertain). Returns most information regarding + * an uncertain release sequence, including any write operations that might + * break the sequence. * @return true, if the ModelChecker is certain that release_heads is complete; * false otherwise */ -bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const +bool ModelChecker::release_seq_heads(const ModelAction *rf, + rel_heads_list_t *release_heads, + struct release_seq *pending) const { /* Only check for release sequences if there are no cycles */ if (mo_graph->checkForCycles()) @@ -1209,6 +1215,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re }; if (!rf) { /* read from future: need to settle this later */ + pending->rf = NULL; return false; /* incomplete */ } @@ -1238,6 +1245,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re ASSERT(rf->same_thread(release)); + pending->writes.clear(); + bool certain = true; for (unsigned int i = 0; i < thrd_lists->size(); i++) { if (id_to_int(rf->get_tid()) == (int)i) @@ -1281,14 +1290,21 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re /* release --mo-> act --mo--> rf */ return true; /* complete */ } + /* act may break release sequence */ + pending->writes.push_back(act); certain = false; } if (!future_ordered) - return false; /* This thread is uncertain */ + certain = false; /* This thread is uncertain */ } - if (certain) + if (certain) { release_heads->push_back(release); + pending->writes.clear(); + } else { + pending->release = release; + pending->rf = rf; + } return certain; } @@ -1307,10 +1323,14 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) { const ModelAction *rf = act->get_reads_from(); + struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq)); + sequence->acquire = act; - if (!release_seq_heads(rf, release_heads)) { + if (!release_seq_heads(rf, release_heads, sequence)) { /* add act to 'lazy checking' list */ - pending_acq_rel_seq->push_back(act); + pending_rel_seqs->push_back(sequence); + } else { + snapshot_free(sequence); } } @@ -1330,9 +1350,10 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue) { bool updated = false; - std::vector::iterator it = pending_acq_rel_seq->begin(); - while (it != pending_acq_rel_seq->end()) { - ModelAction *act = *it; + std::vector::iterator it = pending_rel_seqs->begin(); + while (it != pending_rel_seqs->end()) { + struct release_seq *pending = *it; + ModelAction *act = pending->acquire; /* Only resolve sequences on the given location, if provided */ if (location && act->get_location() != location) { @@ -1343,7 +1364,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ const ModelAction *rf = act->get_reads_from(); rel_heads_list_t release_heads; bool complete; - complete = release_seq_heads(rf, &release_heads); + 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])) @@ -1370,10 +1391,12 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } } } - if (complete) - it = pending_acq_rel_seq->erase(it); - else + if (complete) { + it = pending_rel_seqs->erase(it); + snapshot_free(pending); + } else { it++; + } } // If we resolved promises or data races, see if we have realized a data race. diff --git a/model.h b/model.h index dfc8e36..d5dc422 100644 --- a/model.h +++ b/model.h @@ -55,6 +55,19 @@ struct model_snapshot_members { ModelAction *next_backtrack; }; +/** @brief Records information regarding a single pending release sequence */ +struct release_seq { + /** @brief The acquire operation */ + ModelAction *acquire; + /** @brief The head of the RMW chain from which 'acquire' reads; may be + * equal to 'release' */ + const ModelAction *rf; + /** @brief The head of the potential longest release sequence chain */ + const ModelAction *release; + /** @brief The write(s) that may break the release sequence */ + std::vector writes; +}; + /** @brief The central structure for model-checking */ class ModelChecker { public: @@ -150,7 +163,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); - bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const; + 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); void do_complete_join(ModelAction *join); @@ -174,12 +187,12 @@ private: std::vector *futurevalues; /** - * List of acquire actions that might synchronize with one or more - * release sequence. Release sequences might be determined lazily as - * promises are fulfilled and modification orders are established. Each - * ModelAction in this list must be an acquire operation. + * List of pending release sequences. Release sequences might be + * determined lazily as promises are fulfilled and modification orders + * are established. Each entry in the list may only be partially + * filled, depending on its pending status. */ - std::vector *pending_acq_rel_seq; + std::vector *pending_rel_seqs; std::vector *thrd_last_action; NodeStack *node_stack; diff --git a/nodestack.cc b/nodestack.cc index a737653..6b1d4ef 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -362,16 +362,18 @@ void Node::explore(thread_id_t tid) explored_children[i] = true; } -NodeStack::NodeStack() - : total_nodes(0) +NodeStack::NodeStack() : + node_list(1, new Node()), + iter(0), + total_nodes(0) { - node_list.push_back(new Node()); total_nodes++; - iter = 0; } NodeStack::~NodeStack() { + for (unsigned int i = 0; i < node_list.size(); i++) + delete node_list[i]; } void NodeStack::print()