From 0170878f8a8be6aa06af6591e50fffdb2ce54022 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 19 Sep 2012 00:34:02 -0700 Subject: [PATCH] merge in master --- action.cc | 4 +- common.cc | 6 ++ common.h | 3 + cyclegraph.cc | 2 + model.cc | 236 ++++++++++++++++++++++++++++++---------------- model.h | 17 ++-- test/releaseseq.c | 47 +++++++++ 7 files changed, 227 insertions(+), 88 deletions(-) create mode 100644 test/releaseseq.c diff --git a/action.cc b/action.cc index 2d9186d..bf55d00 100644 --- a/action.cc +++ b/action.cc @@ -181,7 +181,7 @@ void ModelAction::read_from(const ModelAction *act) ASSERT(cv); reads_from = act; if (act != NULL && this->is_acquire()) { - std::vector< const ModelAction *, MyAlloc > release_heads; + rel_heads_list_t release_heads; model->get_release_seq_heads(this, &release_heads); for (unsigned int i = 0; i < release_heads.size(); i++) synchronize_with(release_heads[i]); @@ -194,7 +194,7 @@ void ModelAction::read_from(const ModelAction *act) * @param act The ModelAction to synchronize with */ void ModelAction::synchronize_with(const ModelAction *act) { - ASSERT(*act < *this); + ASSERT(*act < *this || type == THREAD_JOIN); model->check_promises(cv, act->cv); cv->merge(act->cv); } diff --git a/common.cc b/common.cc index 8cb649b..ac5cb59 100644 --- a/common.cc +++ b/common.cc @@ -3,6 +3,7 @@ #include #include "common.h" +#include "model.h" #define MAX_TRACE_LEN 100 @@ -23,3 +24,8 @@ void print_trace(void) free(strings); } + +void model_print_summary(void) +{ + model->print_summary(); +} diff --git a/common.h b/common.h index 80bc9ad..2dc8b7d 100644 --- a/common.h +++ b/common.h @@ -22,6 +22,8 @@ do { \ if (!(expr)) { \ fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \ + print_trace(); \ + model_print_summary(); \ exit(EXIT_FAILURE); \ } \ } while (0); @@ -29,5 +31,6 @@ do { \ #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__) void print_trace(void); +void model_print_summary(void); #endif /* __COMMON_H__ */ diff --git a/cyclegraph.cc b/cyclegraph.cc index ecf8a78..2bfe76a 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -41,6 +41,7 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) { void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { ASSERT(from); ASSERT(to); + ASSERT(from != to); CycleNode *fromnode=getNode(from); CycleNode *tonode=getNode(to); @@ -82,6 +83,7 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) { ASSERT(from); ASSERT(rmw); + ASSERT(from != rmw); CycleNode *fromnode=getNode(from); CycleNode *rmwnode=getNode(rmw); diff --git a/model.cc b/model.cc index fb492a5..3fb3758 100644 --- a/model.cc +++ b/model.cc @@ -30,7 +30,7 @@ ModelChecker::ModelChecker(struct model_params params) : obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), - lazy_sync_with_release(new HashTable, uintptr_t, 4>()), + lazy_sync_with_release(new HashTable()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), @@ -293,7 +293,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) bool r_status = false; if (!second_part_of_rmw) { - check_recency(curr,false); + check_recency(curr); r_status = r_modification_order(curr, reads_from); } @@ -345,6 +345,54 @@ bool ModelChecker::process_write(ModelAction *curr) return updated_mod_order || updated_promises; } +/** + * Initialize the current action by performing one or more of the following + * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward + * in the NodeStack, manipulating backtracking sets, allocating and + * initializing clock vectors, and computing the promises to fulfill. + * + * @param curr The current action, as passed from the user context; may be + * freed/invalidated after the execution of this function + * @return The current action, as processed by the ModelChecker. Is only the + * same as the parameter @a curr if this is a newly-explored action. + */ +ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) +{ + ModelAction *newcurr; + + if (curr->is_rmwc() || curr->is_rmw()) { + newcurr = process_rmw(curr); + delete curr; + compute_promises(newcurr); + return newcurr; + } + + newcurr = node_stack->explore_action(curr); + if (newcurr) { + /* First restore type and order in case of RMW operation */ + if (curr->is_rmwr()) + newcurr->copy_typeandorder(curr); + + ASSERT(curr->get_location()==newcurr->get_location()); + /* Discard duplicate ModelAction; use action from NodeStack */ + delete curr; + + /* If we have diverged, we need to reset the clock vector. */ + if (diverge == NULL) + newcurr->create_cv(get_parent_action(newcurr->get_tid())); + } else { + newcurr = curr; + /* + * Perform one-time actions when pushing new ModelAction onto + * NodeStack + */ + curr->create_cv(get_parent_action(curr->get_tid())); + if (curr->is_write()) + compute_promises(curr); + } + return newcurr; +} + /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -359,45 +407,20 @@ bool ModelChecker::process_write(ModelAction *curr) */ Thread * ModelChecker::check_current_action(ModelAction *curr) { - bool second_part_of_rmw = false; - ASSERT(curr); - if (curr->is_rmwc() || curr->is_rmw()) { - ModelAction *tmp = process_rmw(curr); - second_part_of_rmw = true; - delete curr; - curr = tmp; - compute_promises(curr); - } else { - ModelAction *tmp = node_stack->explore_action(curr, scheduler->get_enabled()); - if (tmp) { - /* Discard duplicate ModelAction; use action from NodeStack */ - /* First restore type and order in case of RMW operation */ - if (curr->is_rmwr()) - tmp->copy_typeandorder(curr); - - /* If we have diverged, we need to reset the clock vector. */ - if (diverge == NULL) - tmp->create_cv(get_parent_action(tmp->get_tid())); - - ASSERT(curr->get_location()==tmp->get_location()); - - delete curr; - curr = tmp; - } else { - /* - * Perform one-time actions when pushing new ModelAction onto - * NodeStack - */ - curr->create_cv(get_parent_action(curr->get_tid())); - /* Build may_read_from set */ - if (curr->is_read()) - build_reads_from_past(curr); - if (curr->is_write()) - compute_promises(curr); - } - } + bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw(); + + ModelAction *newcurr = initialize_curr_action(curr); + + /* Add the action to lists before any other model-checking tasks */ + if (!second_part_of_rmw) + add_action_to_lists(newcurr); + + /* Build may_read_from set for newly-created actions */ + if (curr == newcurr && curr->is_read()) + build_reads_from_past(curr); + curr = newcurr; /* Thread specific actions */ switch (curr->get_type()) { @@ -413,6 +436,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (!blocking->is_complete()) { blocking->push_wait_list(curr); scheduler->sleep(waiting); + } else { + do_complete_join(curr); } break; } @@ -422,6 +447,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) ModelAction *act = th->pop_wait_list(); Thread *wake = get_thread(act); scheduler->wake(wake); + do_complete_join(act); } th->complete(); break; @@ -457,18 +483,30 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) 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 */ + case WORK_CHECK_MO_EDGES: { + /** @todo Complete verification of work_queue */ + ModelAction *act = work.action; + bool updated = false; + + if (act->is_read()) { + if (r_modification_order(act, act->get_reads_from())) + updated = true; + } + if (act->is_write()) { + if (w_modification_order(act)) + updated = true; + } + + if (updated) + work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); + break; + } default: ASSERT(false); break; } } - /* Add action to list. */ - if (!second_part_of_rmw) - add_action_to_lists(curr); - check_curr_backtracking(curr); set_backtracking(curr); @@ -476,6 +514,19 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(curr); } +/** + * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH + * operation from the Thread it is joining with. Must be called after the + * completion of the Thread in question. + * @param join The THREAD_JOIN action + */ +void ModelChecker::do_complete_join(ModelAction *join) +{ + Thread *blocking = (Thread *)join->get_location(); + ModelAction *act = get_last_action(blocking->get_id()); + join->synchronize_with(act); +} + void ModelChecker::check_curr_backtracking(ModelAction * curr) { Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); @@ -514,11 +565,24 @@ bool ModelChecker::isfeasible() { /** @returns whether the current partial trace is feasible other than * multiple RMW reading from the same store. */ bool ModelChecker::isfeasibleotherthanRMW() { + if (DBG_ENABLED()) { + if (mo_graph->checkForCycles()) + DEBUG("Infeasible: modification order cycles\n"); + if (failed_promise) + DEBUG("Infeasible: failed promise\n"); + if (too_many_reads) + DEBUG("Infeasible: too many reads\n"); + if (promises_expired()) + DEBUG("Infeasible: promises expired\n"); + } return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired(); } /** Returns whether the current completed trace is feasible. */ bool ModelChecker::isfinalfeasible() { + if (DBG_ENABLED() && promises->size() != 0) + DEBUG("Infeasible: unrevolved promises\n"); + return isfeasible() && promises->size() == 0; } @@ -545,7 +609,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { * * If so, we decide that the execution is no longer feasible. */ -void ModelChecker::check_recency(ModelAction *curr, bool already_added) { +void ModelChecker::check_recency(ModelAction *curr) { if (params.maxreads != 0) { if (curr->get_node()->get_read_from_size() <= 1) return; @@ -566,12 +630,10 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) { action_list_t::reverse_iterator rit = list->rbegin(); /* Skip past curr */ - if (already_added) { - for (; (*rit) != curr; rit++) - ; - /* go past curr now */ - rit++; - } + for (; (*rit) != curr; rit++) + ; + /* go past curr now */ + rit++; action_list_t::reverse_iterator ritcopy = rit; //See if we have enough reads from the same value @@ -662,10 +724,13 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - /* Include at most one act per-thread that "happens before" curr */ - if (act->happens_before(curr)) { + /* + * Include at most one act per-thread that "happens + * before" curr. Don't consider reflexively. + */ + if (act->happens_before(curr) && act != curr) { if (act->is_write()) { - if (rf != act && act != curr) { + if (rf != act) { mo_graph->addEdge(act, rf); added = true; } @@ -676,7 +741,6 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf added = true; } } - break; } } @@ -769,7 +833,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) if (curr->is_seqcst()) { /* We have to at least see the last sequentially consistent write, so we are initialized. */ - ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location()); + ModelAction *last_seq_cst = get_last_seq_cst(curr); if (last_seq_cst != NULL) { mo_graph->addEdge(last_seq_cst, curr); added = true; @@ -783,8 +847,23 @@ bool ModelChecker::w_modification_order(ModelAction *curr) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; + if (act == curr) { + /* + * If RMW, we already have all relevant edges, + * so just skip to next thread. + * If normal write, we need to look at earlier + * actions, so continue processing list. + */ + if (curr->is_rmw()) + break; + else + continue; + } - /* Include at most one act per-thread that "happens before" curr */ + /* + * Include at most one act per-thread that "happens + * before" curr + */ if (act->happens_before(curr)) { /* * Note: if act is RMW, just add edge: @@ -792,11 +871,9 @@ bool ModelChecker::w_modification_order(ModelAction *curr) * The following edge should be handled elsewhere: * readfrom(act) --mo--> act */ - if (act->is_write()) { - //RMW shouldn't have an edge to themselves - if (act!=curr) - mo_graph->addEdge(act, curr); - } else if (act->is_read() && act->get_reads_from() != NULL) + if (act->is_write()) + mo_graph->addEdge(act, curr); + else if (act->is_read() && act->get_reads_from() != NULL) mo_graph->addEdge(act->get_reads_from(), curr); added = true; break; @@ -867,8 +944,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * @return true, if the ModelChecker is certain that release_heads is complete; * false otherwise */ -bool ModelChecker::release_seq_head(const ModelAction *rf, - std::vector< const ModelAction *, MyAlloc > *release_heads) const +bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const { if (!rf) { /* read from future: need to settle this later */ @@ -973,15 +1049,14 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, * 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< const ModelAction *, MyAlloc > *release_heads) +void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) { const ModelAction *rf = act->get_reads_from(); bool complete; complete = release_seq_head(rf, release_heads); if (!complete) { /* add act to 'lazy checking' list */ - std::list *list; + action_list_t *list; list = lazy_sync_with_release->get_safe_ptr(act->get_location()); list->push_back(act); (*lazy_sync_size)++; @@ -1003,17 +1078,17 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, */ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue) { - std::list *list; + action_list_t *list; list = lazy_sync_with_release->getptr(location); if (!list) return false; bool updated = false; - std::list::iterator it = list->begin(); + action_list_t::iterator it = list->begin(); while (it != list->end()) { ModelAction *act = *it; const ModelAction *rf = act->get_reads_from(); - std::vector< const ModelAction *, MyAlloc > release_heads; + rel_heads_list_t release_heads; bool complete; complete = release_seq_head(rf, &release_heads); for (unsigned int i = 0; i < release_heads.size(); i++) { @@ -1087,18 +1162,21 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) } /** - * Gets the last memory_order_seq_cst action (in the total global sequence) - * performed on a particular object (i.e., memory location). - * @param location The object location to check - * @return The last seq_cst action performed + * Gets the last memory_order_seq_cst write (in the total global sequence) + * performed on a particular object (i.e., memory location), not including the + * current action. + * @param curr The current ModelAction; also denotes the object location to + * check + * @return The last seq_cst write */ -ModelAction * ModelChecker::get_last_seq_cst(const void *location) +ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) { + void *location = curr->get_location(); action_list_t *list = obj_map->get_safe_ptr(location); /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) - if ((*rit)->is_write() && (*rit)->is_seqcst()) + if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr) return *rit; return NULL; } @@ -1212,7 +1290,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) bool initialized = false; if (curr->is_seqcst()) { - last_seq_cst = get_last_seq_cst(curr->get_location()); + last_seq_cst = get_last_seq_cst(curr); /* We have to at least see the last sequentially consistent write, so we are initialized. */ if (last_seq_cst != NULL) @@ -1228,7 +1306,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) ModelAction *act = *rit; /* Only consider 'write' actions */ - if (!act->is_write()) + if (!act->is_write() || act == curr) continue; /* Don't consider more than one seq_cst write if we are a seq_cst read. */ diff --git a/model.h b/model.h index 4fc32c6..fd6e6c2 100644 --- a/model.h +++ b/model.h @@ -24,6 +24,9 @@ class NodeStack; class CycleGraph; class Promise; +/** @brief Shorthand for a list of release sequence heads */ +typedef std::vector< const ModelAction *, MyAlloc > rel_heads_list_t; + /** * Model checker parameter structure. Holds run-time configuration options for * the model checker. @@ -85,8 +88,7 @@ public: bool isfeasibleotherthanRMW(); bool isfinalfeasible(); void check_promises(ClockVector *old_cv, ClockVector * merge_cv); - void get_release_seq_heads(ModelAction *act, - std::vector< const ModelAction *, MyAlloc > *release_heads); + void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads); void finish_execution(); bool isfeasibleprefix(); void set_assert() {asserted=true;} @@ -112,12 +114,13 @@ private: */ void set_current_action(ModelAction *act) { priv->current_action = act; } Thread * check_current_action(ModelAction *curr); + ModelAction * initialize_curr_action(ModelAction *curr); bool process_read(ModelAction *curr, bool second_part_of_rmw); bool process_write(ModelAction *curr); bool take_step(); - void check_recency(ModelAction *curr, bool already_added); + void check_recency(ModelAction *curr); ModelAction * get_last_conflict(ModelAction *act); void set_backtracking(ModelAction *act); Thread * get_next_thread(ModelAction *curr); @@ -129,15 +132,15 @@ private: void check_curr_backtracking(ModelAction * curr); void add_action_to_lists(ModelAction *act); ModelAction * get_last_action(thread_id_t tid); - ModelAction * get_last_seq_cst(const void *location); + ModelAction * get_last_seq_cst(ModelAction *curr); void build_reads_from_past(ModelAction *curr); ModelAction * process_rmw(ModelAction *curr); 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_head(const ModelAction *rf, - std::vector< const ModelAction *, MyAlloc > *release_heads) const; + bool release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const; bool resolve_release_sequences(void *location, work_queue_t *work_queue); + void do_complete_join(ModelAction *join); ModelAction *diverge; @@ -160,7 +163,7 @@ private: * This structure maps its lists by object location. Each ModelAction * in the lists should be an acquire operation. */ - HashTable, uintptr_t, 4> *lazy_sync_with_release; + HashTable *lazy_sync_with_release; /** * Represents the total size of the diff --git a/test/releaseseq.c b/test/releaseseq.c new file mode 100644 index 0000000..d3127f3 --- /dev/null +++ b/test/releaseseq.c @@ -0,0 +1,47 @@ +/* + * This test performs some relaxes, release, acquire opeations on a single + * atomic variable. It can give some rough idea of release sequence support but + * probably should be improved to give better information. + */ + +#include + +#include "libthreads.h" +#include "librace.h" +#include "stdatomic.h" + +atomic_int x; + +static void a(void *obj) +{ + atomic_store_explicit(&x, 1, memory_order_release); + atomic_store_explicit(&x, 42, memory_order_relaxed); +} + +static void b(void *obj) +{ + int r = atomic_load_explicit(&x, memory_order_acquire); + printf("r = %u\n", r); +} + +static void c(void *obj) +{ + atomic_store_explicit(&x, 2, memory_order_relaxed); +} + +void user_main() +{ + thrd_t t1, t2, t3; + + atomic_init(&x, 0); + + printf("Thread %d: creating 3 threads\n", thrd_current()); + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&b, NULL); + thrd_create(&t3, (thrd_start_t)&c, NULL); + + thrd_join(t1); + thrd_join(t2); + thrd_join(t3); + printf("Thread %d is finished\n", thrd_current()); +} -- 2.34.1