For now, I write this "lazy check" as follows:
Whenever one of the following occurs:
* a Promise is fulfilled
* a mo_graph edge is added
Then I recheck all the actions (for the relevant object location) that are
waiting in the lazy release head queue.
/* Assign reads_from values */
Thread *th = get_thread(curr->get_tid());
uint64_t value = VALUE_NONE;
/* Assign reads_from values */
Thread *th = get_thread(curr->get_tid());
uint64_t value = VALUE_NONE;
if (curr->is_read()) {
const ModelAction *reads_from = curr->get_node()->get_read_from();
if (reads_from != NULL) {
value = reads_from->get_value();
/* Assign reads_from, perform release/acquire synchronization */
curr->read_from(reads_from);
if (curr->is_read()) {
const ModelAction *reads_from = curr->get_node()->get_read_from();
if (reads_from != NULL) {
value = reads_from->get_value();
/* Assign reads_from, perform release/acquire synchronization */
curr->read_from(reads_from);
- r_modification_order(curr,reads_from);
+ if (r_modification_order(curr,reads_from))
+ updated = true;
} else {
/* Read from future value */
value = curr->get_node()->get_future_value();
} else {
/* Read from future value */
value = curr->get_node()->get_future_value();
promises->push_back(valuepromise);
}
} else if (curr->is_write()) {
promises->push_back(valuepromise);
}
} else if (curr->is_write()) {
- w_modification_order(curr);
- resolve_promises(curr);
+ if (w_modification_order(curr))
+ updated = true;;
+ if (resolve_promises(curr))
+ updated = true;
+ if (updated)
+ resolve_release_sequences(curr->get_location());
+
th->set_return_value(value);
/* Add action to list. */
th->set_return_value(value);
/* Add action to list. */