X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=acecd5a6e20f6b512cef0d9e136db4422d8078d8;hb=d70f6f259c9850e5fceb527e3a9541c440c0146b;hp=84c20eb5c42f0ff9b1fa4f3ef668aa6432b793d5;hpb=0e8659aba12909cfc5785163022378519837710e;p=model-checker.git 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.