From: Brian Norris Date: Fri, 14 Sep 2012 18:25:59 +0000 (-0700) Subject: Merge branch 'norris' X-Git-Tag: pldi2013~190 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=202074f941d19cef894068e7f79d76b2df598f4b;hp=f7a6ea5bf658115849fcc5b8a06a3f8c5a629656;p=model-checker.git Merge branch 'norris' --- diff --git a/Makefile b/Makefile index a0608b5..53b0331 100644 --- a/Makefile +++ b/Makefile @@ -44,15 +44,21 @@ malloc.o: malloc.c %.o: %.cc $(CXX) -fPIC -c $< $(CPPFLAGS) +PHONY += clean clean: rm -f *.o *.so $(MAKE) -C $(TESTS_DIR) clean +PHONY += mrclean mrclean: clean rm -rf docs -tags:: +PHONY += tags +tags: ctags -R -tests:: $(LIB_SO) +PHONY += tests +tests: $(LIB_SO) $(MAKE) -C $(TESTS_DIR) + +.PHONY: $(PHONY) diff --git a/model.cc b/model.cc index cdce102..954c07d 100644 --- a/model.cc +++ b/model.cc @@ -265,11 +265,11 @@ ModelAction * ModelChecker::get_next_backtrack() /** * Processes a read or rmw model action. * @param curr is the read model action to process. - * @param th is the thread * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw. * @return True if processing this read updates the mo_graph. */ -bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) { +bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) +{ uint64_t value; bool updated = false; while (true) { @@ -303,11 +303,36 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part Promise *valuepromise = new Promise(curr, value, expiration); promises->push_back(valuepromise); } - th->set_return_value(value); + get_thread(curr)->set_return_value(value); return updated; } } +/** + * Process a write ModelAction + * @param curr The ModelAction to process + * @return True if the mo_graph was updated or promises were resolved + */ +bool ModelChecker::process_write(ModelAction *curr) +{ + bool updated_mod_order = w_modification_order(curr); + bool updated_promises = resolve_promises(curr); + + if (promises->size() == 0) { + for (unsigned int i = 0; isize(); i++) { + struct PendingFutureValue pfv = (*futurevalues)[i]; + if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) && + (!priv->next_backtrack || *pfv.act > *priv->next_backtrack)) + priv->next_backtrack = pfv.act; + } + futurevalues->resize(0); + } + + mo_graph->commitChanges(); + get_thread(curr)->set_return_value(VALUE_NONE); + return updated_mod_order || updated_promises; +} + /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -395,33 +420,36 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) break; } - bool updated = false; + work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); - if (curr->is_read()) { - updated = process_read(curr, get_thread(curr), second_part_of_rmw); - } + while (!work_queue.empty()) { + WorkQueueEntry work = work_queue.front(); + work_queue.pop_front(); - if (curr->is_write()) { - bool updated_mod_order = w_modification_order(curr); - bool updated_promises = resolve_promises(curr); - updated = updated || updated_mod_order || updated_promises; - - if (promises->size()==0) { - for (unsigned int i = 0; isize(); i++) { - struct PendingFutureValue pfv=(*futurevalues)[i]; - if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) && - (!priv->next_backtrack || *pfv.act > *priv->next_backtrack)) - priv->next_backtrack = pfv.act; - } - futurevalues->resize(0); - } + switch (work.type) { + case WORK_CHECK_CURR_ACTION: { + ModelAction *act = work.action; + bool updated = false; + if (act->is_read() && process_read(act, second_part_of_rmw)) + updated = true; - mo_graph->commitChanges(); - get_thread(curr)->set_return_value(VALUE_NONE); - } + if (act->is_write() && process_write(act)) + updated = true; - if (updated) - resolve_release_sequences(curr->get_location()); + if (updated) + work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); + break; + } + case WORK_CHECK_RELEASE_SEQ: + resolve_release_sequences(work.location, &work_queue); + break; + case WORK_CHECK_MO_EDGES: + /** @todo Perform follow-up mo_graph checks */ + default: + ASSERT(false); + break; + } + } /* Add action to list. */ if (!second_part_of_rmw) @@ -954,9 +982,12 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, * * @param location The location/object that should be checked for release * sequence resolutions - * @return True if any updates occurred (new synchronization, new mo_graph edges) + * @param work_queue The work queue to which to add work items as they are + * generated + * @return True if any updates occurred (new synchronization, new mo_graph + * edges) */ -bool ModelChecker::resolve_release_sequences(void *location) +bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue) { std::list *list; list = lazy_sync_with_release->getptr(location); @@ -979,14 +1010,18 @@ bool ModelChecker::resolve_release_sequences(void *location) } if (updated) { + /* Re-check act for mo_graph edges */ + work_queue->push_back(MOEdgeWorkEntry(act)); + /* propagate synchronization to later actions */ action_list_t::reverse_iterator it = action_trace->rbegin(); while ((*it) != act) { ModelAction *propagate = *it; - if (act->happens_before(propagate)) - /** @todo new mo_graph edges along with - * this synchronization? */ + if (act->happens_before(propagate)) { propagate->synchronize_with(act); + /* Re-check 'propagate' for mo_graph edges */ + work_queue->push_back(MOEdgeWorkEntry(propagate)); + } } } if (complete) { diff --git a/model.h b/model.h index 4f1d6ee..4fc32c6 100644 --- a/model.h +++ b/model.h @@ -17,6 +17,7 @@ #include "action.h" #include "clockvector.h" #include "hashtable.h" +#include "workqueue.h" /* Forward declaration */ class NodeStack; @@ -111,7 +112,8 @@ private: */ void set_current_action(ModelAction *act) { priv->current_action = act; } Thread * check_current_action(ModelAction *curr); - bool process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw); + bool process_read(ModelAction *curr, bool second_part_of_rmw); + bool process_write(ModelAction *curr); bool take_step(); @@ -135,7 +137,7 @@ private: bool w_modification_order(ModelAction *curr); bool release_seq_head(const ModelAction *rf, std::vector< const ModelAction *, MyAlloc > *release_heads) const; - bool resolve_release_sequences(void *location); + bool resolve_release_sequences(void *location, work_queue_t *work_queue); ModelAction *diverge; diff --git a/workqueue.h b/workqueue.h new file mode 100644 index 0000000..71067bb --- /dev/null +++ b/workqueue.h @@ -0,0 +1,107 @@ +/** + * @file workqueue.h + * @brief Provides structures for queueing ModelChecker actions to be taken + */ + +#ifndef __WORKQUEUE_H__ +#define __WORKQUEUE_H__ + +#include +#include "mymemory.h" + +class ModelAction; + +typedef enum { + WORK_NONE = 0, /**< No work to be done */ + WORK_CHECK_CURR_ACTION, /**< Check the current action; used for the + first action of the work loop */ + WORK_CHECK_RELEASE_SEQ, /**< Check if any pending release sequences + are resolved */ + WORK_CHECK_MO_EDGES, /**< Check if new mo_graph edges can be added */ +} model_work_t; + +/** + */ +class WorkQueueEntry { + public: + /** @brief Type of work queue entry */ + model_work_t type; + + /** + * @brief Object affected + * @see CheckRelSeqWorkEntry + */ + void *location; + + /** + * @brief The ModelAction to work on + * @see MOEdgeWorkEntry + */ + ModelAction *action; +}; + +/** + * @brief Work: perform initial promise, mo_graph checks on the current action + * + * This WorkQueueEntry performs the normal, first-pass checks for a ModelAction + * that is currently being explored. The current ModelAction (@a action) is the + * only relevant parameter to this entry. + */ +class CheckCurrWorkEntry : public WorkQueueEntry { + public: + /** + * @brief Constructor for a "check current action" work entry + * @param curr The current action + */ + CheckCurrWorkEntry(ModelAction *curr) { + type = WORK_CHECK_CURR_ACTION; + location = NULL; + action = curr; + } +}; + +/** + * @brief Work: check an object location for resolved release sequences + * + * This WorkQueueEntry checks synchronization and the mo_graph for resolution + * of any release sequences. The object @a location is the only relevant + * parameter to this entry. + */ +class CheckRelSeqWorkEntry : public WorkQueueEntry { + public: + /** + * @brief Constructor for a "check release sequences" work entry + * @param l The location which must be checked for release sequences + */ + CheckRelSeqWorkEntry(void *l) { + type = WORK_CHECK_RELEASE_SEQ; + location = l; + action = NULL; + } +}; + +/** + * @brief Work: check a ModelAction for new mo_graph edges + * + * This WorkQueueEntry checks for new mo_graph edges for a particular + * ModelAction (e.g., that was just generated or that updated its + * synchronization). The ModelAction @a action is the only relevant parameter + * to this entry. + */ +class MOEdgeWorkEntry : public WorkQueueEntry { + public: + /** + * @brief Constructor for a mo_edge work entry + * @param updated The ModelAction which was updated, triggering this work + */ + MOEdgeWorkEntry(ModelAction *updated) { + type = WORK_CHECK_MO_EDGES; + location = NULL; + action = updated; + } +}; + +/** @brief typedef for the work queue type */ +typedef std::list< WorkQueueEntry, MyAlloc > work_queue_t; + +#endif /* __WORKQUEUE_H__ */