From: bdemsky Date: Tue, 4 Jun 2019 04:53:31 +0000 (-0700) Subject: remove old release sequences X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=82f6d9ab97a87e874fb1b5dfa237266f4bfc95d1;p=c11tester.git remove old release sequences --- diff --git a/action.cc b/action.cc index 8395c885..bd958505 100644 --- a/action.cc +++ b/action.cc @@ -46,7 +46,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, sleep_flag(false) { /* References to NULL atomic variables can end up here */ - ASSERT(loc || type == ATOMIC_FENCE || type == MODEL_FIXUP_RELSEQ); + ASSERT(loc || type == ATOMIC_FENCE); Thread *t = thread ? thread : thread_current(); this->tid = t->get_id(); @@ -90,11 +90,6 @@ bool ModelAction::is_thread_join() const return type == THREAD_JOIN || type == PTHREAD_JOIN; } -bool ModelAction::is_relseq_fixup() const -{ - return type == MODEL_FIXUP_RELSEQ; -} - bool ModelAction::is_mutex_op() const { return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL; @@ -535,7 +530,6 @@ bool ModelAction::happens_before(const ModelAction *act) const const char * ModelAction::get_type_str() const { switch (this->type) { - case MODEL_FIXUP_RELSEQ: return "relseq fixup"; case THREAD_CREATE: return "thread create"; case THREAD_START: return "thread start"; case THREAD_YIELD: return "thread yield"; diff --git a/action.h b/action.h index 06d76c25..ef939284 100644 --- a/action.h +++ b/action.h @@ -50,8 +50,6 @@ using std::memory_order_seq_cst; /** @brief Represents an action type, identifying one of several types of * ModelAction */ typedef enum action_type { - MODEL_FIXUP_RELSEQ, /**< Special ModelAction: finalize a release - * sequence */ THREAD_CREATE, /**< A thread creation action */ THREAD_START, /**< First action in each thread */ THREAD_YIELD, /**< A thread yield action */ @@ -128,7 +126,6 @@ public: void set_try_lock(bool obtainedlock); bool is_thread_start() const; bool is_thread_join() const; - bool is_relseq_fixup() const; bool is_mutex_op() const; bool is_lock() const; bool is_trylock() const; diff --git a/execution.cc b/execution.cc index 7a51bca6..369498b0 100644 --- a/execution.cc +++ b/execution.cc @@ -745,9 +745,6 @@ bool ModelExecution::process_mutex(ModelAction *curr) */ bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work) { - /* Readers to which we may send our future value */ - ModelVector send_fv; - bool updated_mod_order = w_modification_order(curr); @@ -885,61 +882,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr) return updated; } -/** - * @brief Process the current action for release sequence fixup activity - * - * Performs model-checker release sequence fixups for the current action, - * forcing a single pending release sequence to break (with a given, potential - * "loose" write) or to complete (i.e., synchronize). If a pending release - * sequence forms a complete release sequence, then we must perform the fixup - * synchronization, mo_graph additions, etc. - * - * @param curr The current action; must be a release sequence fixup action - * @param work_queue The work queue to which to add work items as they are - * generated - */ -void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue) -{ - const ModelAction *write = curr->get_node()->get_relseq_break(); - struct release_seq *sequence = pending_rel_seqs.back(); - pending_rel_seqs.pop_back(); - ASSERT(sequence); - ModelAction *acquire = sequence->acquire; - const ModelAction *rf = sequence->rf; - const ModelAction *release = sequence->release; - ASSERT(acquire); - ASSERT(release); - ASSERT(rf); - ASSERT(release->same_thread(rf)); - - if (write == NULL) { - /** - * @todo Forcing a synchronization requires that we set - * modification order constraints. For instance, we can't allow - * a fixup sequence in which two separate read-acquire - * operations read from the same sequence, where the first one - * synchronizes and the other doesn't. Essentially, we can't - * allow any writes to insert themselves between 'release' and - * 'rf' - */ - - /* Must synchronize */ - if (!synchronize(release, acquire)) - return; - - /* Propagate the changed clock vector */ - propagate_clockvector(acquire, work_queue); - } else { - /* Break release sequence with new edges: - * release --mo--> write --mo--> rf */ - mo_graph->addEdge(release, write); - mo_graph->addEdge(write, rf); - } - - /* See if we have realized a data race */ - checkDataRaces(); -} - /** * Initialize the current action by performing one or more of the following * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward @@ -995,9 +937,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) * Perform one-time actions when pushing new ModelAction onto * NodeStack */ - if (newcurr->is_relseq_fixup()) - compute_relseq_breakwrites(newcurr); - else if (newcurr->is_wait()) + if (newcurr->is_wait()) newcurr->get_node()->set_misc_max(2); else if (newcurr->is_notify_one()) { newcurr->get_node()->set_misc_max(get_safe_ptr_action(&condvar_waiters_map, newcurr->get_location())->size()); @@ -1129,45 +1069,30 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) switch (work.type) { case WORK_CHECK_CURR_ACTION: { ModelAction *act = work.action; - bool update = false; /* update this location's release seq's */ - bool update_all = false; /* update all release seq's */ - if (process_thread_action(curr)) - update_all = true; + process_thread_action(curr); - if (act->is_read() && !second_part_of_rmw && process_read(act)) - update = true; + if (act->is_read() && !second_part_of_rmw) + process_read(act); - if (act->is_write() && process_write(act, &work_queue)) - update = true; + if (act->is_write()) + process_write(act, &work_queue); + + if (act->is_fence()) + process_fence(act); + + if (act->is_mutex_op()) + process_mutex(act); - if (act->is_fence() && process_fence(act)) - update_all = true; - - if (act->is_mutex_op() && process_mutex(act)) - update_all = true; - - if (act->is_relseq_fixup()) - process_relseq_fixup(curr, &work_queue); - - if (update_all) - work_queue.push_back(CheckRelSeqWorkEntry(NULL)); - else if (update) - work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); break; } - case WORK_CHECK_RELEASE_SEQ: - resolve_release_sequences(work.location, &work_queue); - break; case WORK_CHECK_MO_EDGES: { /** @todo Complete verification of work_queue */ ModelAction *act = work.action; - bool updated = false; if (act->is_read()) { const ModelAction *rf = act->get_reads_from(); - if (r_modification_order(act, rf)) - updated = true; + r_modification_order(act, rf); if (act->is_seqcst()) { ModelAction *last_sc_write = get_last_seq_cst_write(act); if (last_sc_write != NULL && rf->happens_before(last_sc_write)) { @@ -1176,13 +1101,9 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) } } if (act->is_write()) { - if (w_modification_order(act)) - updated = true; + w_modification_order(act); } mo_graph->commitChanges(); - - if (updated) - work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); break; } default: @@ -1203,8 +1124,7 @@ void ModelExecution::check_curr_backtracking(ModelAction *curr) if ((parnode && !parnode->backtrack_empty()) || !currnode->misc_empty() || - !currnode->read_from_empty() || - !currnode->relseq_break_empty()) { + !currnode->read_from_empty()) { set_latest_backtrack(curr); } } @@ -1216,7 +1136,7 @@ void ModelExecution::check_curr_backtracking(ModelAction *curr) */ bool ModelExecution::isfeasibleprefix() const { - return pending_rel_seqs.size() == 0 && is_feasible_prefix_ignore_relseq(); + return !is_infeasible(); } /** @@ -1242,16 +1162,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const model_print("%s: %s", prefix ? prefix : "Infeasible", buf); } -/** - * Returns whether the current completed trace is feasible, except for pending - * release sequences. - */ -bool ModelExecution::is_feasible_prefix_ignore_relseq() const -{ - return !is_infeasible() ; - -} - /** * Check if the current partial trace is infeasible. Does not check any * end-of-execution flags, which might rule out the execution. Thus, this is @@ -1852,8 +1762,6 @@ void ModelExecution::get_release_seq_heads(ModelAction *acquire, */ void ModelExecution::propagate_clockvector(ModelAction *acquire, work_queue_t *work) { - /* Re-check all pending release sequences */ - work->push_back(CheckRelSeqWorkEntry(NULL)); /* Re-check read-acquire for mo_graph edges */ work->push_back(MOEdgeWorkEntry(acquire)); @@ -2101,29 +2009,6 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const return get_parent_action(tid)->get_cv(); } -/** - * Compute the set of writes that may break the current pending release - * sequence. This information is extracted from previou release sequence - * calculations. - * - * @param curr The current ModelAction. Must be a release sequence fixup - * action. - */ -void ModelExecution::compute_relseq_breakwrites(ModelAction *curr) -{ - if (pending_rel_seqs.empty()) - return; - - struct release_seq *pending = pending_rel_seqs.back(); - for (unsigned int i = 0; i < pending->writes.size(); i++) { - const ModelAction *write = pending->writes[i]; - curr->get_node()->add_relseq_break(write); - } - - /* NULL means don't break the sequence; just synchronize */ - curr->get_node()->add_relseq_break(NULL); -} - /** * Build up an initial set of all past writes that this 'read' action may read * from, as well as any previously-observed future values that must still be valid. @@ -2445,26 +2330,3 @@ Thread * ModelExecution::take_step(ModelAction *curr) return action_select_next_thread(curr); } -/** - * Launch end-of-execution release sequence fixups only when - * the execution is otherwise feasible AND there are: - * - * (1) pending release sequences - * (2) pending assertions that could be invalidated by a change - * in clock vectors (i.e., data races) - * (3) no pending promises - */ -void ModelExecution::fixup_release_sequences() -{ - while (!pending_rel_seqs.empty() && - is_feasible_prefix_ignore_relseq() && - haveUnrealizedRaces()) { - model_print("*** WARNING: release sequence fixup action " - "(%zu pending release seuqence(s)) ***\n", - pending_rel_seqs.size()); - ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, - std::memory_order_seq_cst, NULL, VALUE_NONE, - model_thread); - take_step(fixup); - }; -} diff --git a/execution.h b/execution.h index 579e9b7c..bc7fb98e 100644 --- a/execution.h +++ b/execution.h @@ -71,7 +71,6 @@ public: const struct model_params * get_params() const { return params; } Thread * take_step(ModelAction *curr); - void fixup_release_sequences(); void print_summary() const; #if SUPPORT_MOD_ORDER_DUMP @@ -110,7 +109,6 @@ public: bool is_complete_execution() const; void print_infeasibility(const char *prefix) const; - bool is_feasible_prefix_ignore_relseq() const; bool is_infeasible() const; bool is_deadlocked() const; bool is_yieldblocked() const; @@ -154,7 +152,6 @@ private: bool process_mutex(ModelAction *curr); bool process_thread_action(ModelAction *curr); - void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue); bool read_from(ModelAction *act, const ModelAction *rf); bool synchronize(const ModelAction *first, ModelAction *second); @@ -168,7 +165,6 @@ private: ModelAction * get_last_conflict(ModelAction *act) const; void set_backtracking(ModelAction *act); bool set_latest_backtrack(ModelAction *act); - void compute_relseq_breakwrites(ModelAction *curr); void check_curr_backtracking(ModelAction *curr); void add_action_to_lists(ModelAction *act); @@ -187,7 +183,6 @@ private: bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const; void propagate_clockvector(ModelAction *acquire, work_queue_t *work); bool resolve_release_sequences(void *location, work_queue_t *work_queue); - void add_future_value(const ModelAction *writer, ModelAction *reader); ModelAction * get_uninitialized_action(const ModelAction *curr) const; action_list_t action_trace; diff --git a/main.cc b/main.cc index 0d4a6ad7..4d308a81 100644 --- a/main.cc +++ b/main.cc @@ -19,14 +19,11 @@ static void param_defaults(struct model_params *params) { params->maxreads = 0; - params->maxfuturedelay = 6; params->fairwindow = 0; params->yieldon = false; params->yieldblock = false; params->enabledcount = 1; params->bound = 0; - params->maxfuturevalues = 0; - params->expireslop = 4; params->verbose = !!DBG_ENABLED(); params->uninitvalue = 0; params->maxexecutions = 0; @@ -52,15 +49,6 @@ static void print_usage(const char *program_name, struct model_params *params) "-m, --liveness=NUM Maximum times a thread can read from the same write\n" " while other writes exist.\n" " Default: %d\n" -"-M, --maxfv=NUM Maximum number of future values that can be sent to\n" -" the same read.\n" -" Default: %d\n" -"-s, --maxfvdelay=NUM Maximum actions that the model checker will wait for\n" -" a write from the future past the expected number\n" -" of actions.\n" -" Default: %d\n" -"-S, --fvslop=NUM Future value expiration sloppiness.\n" -" Default: %u\n" "-y, --yield Enable CHESS-like yield-based fairness support\n" " (requires thrd_yield() in test program).\n" " Default: %s\n" @@ -89,16 +77,13 @@ static void print_usage(const char *program_name, struct model_params *params) " -- Program arguments follow.\n\n", program_name, params->maxreads, - params->maxfuturevalues, - params->maxfuturedelay, - params->expireslop, params->yieldon ? "enabled" : "disabled", params->yieldblock ? "enabled" : "disabled", params->fairwindow, params->enabledcount, params->bound, params->verbose, - params->uninitvalue, + params->uninitvalue, params->maxexecutions); exit(EXIT_SUCCESS); @@ -106,13 +91,10 @@ static void print_usage(const char *program_name, struct model_params *params) static void parse_options(struct model_params *params, int argc, char **argv) { - const char *shortopts = "hyYt:o:m:M:s:S:f:e:b:u:x:v::"; + const char *shortopts = "hyYt:o:m:f:e:b:u:x:v::"; const struct option longopts[] = { {"help", no_argument, NULL, 'h'}, {"liveness", required_argument, NULL, 'm'}, - {"maxfv", required_argument, NULL, 'M'}, - {"maxfvdelay", required_argument, NULL, 's'}, - {"fvslop", required_argument, NULL, 'S'}, {"fairness", required_argument, NULL, 'f'}, {"yield", no_argument, NULL, 'y'}, {"yieldblock", no_argument, NULL, 'Y'}, @@ -135,12 +117,6 @@ static void parse_options(struct model_params *params, int argc, char **argv) case 'x': params->maxexecutions = atoi(optarg); break; - case 's': - params->maxfuturedelay = atoi(optarg); - break; - case 'S': - params->expireslop = atoi(optarg); - break; case 'f': params->fairwindow = atoi(optarg); break; @@ -153,9 +129,6 @@ static void parse_options(struct model_params *params, int argc, char **argv) case 'm': params->maxreads = atoi(optarg); break; - case 'M': - params->maxfuturevalues = atoi(optarg); - break; case 'v': params->verbose = optarg ? atoi(optarg) : 1; break; diff --git a/model.cc b/model.cc index 6f6ba3ec..6f289686 100644 --- a/model.cc +++ b/model.cc @@ -544,7 +544,6 @@ void ModelChecker::run() i++; } while (i<2); // while (has_next); - execution->fixup_release_sequences(); model_print("******* Model-checking complete: *******\n"); print_stats(); diff --git a/nodestack.cc b/nodestack.cc index e3bccc99..f6761389 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -42,8 +42,6 @@ Node::Node(const struct model_params *params, ModelAction *act, Node *par, enabled_array(NULL), read_from_past(), read_from_past_idx(0), - relseq_break_writes(), - relseq_break_index(0), misc_index(0), misc_max(0), yield_data(NULL) @@ -175,7 +173,6 @@ void Node::print() const model_print("\n"); model_print(" misc: %s\n", misc_empty() ? "empty" : "non-empty"); - model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty"); } /****************************** threads backtracking **************************/ @@ -442,61 +439,6 @@ bool Node::increment_read_from_past() /************************** end read from past ********************************/ -/*********************** breaking release sequences ***************************/ - -/** - * Add a write ModelAction to the set of writes that may break the release - * sequence. This is used during replay exploration of pending release - * sequences. This Node must correspond to a release sequence fixup action. - * - * @param write The write that may break the release sequence. NULL means we - * allow the release sequence to synchronize. - */ -void Node::add_relseq_break(const ModelAction *write) -{ - relseq_break_writes.push_back(write); -} - -/** - * Get the write that may break the current pending release sequence, - * according to the replay / divergence pattern. - * - * @return A write that may break the release sequence. If NULL, that means - * the release sequence should not be broken. - */ -const ModelAction * Node::get_relseq_break() const -{ - if (relseq_break_index < (int)relseq_break_writes.size()) - return relseq_break_writes[relseq_break_index]; - else - return NULL; -} - -/** - * Increments the index into the relseq_break_writes set to explore the next - * item. - * @return Returns false if we have explored all values. - */ -bool Node::increment_relseq_break() -{ - DBG(); - if (relseq_break_index < ((int)relseq_break_writes.size())) { - relseq_break_index++; - return (relseq_break_index < ((int)relseq_break_writes.size())); - } - return false; -} - -/** - * @return True if all writes that may break the release sequence have been - * explored - */ -bool Node::relseq_break_empty() const -{ - return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size())); -} - -/******************* end breaking release sequences ***************************/ /** * Increments some behavior's index, if a new behavior is available @@ -510,9 +452,6 @@ bool Node::increment_behaviors() /* read from a different value */ if (increment_read_from()) return true; - /* resolve a release sequence differently */ - if (increment_relseq_break()) - return true; return false; } diff --git a/nodestack.h b/nodestack.h index b7e630b0..702c9931 100644 --- a/nodestack.h +++ b/nodestack.h @@ -98,11 +98,6 @@ public: bool increment_misc(); bool misc_empty() const; - void add_relseq_break(const ModelAction *write); - const ModelAction * get_relseq_break() const; - bool increment_relseq_break(); - bool relseq_break_empty() const; - bool increment_behaviors(); void print() const; @@ -113,8 +108,6 @@ private: int get_yield_data(int tid1, int tid2) const; bool read_from_past_empty() const; bool increment_read_from_past(); - bool future_value_empty() const; - bool increment_future_value(); read_from_type_t read_from_status; const struct model_params * get_params() const { return params; } @@ -140,9 +133,6 @@ private: ModelVector read_from_past; unsigned int read_from_past_idx; - ModelVector relseq_break_writes; - int relseq_break_index; - int misc_index; int misc_max; int * yield_data; diff --git a/params.h b/params.h index d5fd1cb3..0b1c5bf7 100644 --- a/params.h +++ b/params.h @@ -7,7 +7,6 @@ */ struct model_params { int maxreads; - int maxfuturedelay; bool yieldon; bool yieldblock; unsigned int fairwindow; @@ -16,15 +15,6 @@ struct model_params { unsigned int uninitvalue; int maxexecutions; - /** @brief Maximum number of future values that can be sent to the same - * read */ - int maxfuturevalues; - - /** @brief Only generate a new future value/expiration pair if the - * expiration time exceeds the existing one by more than the slop - * value */ - unsigned int expireslop; - /** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */ int verbose; diff --git a/pthread.cc b/pthread.cc index 723e60b5..e5bc9018 100644 --- a/pthread.cc +++ b/pthread.cc @@ -17,14 +17,11 @@ static void param_defaults(struct model_params *params) { params->maxreads = 0; - params->maxfuturedelay = 6; params->fairwindow = 0; params->yieldon = false; params->yieldblock = false; params->enabledcount = 1; params->bound = 0; - params->maxfuturevalues = 0; - params->expireslop = 4; params->verbose = !!DBG_ENABLED(); params->uninitvalue = 0; params->maxexecutions = 0; diff --git a/workqueue.h b/workqueue.h index 90347883..be0188b3 100644 --- a/workqueue.h +++ b/workqueue.h @@ -27,12 +27,6 @@ class WorkQueueEntry { /** @brief Type of work queue entry */ model_work_t type; - /** - * @brief Object affected - * @see CheckRelSeqWorkEntry - */ - void *location; - /** * @brief The ModelAction to work on * @see MOEdgeWorkEntry @@ -55,31 +49,10 @@ class CheckCurrWorkEntry : public WorkQueueEntry { */ CheckCurrWorkEntry(ModelAction *curr) { type = WORK_CHECK_CURR_ACTION; - location = NULL; action = curr; } }; -/** - * @brief Work: check an object location for resolved release sequences - * - * This WorkQueueEntry checks synchronization and the mo_graph for resolution - * of any release sequences. The object @a location is the only relevant - * parameter to this entry. - */ -class CheckRelSeqWorkEntry : public WorkQueueEntry { - public: - /** - * @brief Constructor for a "check release sequences" work entry - * @param l The location which must be checked for release sequences - */ - CheckRelSeqWorkEntry(void *l) { - type = WORK_CHECK_RELEASE_SEQ; - location = l; - action = NULL; - } -}; - /** * @brief Work: check a ModelAction for new mo_graph edges * @@ -96,7 +69,6 @@ class MOEdgeWorkEntry : public WorkQueueEntry { */ MOEdgeWorkEntry(ModelAction *updated) { type = WORK_CHECK_MO_EDGES; - location = NULL; action = updated; } };