From 237f94a977b3c09f8b3b2f551e0057a4ed36b06d Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 1 Mar 2013 16:19:10 -0800 Subject: [PATCH] model: fixes for future value passing For one, we don't want to 'add_future_value()' when w_modification_order is called anywhere besides process_write(). Also, we want to filter out potential future values based on the existence of a Promise that this write must resolve. So pass a vector parameter to w_modification_order for recording future values only when (and where) we want them. --- model.cc | 28 ++++++++++++++++++++++------ model.h | 2 +- 2 files changed, 23 insertions(+), 7 deletions(-) diff --git a/model.cc b/model.cc index 618b37e0..129f6c02 100644 --- a/model.cc +++ b/model.cc @@ -1044,12 +1044,26 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read */ bool ModelChecker::process_write(ModelAction *curr) { - bool updated_mod_order = w_modification_order(curr); + /* Readers to which we may send our future value */ + std::vector< ModelAction *, ModelAlloc > send_fv; + + bool updated_mod_order = w_modification_order(curr, &send_fv); int promise_idx = get_promise_to_resolve(curr); + const ModelAction *earliest_promise_reader; bool updated_promises = false; - if (promise_idx >= 0) + if (promise_idx >= 0) { + earliest_promise_reader = (*promises)[promise_idx]->get_reader(0); updated_promises = resolve_promise(curr, promise_idx); + } else + earliest_promise_reader = NULL; + + /* Don't send future values to reads after the Promise we resolve */ + for (unsigned int i = 0; i < send_fv.size(); i++) { + ModelAction *read = send_fv[i]; + if (!earliest_promise_reader || *read < *earliest_promise_reader) + futurevalues->push_back(PendingFutureValue(curr, read)); + } if (promises->size() == 0) { for (unsigned int i = 0; i < futurevalues->size(); i++) { @@ -1506,7 +1520,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr) } } if (act->is_write()) { - if (w_modification_order(act)) + if (w_modification_order(act, NULL)) updated = true; } mo_graph->commitChanges(); @@ -1837,9 +1851,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) * (II) Sending the write back to non-synchronizing reads. * * @param curr The current action. Must be a write. + * @param send_fv A vector for stashing reads to which we may pass our future + * value. If NULL, then don't record any future values. * @return True if modification order edges were added; false otherwise */ -bool ModelChecker::w_modification_order(ModelAction *curr) +bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc > *send_fv) { std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; @@ -1932,9 +1948,9 @@ bool ModelChecker::w_modification_order(ModelAction *curr) pendingfuturevalue. */ - if (thin_air_constraint_may_allow(curr, act)) { + if (send_fv && thin_air_constraint_may_allow(curr, act)) { if (!is_infeasible()) - futurevalues->push_back(PendingFutureValue(curr, act)); + send_fv->push_back(act); else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from()) add_future_value(curr, act); } diff --git a/model.h b/model.h index fe76d7f9..412543db 100644 --- a/model.h +++ b/model.h @@ -196,7 +196,7 @@ private: template bool r_modification_order(ModelAction *curr, const rf_type *rf); - bool w_modification_order(ModelAction *curr); + bool w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc > *send_fv); 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