From b81523a0046db06d5ecd9693788ca29f4b023ddb Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 18 Sep 2012 18:54:40 -0700 Subject: [PATCH] model: add typedef for list of release sequence heads --- action.cc | 2 +- model.cc | 8 +++----- model.h | 9 +++++---- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/action.cc b/action.cc index 2021f0a..801e548 100644 --- a/action.cc +++ b/action.cc @@ -173,7 +173,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]); diff --git a/model.cc b/model.cc index 2b295de..52b2e17 100644 --- a/model.cc +++ b/model.cc @@ -931,8 +931,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 */ @@ -1037,8 +1036,7 @@ 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; @@ -1077,7 +1075,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ 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++) { diff --git a/model.h b/model.h index b2b312f..eb50d37 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;} @@ -136,8 +138,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_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); -- 2.34.1