From 87d6ae25425840ccad0ef6edef6e279967e83be6 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 19 Dec 2012 15:26:47 -0800 Subject: [PATCH] action: add get_thread_operand() method Instead of guessing at the (type-unsafe) storage within THREAD_{CREATE,JOIN} ModelActions, we can at least code this within a single method. Note that this method may get more complex, particularly for THREAD_CREATE. --- action.cc | 24 ++++++++++++++++++++++++ action.h | 2 ++ model.cc | 7 +++---- 3 files changed, 29 insertions(+), 4 deletions(-) diff --git a/action.cc b/action.cc index 84c20eb..acecd5a 100644 --- a/action.cc +++ b/action.cc @@ -238,6 +238,30 @@ void ModelAction::copy_typeandorder(ModelAction * act) this->order = act->order; } +/** + * Get the Thread which is the operand of this action. This is only valid for + * THREAD_* operations (currently only for THREAD_CREATE and THREAD_JOIN). Note + * that this provides a central place for determining the conventions of Thread + * storage in ModelAction, where we generally aren't very type-safe (e.g., we + * store object references in a (void *) address. + * + * For THREAD_CREATE, this yields the Thread which is created. + * For THREAD_JOIN, this yields the Thread we are joining with. + * + * @return The Thread which this action acts on, if exists; otherwise NULL + */ +Thread * ModelAction::get_thread_operand() const +{ + if (type == THREAD_CREATE) + /* THREAD_CREATE uses (Thread *) for location */ + return (Thread *)get_location(); + else if (type == THREAD_JOIN) + /* THREAD_JOIN uses (Thread *) for location */ + return (Thread *)get_location(); + else + return NULL; +} + /** This method changes an existing read part of an RMW action into either: * (1) a full RMW action in case of the completed write or * (2) a READ action in case a failed action. diff --git a/action.h b/action.h index 5ec1098..f742ddc 100644 --- a/action.h +++ b/action.h @@ -125,6 +125,8 @@ public: bool is_conflicting_lock(const ModelAction *act) const; bool could_synchronize_with(const ModelAction *act) const; + Thread * get_thread_operand() const; + void create_cv(const ModelAction *parent = NULL); ClockVector * get_cv() const { return cv; } bool synchronize_with(const ModelAction *act); diff --git a/model.cc b/model.cc index 14b1aa3..84c4268 100644 --- a/model.cc +++ b/model.cc @@ -217,9 +217,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) /* Do not split atomic actions. */ if (curr->is_rmwr()) return thread_current(); - /* The THREAD_CREATE action points to the created Thread */ else if (curr->get_type() == THREAD_CREATE) - return (Thread *)curr->get_location(); + return curr->get_thread_operand(); } /* Have we completed exploring the preselected path? */ @@ -949,12 +948,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr) switch (curr->get_type()) { case THREAD_CREATE: { - Thread *th = (Thread *)curr->get_location(); + Thread *th = curr->get_thread_operand(); th->set_creation(curr); break; } case THREAD_JOIN: { - Thread *blocking = (Thread *)curr->get_location(); + Thread *blocking = curr->get_thread_operand(); ModelAction *act = get_last_action(blocking->get_id()); curr->synchronize_with(act); updated = true; /* trigger rel-seq checks */ -- 2.34.1