X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=execution.cc;h=4496b9c63deeca6fa8198ec086425ba8fa1d6932;hp=a74147be4bbe7e068a9ddd05a58ff459ccb1a7c8;hb=98dd349fcc6e59853e3b54f33ea449527fcd9382;hpb=3a4e118d45bf83a3b4c3a0a73d1071fa8fe5476d diff --git a/execution.cc b/execution.cc index a74147b..4496b9c 100644 --- a/execution.cc +++ b/execution.cc @@ -58,7 +58,7 @@ struct model_snapshot_members { /** @brief Constructor */ ModelExecution::ModelExecution(ModelChecker *m, - struct model_params *params, + const struct model_params *params, Scheduler *scheduler, NodeStack *node_stack) : model(m), @@ -264,6 +264,28 @@ bool ModelExecution::is_deadlocked() const return blocking_threads; } +/** + * @brief Check if we are yield-blocked + * + * A program can be "yield-blocked" if all threads are ready to execute a + * yield. + * + * @return True if the program is yield-blocked; false otherwise + */ +bool ModelExecution::is_yieldblocked() const +{ + if (!params->yieldblock) + return false; + + for (unsigned int i = 0; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + Thread *t = get_thread(tid); + if (t->get_pending() && t->get_pending()->is_yield()) + return true; + } + return false; +} + /** * Check if this is a complete execution. That is, have all thread completed * execution (rather than exiting because sleep sets have forced a redundant @@ -273,6 +295,8 @@ bool ModelExecution::is_deadlocked() const */ bool ModelExecution::is_complete_execution() const { + if (is_yieldblocked()) + return false; for (unsigned int i = 0; i < get_num_threads(); i++) if (is_enabled(int_to_id(i))) return false; @@ -793,9 +817,10 @@ void ModelExecution::add_future_value(const ModelAction *writer, ModelAction *re /** * Process a write ModelAction * @param curr The ModelAction to process + * @param work The work queue, for adding fixup work * @return True if the mo_graph was updated or promises were resolved */ -bool ModelExecution::process_write(ModelAction *curr) +bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work) { /* Readers to which we may send our future value */ ModelVector send_fv; @@ -808,7 +833,7 @@ bool ModelExecution::process_write(ModelAction *curr) if (promise) { earliest_promise_reader = promise->get_reader(0); - updated_promises = resolve_promise(curr, promise); + updated_promises = resolve_promise(curr, promise, work); } else earliest_promise_reader = NULL; @@ -1001,21 +1026,9 @@ void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_ /* Must synchronize */ if (!synchronize(release, acquire)) return; - /* Re-check all pending release sequences */ - work_queue->push_back(CheckRelSeqWorkEntry(NULL)); - /* Re-check act for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(acquire)); - - /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace.rbegin(); - for (; (*rit) != acquire; rit++) { - ModelAction *propagate = *rit; - if (acquire->happens_before(propagate)) { - synchronize(acquire, propagate); - /* Re-check 'propagate' for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(propagate)); - } - } + + /* Propagate the changed clock vector */ + propagate_clockvector(acquire, work_queue); } else { /* Break release sequence with new edges: * release --mo--> write --mo--> rf */ @@ -1181,9 +1194,10 @@ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *wai /** * @brief Check whether a model action is enabled. * - * Checks whether a lock or join operation would be successful (i.e., is the - * lock already locked, or is the joined thread already complete). If not, put - * the action in a waiter list. + * Checks whether an operation would be successful (i.e., is a lock already + * locked, or is the joined thread already complete). + * + * For yield-blocking, yields are never enabled. * * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled. @@ -1200,6 +1214,8 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { thread_blocking_check_promises(blocking, get_thread(curr)); return false; } + } else if (params->yieldblock && curr->is_yield()) { + return false; } return true; @@ -1257,7 +1273,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (act->is_read() && !second_part_of_rmw && process_read(act)) update = true; - if (act->is_write() && process_write(act)) + if (act->is_write() && process_write(act, &work_queue)) update = true; if (act->is_fence() && process_fence(act)) @@ -2035,6 +2051,37 @@ void ModelExecution::get_release_seq_heads(ModelAction *acquire, } } +/** + * @brief Propagate a modified clock vector to actions later in the execution + * order + * + * After an acquire operation lazily completes a release-sequence + * synchronization, we must update all clock vectors for operations later than + * the acquire in the execution order. + * + * @param acquire The ModelAction whose clock vector must be propagated + * @param work The work queue to which we can add work items, if this + * propagation triggers more updates (e.g., to the modification order) + */ +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)); + + /* propagate synchronization to later actions */ + action_list_t::reverse_iterator rit = action_trace.rbegin(); + for (; (*rit) != acquire; rit++) { + ModelAction *propagate = *rit; + if (acquire->happens_before(propagate)) { + synchronize(acquire, propagate); + /* Re-check 'propagate' for mo_graph edges */ + work->push_back(MOEdgeWorkEntry(propagate)); + } + } +} + /** * Attempt to resolve all stashed operations that might synchronize with a * release sequence for a given location. This implements the "lazy" portion of @@ -2073,22 +2120,8 @@ bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *wor updated = true; if (updated) { - /* Re-check all pending release sequences */ - work_queue->push_back(CheckRelSeqWorkEntry(NULL)); - /* Re-check read-acquire for mo_graph edges */ - if (acquire->is_read()) - work_queue->push_back(MOEdgeWorkEntry(acquire)); - - /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace.rbegin(); - for (; (*rit) != acquire; rit++) { - ModelAction *propagate = *rit; - if (acquire->happens_before(propagate)) { - synchronize(acquire, propagate); - /* Re-check 'propagate' for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(propagate)); - } - } + /* Propagate the changed clock vector */ + propagate_clockvector(acquire, work_queue); } if (complete) { it = pending_rel_seqs.erase(it); @@ -2301,15 +2334,20 @@ Promise * ModelExecution::pop_promise_to_resolve(const ModelAction *curr) * Resolve a Promise with a current write. * @param write The ModelAction that is fulfilling Promises * @param promise The Promise to resolve + * @param work The work queue, for adding new fixup work * @return True if the Promise was successfully resolved; false otherwise */ -bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise) +bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise, + work_queue_t *work) { ModelVector actions_to_check; for (unsigned int i = 0; i < promise->get_num_readers(); i++) { ModelAction *read = promise->get_reader(i); - read_from(read, write); + if (read_from(read, write)) { + /* Propagate the changed clock vector */ + propagate_clockvector(read, work); + } actions_to_check.push_back(read); } /* Make sure the promise's value matches the write's value */ @@ -2616,7 +2654,7 @@ void ModelExecution::dumpGraph(char *filename) const mo_graph->dumpNodes(file); ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads()); - for (action_list_t::iterator it = action_trace.begin(); it != action_trace.end(); it++) { + for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) { ModelAction *act = *it; if (act->is_read()) { mo_graph->dot_print_node(file, act); @@ -2659,6 +2697,8 @@ void ModelExecution::print_summary() const model_print("Execution %d:", get_execution_number()); if (isfeasibleprefix()) { + if (is_yieldblocked()) + model_print(" YIELD BLOCKED"); if (scheduler->all_threads_sleeping()) model_print(" SLEEP-SET REDUNDANT"); model_print("\n"); @@ -2816,7 +2856,7 @@ void ModelExecution::fixup_release_sequences() { while (!pending_rel_seqs.empty() && is_feasible_prefix_ignore_relseq() && - !unrealizedraces.empty()) { + haveUnrealizedRaces()) { model_print("*** WARNING: release sequence fixup action " "(%zu pending release seuqence(s)) ***\n", pending_rel_seqs.size());