From: Brian Norris Date: Wed, 3 Oct 2012 00:29:56 +0000 (-0700) Subject: model: remove obsolete ModelChecker::do_complete_join() X-Git-Tag: pldi2013~121^2~2 X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=cef10a2b49af5da16ffe59c5b9ddd210c668fbac;p=model-checker.git model: remove obsolete ModelChecker::do_complete_join() This function was folded into the one place it is used, now. --- diff --git a/model.cc b/model.cc index ce9e066..097da8a 100644 --- a/model.cc +++ b/model.cc @@ -697,19 +697,6 @@ 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(); diff --git a/model.h b/model.h index 6f082c6..867ec03 100644 --- a/model.h +++ b/model.h @@ -152,7 +152,6 @@ private: bool w_modification_order(ModelAction *curr); 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; ModelAction *earliest_diverge;