From 0e9020d6d5a4e0570d1001b07393d080de8bb318 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 14 Aug 2012 17:21:29 -0700 Subject: [PATCH] model: add release sequence support The ModelChecker now can find the head(s) of the release sequence(s) with which a particular ModelAction (read-acquire) will synchronize. The ModelChecker::release_seq_head function can locate a release sequence head for a given ModelAction, based on information at a given moment. That is, it knows happens-before and modification information for the present, but some decisions may need to be made in the future as reads-from promises are fulfilled or modification ordering is observed by future reads and writes. Lazy checking for the latter cases has yet to be implemented. --- model.cc | 122 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ model.h | 4 ++ 2 files changed, 126 insertions(+) diff --git a/model.cc b/model.cc index 44e1a2d..bd0c3dc 100644 --- a/model.cc +++ b/model.cc @@ -503,6 +503,128 @@ void ModelChecker::w_modification_order(ModelAction * curr) { } } +/** + * Finds the head(s) of the release sequence(s) containing a given ModelAction. + * The ModelAction under consideration is expected to be taking part in + * release/acquire synchronization as an object of the "reads from" relation. + * Note that this can only provide release sequence support for RMW chains + * which do not read from the future, as those actions cannot be traced until + * their "promise" is fulfilled. Similarly, we may not even establish the + * presence of a release sequence with certainty, as some modification order + * constraints may be decided further in the future. Thus, this function + * "returns" two pieces of data: a pass-by-reference vector of @a release_heads + * and a boolean representing certainty. + * + * @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 + * execution of this function, release_heads will contain the heads of all the + * relevant release sequences, if any exists + * @return true, if the ModelChecker is certain that release_heads is complete; + * false otherwise + */ +bool ModelChecker::release_seq_head(const ModelAction *rf, + std::vector *release_heads) const +{ + ASSERT(rf->is_write()); + if (!rf) { + /* read from future: need to settle this later */ + return false; /* incomplete */ + } + if (rf->is_release()) + release_heads->push_back(rf); + if (rf->is_rmw()) { + if (rf->is_acquire()) + return true; /* complete */ + return release_seq_head(rf->get_reads_from(), release_heads); + } + if (rf->is_release()) + return true; /* complete */ + + /* else relaxed write; check modification order for contiguous subsequence + * -> rf must be same thread as release */ + int tid = id_to_int(rf->get_tid()); + std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location()); + action_list_t *list = &(*thrd_lists)[tid]; + action_list_t::const_reverse_iterator rit; + + /* Find rf in the thread list */ + for (rit = list->rbegin(); rit != list->rend(); rit++) + if (*rit == rf) + break; + + /* Find the last write/release */ + for (; rit != list->rend(); rit++) + if ((*rit)->is_release()) + break; + if (rit == list->rend()) { + /* No write-release in this thread */ + return true; /* complete */ + } + ModelAction *release = *rit; + + ASSERT(rf->same_thread(release)); + + bool certain = true; + for (unsigned int i = 0; i < thrd_lists->size(); i++) { + if (id_to_int(rf->get_tid()) == (int)i) + continue; + list = &(*thrd_lists)[i]; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + const ModelAction *act = *rit; + if (!act->is_write()) + continue; + /* Reach synchronization -> this thread is complete */ + if (act->happens_before(release)) + break; + if (rf->happens_before(act)) + continue; + + /* Check modification order */ + if (mo_graph->checkReachable(rf, act)) + /* rf --mo--> act */ + continue; + if (mo_graph->checkReachable(act, release)) + /* act --mo--> release */ + break; + if (mo_graph->checkReachable(release, act) && + mo_graph->checkReachable(act, rf)) { + /* release --mo-> act --mo--> rf */ + return true; /* complete */ + } + certain = false; + } + } + + if (certain) + release_heads->push_back(release); + return certain; +} + +/** + * A public interface for getting the release sequence head(s) with which a + * 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 + * synchronization at some later point in execution. + * @param act The 'acquire' action that may read from a release sequence + * @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_head + */ +void ModelChecker::get_release_seq_heads(ModelAction *act, + std::vector *release_heads) +{ + const ModelAction *rf = act->get_reads_from(); + bool complete; + complete = release_seq_head(rf, release_heads); + if (!complete) { + /** @todo complete lazy checking */ + } +} + /** * Performs various bookkeeping operations for the current ModelAction. For * instance, adds action to the per-object, per-thread action vector and to the diff --git a/model.h b/model.h index e8a3efc..dea744c 100644 --- a/model.h +++ b/model.h @@ -61,6 +61,8 @@ public: bool isfeasible(); bool isfinalfeasible(); void check_promises(ClockVector *old_cv, ClockVector * merge_cv); + void get_release_seq_heads(ModelAction *act, + std::vector *release_heads); void finish_execution(); @@ -103,6 +105,8 @@ private: void post_r_modification_order(ModelAction *curr, const ModelAction *rf); void r_modification_order(ModelAction *curr, const ModelAction *rf); void w_modification_order(ModelAction *curr); + bool release_seq_head(const ModelAction *rf, + std::vector *release_heads) const; ModelAction *current_action; ModelAction *diverge; -- 2.34.1