stats.num_buggy_executions++;
else if (is_complete_execution())
stats.num_complete++;
- else if (scheduler->all_threads_sleeping())
+ else {
stats.num_redundant++;
- else
- ASSERT(false);
+
+ /**
+ * @todo We can violate this ASSERT() when fairness/sleep sets
+ * conflict to cause an execution to terminate, e.g. with:
+ * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
+ */
+ //ASSERT(scheduler->all_threads_sleeping());
+ }
}
/** @brief Print execution stats */
write_thread = write_thread->get_parent();
struct future_value fv = {
- writer->get_value(),
+ writer->get_write_value(),
writer->get_seq_number() + params.maxfuturedelay,
write_thread->get_id(),
};
*/
bool ModelChecker::process_write(ModelAction *curr)
{
- bool updated_mod_order = w_modification_order(curr);
- bool updated_promises = resolve_promises(curr);
+ /* Readers to which we may send our future value */
+ std::vector< ModelAction *, ModelAlloc<ModelAction *> > send_fv;
+
+ bool updated_mod_order = w_modification_order(curr, &send_fv);
+ int promise_idx = get_promise_to_resolve(curr);
+ const ModelAction *earliest_promise_reader;
+ bool updated_promises = false;
+
+ if (promise_idx >= 0) {
+ earliest_promise_reader = (*promises)[promise_idx]->get_reader(0);
+ updated_promises = resolve_promise(curr, promise_idx);
+ } else
+ earliest_promise_reader = NULL;
+
+ /* Don't send future values to reads after the Promise we resolve */
+ for (unsigned int i = 0; i < send_fv.size(); i++) {
+ ModelAction *read = send_fv[i];
+ if (!earliest_promise_reader || *read < *earliest_promise_reader)
+ futurevalues->push_back(PendingFutureValue(curr, read));
+ }
if (promises->size() == 0) {
for (unsigned int i = 0; i < futurevalues->size(); i++) {
*/
bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
{
+ ASSERT(rf);
act->set_read_from(rf);
- if (rf != NULL && act->is_acquire()) {
+ if (act->is_acquire()) {
rel_heads_list_t release_heads;
get_release_seq_heads(act, act, &release_heads);
int num_heads = release_heads.size();
}
}
if (act->is_write()) {
- if (w_modification_order(act))
+ if (w_modification_order(act, NULL))
updated = true;
}
mo_graph->commitChanges();
*/
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
{
- if (params.maxreads != 0) {
- if (curr->get_node()->get_read_from_past_size() <= 1)
+ if (!params.maxreads)
+ return;
+ if (curr->get_node()->get_read_from_past_size() <= 1)
+ return;
+ /* Must make sure that execution is currently feasible... We could
+ * accidentally clear by rolling back */
+ if (is_infeasible())
+ return;
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ int tid = id_to_int(curr->get_tid());
+
+ /* Skip checks */
+ if ((int)thrd_lists->size() <= tid)
+ return;
+ action_list_t *list = &(*thrd_lists)[tid];
+
+ action_list_t::reverse_iterator rit = list->rbegin();
+ /* Skip past curr */
+ for (; (*rit) != curr; rit++)
+ ;
+ /* go past curr now */
+ rit++;
+
+ action_list_t::reverse_iterator ritcopy = rit;
+ /* See if we have enough reads from the same value */
+ int count = 0;
+ for (; count < params.maxreads; rit++, count++) {
+ if (rit == list->rend())
return;
- //Must make sure that execution is currently feasible... We could
- //accidentally clear by rolling back
- if (is_infeasible())
+ ModelAction *act = *rit;
+ if (!act->is_read())
return;
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
- int tid = id_to_int(curr->get_tid());
- /* Skip checks */
- if ((int)thrd_lists->size() <= tid)
+ if (act->get_reads_from() != rf)
return;
- action_list_t *list = &(*thrd_lists)[tid];
-
- action_list_t::reverse_iterator rit = list->rbegin();
- /* Skip past curr */
- for (; (*rit) != curr; rit++)
- ;
- /* go past curr now */
- rit++;
-
- action_list_t::reverse_iterator ritcopy = rit;
- //See if we have enough reads from the same value
- int count = 0;
- for (; count < params.maxreads; rit++, count++) {
- if (rit == list->rend())
- return;
- ModelAction *act = *rit;
- if (!act->is_read())
- return;
-
- if (act->get_reads_from() != rf)
- return;
- if (act->get_node()->get_read_from_past_size() <= 1)
- return;
- }
- for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
- /* Get write */
- const ModelAction *write = curr->get_node()->get_read_from_past(i);
+ if (act->get_node()->get_read_from_past_size() <= 1)
+ return;
+ }
+ for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
+ /* Get write */
+ const ModelAction *write = curr->get_node()->get_read_from_past(i);
- /* Need a different write */
- if (write == rf)
- continue;
+ /* Need a different write */
+ if (write == rf)
+ continue;
- /* Test to see whether this is a feasible write to read from */
- /** NOTE: all members of read-from set should be
- * feasible, so we no longer check it here **/
+ /* Test to see whether this is a feasible write to read from */
+ /** NOTE: all members of read-from set should be
+ * feasible, so we no longer check it here **/
- rit = ritcopy;
+ rit = ritcopy;
- bool feasiblewrite = true;
- //new we need to see if this write works for everyone
+ bool feasiblewrite = true;
+ /* now we need to see if this write works for everyone */
- for (int loop = count; loop > 0; loop--, rit++) {
- ModelAction *act = *rit;
- bool foundvalue = false;
- for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
- if (act->get_node()->get_read_from_past(j) == write) {
- foundvalue = true;
- break;
- }
- }
- if (!foundvalue) {
- feasiblewrite = false;
+ for (int loop = count; loop > 0; loop--, rit++) {
+ ModelAction *act = *rit;
+ bool foundvalue = false;
+ for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
+ if (act->get_node()->get_read_from_past(j) == write) {
+ foundvalue = true;
break;
}
}
- if (feasiblewrite) {
- priv->too_many_reads = true;
- return;
+ if (!foundvalue) {
+ feasiblewrite = false;
+ break;
}
}
+ if (feasiblewrite) {
+ priv->too_many_reads = true;
+ return;
+ }
}
}
* (II) Sending the write back to non-synchronizing reads.
*
* @param curr The current action. Must be a write.
+ * @param send_fv A vector for stashing reads to which we may pass our future
+ * value. If NULL, then don't record any future values.
* @return True if modification order edges were added; false otherwise
*/
-bool ModelChecker::w_modification_order(ModelAction *curr)
+bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv)
{
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
pendingfuturevalue.
*/
- if (thin_air_constraint_may_allow(curr, act)) {
+ if (send_fv && thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible())
- futurevalues->push_back(PendingFutureValue(curr, act));
+ send_fv->push_back(act);
else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
add_future_value(curr, act);
}
}
/**
- * Resolve a set of Promises with a current write. The set is provided in the
- * Node corresponding to @a write.
+ * @brief Find the promise, if any to resolve for the current action
+ * @param curr The current ModelAction. Should be a write.
+ * @return The (non-negative) index for the Promise to resolve, if any;
+ * otherwise -1
+ */
+int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
+{
+ for (unsigned int i = 0; i < promises->size(); i++)
+ if (curr->get_node()->get_promise(i))
+ return i;
+ return -1;
+}
+
+/**
+ * Resolve a Promise with a current write.
* @param write The ModelAction that is fulfilling Promises
- * @return True if promises were resolved; false otherwise
+ * @param promise_idx The index corresponding to the promise
+ * @return True if the Promise was successfully resolved; false otherwise
*/
-bool ModelChecker::resolve_promises(ModelAction *write)
+bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
{
- bool haveResolved = false;
std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
- promise_list_t mustResolve, resolved;
-
- for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
- Promise *promise = (*promises)[promise_index];
- if (write->get_node()->get_promise(i)) {
- for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
- ModelAction *read = promise->get_reader(j);
- read_from(read, write);
- actions_to_check.push_back(read);
- }
- //Make sure the promise's value matches the write's value
- ASSERT(promise->is_compatible(write));
- mo_graph->resolvePromise(promise, write, &mustResolve);
+ promise_list_t mustResolve;
+ Promise *promise = (*promises)[promise_idx];
- resolved.push_back(promise);
- promises->erase(promises->begin() + promise_index);
-
- haveResolved = true;
- } else
- promise_index++;
+ for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
+ ModelAction *read = promise->get_reader(i);
+ read_from(read, write);
+ actions_to_check.push_back(read);
}
+ /* Make sure the promise's value matches the write's value */
+ ASSERT(promise->is_compatible(write) && promise->same_value(write));
+ mo_graph->resolvePromise(promise, write, &mustResolve);
+
+ promises->erase(promises->begin() + promise_idx);
+
+ /** @todo simplify the 'mustResolve' stuff */
+ ASSERT(mustResolve.size() <= 1);
+
+ if (!mustResolve.empty() && mustResolve[0] != promise)
+ priv->failed_promise = true;
+ delete promise;
- for (unsigned int i = 0; i < mustResolve.size(); i++) {
- if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
- == resolved.end())
- priv->failed_promise = true;
- }
- for (unsigned int i = 0; i < resolved.size(); i++)
- delete resolved[i];
//Check whether reading these writes has made threads unable to
//resolve promises
mo_check_promises(read, true);
}
- return haveResolved;
+ return true;
}
/**
{
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
- if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value())
+ if (!promise->is_compatible(curr) || !promise->same_value(curr))
continue;
bool satisfy = true;
Promise *promise = (*promises)[i];
// Is this promise on the same location?
- if (promise->get_value() != write->get_value())
+ if (!promise->same_location(write))
continue;
for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
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++) {
- ModelAction *action = *it;
- if (action->is_read()) {
- fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
- if (action->get_reads_from() != NULL)
- fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+ ModelAction *act = *it;
+ if (act->is_read()) {
+ mo_graph->dot_print_node(file, act);
+ if (act->get_reads_from())
+ mo_graph->dot_print_edge(file,
+ act->get_reads_from(),
+ act,
+ "label=\"rf\", color=red, weight=2");
+ else
+ mo_graph->dot_print_edge(file,
+ act->get_reads_from_promise(),
+ act,
+ "label=\"rf\", color=red");
}
- if (thread_array[action->get_tid()] != NULL) {
- fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
+ if (thread_array[act->get_tid()]) {
+ mo_graph->dot_print_edge(file,
+ thread_array[id_to_int(act->get_tid())],
+ act,
+ "label=\"sb\", color=blue, weight=400");
}
- thread_array[action->get_tid()] = action;
+ thread_array[act->get_tid()] = act;
}
fprintf(file, "}\n");
model_free(thread_array);