} 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))
* 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) {
*/
if (act->happens_before(curr) && act != curr) {
if (act->is_write()) {
- if (rf != act) {
+ if (!act->equals(rf)) {
mo_graph->addEdge(act, rf);
added = true;
}
if (prevreadfrom == NULL)
continue;
- if (rf != prevreadfrom) {
+ if (!prevreadfrom->equals(rf)) {
mo_graph->addEdge(prevreadfrom, rf);
added = true;
}
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);