} else if (!second_part_of_rmw) {
/* Read from future value */
struct future_value fv = curr->get_node()->get_future_value();
+ Promise *promise = new Promise(curr, fv);
value = fv.value;
- curr->set_value(fv.value);
- curr->set_read_from(NULL);
- promises->push_back(new Promise(curr, fv));
+ 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))
{
char buf[100];
char *ptr = buf;
- if (mo_graph->checkForRMWViolation())
- ptr += sprintf(ptr, "[RMW atomicity]");
if (mo_graph->checkForCycles())
ptr += sprintf(ptr, "[mo cycle]");
if (priv->failed_promise)
*/
bool ModelChecker::is_infeasible() const
{
- return mo_graph->checkForRMWViolation() ||
- mo_graph->checkForCycles() ||
+ return mo_graph->checkForCycles() ||
priv->failed_promise ||
priv->too_many_reads ||
priv->bad_synchronization ||
* read.
*
* Basic idea is the following: Go through each other thread and find
- * the lastest action that happened before our read. Two cases:
+ * the last action that happened before our read. Two cases:
*
* (1) The action is a write => that write must either occur before
* the write we read from or be the write we read from.
* must occur before the write we read from or be the same write.
*
* @param curr The current action. Must be a read.
- * @param rf The action that curr reads from. Must be a write.
+ * @param rf The ModelAction or Promise that curr reads from. Must be a write.
* @return True if modification order edges were added; false otherwise
*/
-bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
+template <typename rf_type>
+bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
{
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (act->is_write() && act != rf && act != curr) {
+ if (act->is_write() && !act->equals(rf) && act != curr) {
/* 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 (rf != act) {
- mo_graph->addEdge(act, rf);
- added = true;
+ if (!act->equals(rf)) {
+ added = mo_graph->addEdge(act, rf) || added;
}
} else {
const ModelAction *prevreadfrom = act->get_reads_from();
if (prevreadfrom == NULL)
continue;
- if (rf != prevreadfrom) {
- mo_graph->addEdge(prevreadfrom, rf);
- added = true;
+ if (!prevreadfrom->equals(rf)) {
+ added = mo_graph->addEdge(prevreadfrom, rf) || added;
}
}
break;
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;
}
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);
+ delete promise;
promises->erase(promises->begin() + promise_index);
actions_to_check.push_back(read);
void ModelChecker::print_summary() const
{
#if SUPPORT_MOD_ORDER_DUMP
- scheduler->print();
char buffername[100];
sprintf(buffername, "exec%04u", stats.num_total);
mo_graph->dumpGraphToFile(buffername);