value = fv.value;
curr->set_read_from_promise(promise);
promises->push_back(promise);
+ mo_graph->startChanges();
+ updated = r_modification_order(curr, promise);
+ mo_graph->commitChanges();
}
get_thread(curr)->set_return_value(value);
return updated;
if (act->is_read()) {
const ModelAction *rf = act->get_reads_from();
- if (rf != NULL && r_modification_order(act, rf))
- updated = true;
+ const Promise *promise = act->get_reads_from_promise();
+ if (rf) {
+ if (r_modification_order(act, rf))
+ updated = true;
+ } else if (promise) {
+ if (r_modification_order(act, promise))
+ updated = true;
+ }
}
if (act->is_write()) {
if (w_modification_order(act))
ModelAction * ModelChecker::process_rmw(ModelAction *act) {
ModelAction *lastread = get_last_action(act->get_tid());
lastread->process_rmw(act);
- if (act->is_rmw() && lastread->get_reads_from() != NULL) {
- mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+ if (act->is_rmw()) {
+ if (lastread->get_reads_from())
+ mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+ else
+ mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread);
mo_graph->commitChanges();
}
return lastread;
/* C++, Section 29.3 statement 5 */
if (curr->is_seqcst() && last_sc_fence_thread_local &&
*act < *last_sc_fence_thread_local) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
/* C++, Section 29.3 statement 4 */
else if (act->is_seqcst() && last_sc_fence_local &&
*act < *last_sc_fence_local) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
/* C++, Section 29.3 statement 6 */
else if (last_sc_fence_thread_before &&
*act < *last_sc_fence_thread_before) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
}
if (act->happens_before(curr) && act != curr) {
if (act->is_write()) {
if (!act->equals(rf)) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
}
} else {
const ModelAction *prevreadfrom = act->get_reads_from();
continue;
if (!prevreadfrom->equals(rf)) {
- mo_graph->addEdge(prevreadfrom, rf);
- added = true;
+ added = mo_graph->addEdge(prevreadfrom, rf) || added;
}
}
break;
return added;
}
-/** This method fixes up the modification order when we resolve a
- * promises. The basic problem is that actions that occur after the
- * read curr could not property add items to the modification order
- * for our read.
- *
- * So for each thread, we find the earliest item that happens after
- * the read curr. This is the item we have to fix up with additional
- * constraints. If that action is write, we add a MO edge between
- * the Action rf and that action. If the action is a read, we add a
- * MO edge between the Action rf, and whatever the read accessed.
- *
- * @param curr is the read ModelAction that we are fixing up MO edges for.
- * @param rf is the write ModelAction that curr reads from.
- *
- */
-void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
-{
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
- unsigned int i;
- ASSERT(curr->is_read());
-
- /* Iterate over all threads */
- for (i = 0; i < thrd_lists->size(); i++) {
- /* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- ModelAction *lastact = NULL;
-
- /* Find last action that happens after curr that is either not curr or a rmw */
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
- if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
- lastact = act;
- } else
- break;
- }
-
- /* Include at most one act per-thread that "happens before" curr */
- if (lastact != NULL) {
- if (lastact == curr) {
- //Case 1: The resolved read is a RMW, and we need to make sure
- //that the write portion of the RMW mod order after rf
-
- mo_graph->addEdge(rf, lastact);
- } else if (lastact->is_read()) {
- //Case 2: The resolved read is a normal read and the next
- //operation is a read, and we need to make sure the value read
- //is mod ordered after rf
-
- const ModelAction *postreadfrom = lastact->get_reads_from();
- if (postreadfrom != NULL && rf != postreadfrom)
- mo_graph->addEdge(rf, postreadfrom);
- } else {
- //Case 3: The resolved read is a normal read and the next
- //operation is a write, and we need to make sure that the
- //write is mod ordered after rf
- if (lastact != rf)
- mo_graph->addEdge(rf, lastact);
- }
- break;
- }
- }
-}
-
/**
* Updates the mo_graph with the constraints imposed from the current write.
*
so we are initialized. */
ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
if (last_seq_cst != NULL) {
- mo_graph->addEdge(last_seq_cst, curr);
- added = true;
+ added = mo_graph->addEdge(last_seq_cst, curr) || added;
}
}
/* C++, Section 29.3 statement 7 */
if (last_sc_fence_thread_before && act->is_write() &&
*act < *last_sc_fence_thread_before) {
- mo_graph->addEdge(act, curr);
- added = true;
+ added = mo_graph->addEdge(act, curr) || added;
break;
}
* readfrom(act) --mo--> act
*/
if (act->is_write())
- mo_graph->addEdge(act, curr);
+ added = mo_graph->addEdge(act, curr) || added;
else if (act->is_read()) {
//if previous read accessed a null, just keep going
if (act->get_reads_from() == NULL)
continue;
- mo_graph->addEdge(act->get_reads_from(), curr);
+ added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
}
- added = true;
break;
} else if (act->is_read() && !act->could_synchronize_with(curr) &&
!act->same_thread(curr)) {
}
}
+ /*
+ * All compatible, thread-exclusive promises must be ordered after any
+ * concrete stores to the same thread, or else they can be merged with
+ * this store later
+ */
+ for (unsigned int i = 0; i < promises->size(); i++)
+ if ((*promises)[i]->is_compatible_exclusive(curr))
+ added = mo_graph->addEdge(curr, (*promises)[i]) || added;
+
return added;
}
*/
bool ModelChecker::resolve_promises(ModelAction *write)
{
- bool resolved = false;
+ 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)) {
ModelAction *read = promise->get_action();
- if (read->is_rmw()) {
- mo_graph->addRMWEdge(write, read);
- }
read_from(read, write);
- //First fix up the modification order for actions that happened
- //before the read
- r_modification_order(read, write);
- //Next fix up the modification order for actions that happened
- //after the read.
- post_r_modification_order(read, write);
//Make sure the promise's value matches the write's value
- ASSERT(promise->get_value() == write->get_value());
- delete promise;
+ ASSERT(promise->is_compatible(write));
+ mo_graph->resolvePromise(read, write, &mustResolve);
+ resolved.push_back(promise);
promises->erase(promises->begin() + promise_index);
actions_to_check.push_back(read);
- resolved = true;
+ haveResolved = true;
} else
promise_index++;
}
+ 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
for (unsigned int i = 0; i < actions_to_check.size(); i++) {
- ModelAction *read=actions_to_check[i];
+ ModelAction *read = actions_to_check[i];
mo_check_promises(read->get_tid(), write, read);
}
- return resolved;
+ return haveResolved;
}
/**
*/
void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
{
- void *location = write->get_location();
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
const ModelAction *act = promise->get_action();
// Is this promise on the same location?
- if (act->get_location() != location)
+ if (!act->same_var(write))
continue;
// same thread as the promise
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=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
+ 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());
}
projects / model-checker.git / blobdiff