if any promise for a thread resolved, we assumed that the corresponding
write happened after all promises for that threads...clearly doesn't
need to be the case...
[Brian Norris:] This fixes some bugs where we don't see all the expected
behaviors: e.g., with
./run.sh test/rmwprog.o -- 3
Now we see all 20 behaviors.
read_from(curr, reads_from);
mo_graph->commitChanges();
read_from(curr, reads_from);
mo_graph->commitChanges();
- mo_check_promises(curr->get_tid(), reads_from);
+ mo_check_promises(curr->get_tid(), reads_from, NULL);
updated |= r_status;
} else if (!second_part_of_rmw) {
updated |= r_status;
} else if (!second_part_of_rmw) {
}
mo_graph->commitChanges();
}
mo_graph->commitChanges();
- mo_check_promises(curr->get_tid(), curr);
+ mo_check_promises(curr->get_tid(), curr, NULL);
get_thread(curr)->set_return_value(VALUE_NONE);
return updated_mod_order || updated_promises;
get_thread(curr)->set_return_value(VALUE_NONE);
return updated_mod_order || updated_promises;
bool ModelChecker::resolve_promises(ModelAction *write)
{
bool resolved = false;
bool ModelChecker::resolve_promises(ModelAction *write)
{
bool resolved = false;
- std::vector< thread_id_t, ModelAlloc<thread_id_t> > threads_to_check;
+ std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
Promise *promise = (*promises)[promise_index];
for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
Promise *promise = (*promises)[promise_index];
delete(promise);
promises->erase(promises->begin() + promise_index);
delete(promise);
promises->erase(promises->begin() + promise_index);
- threads_to_check.push_back(read->get_tid());
+ actions_to_check.push_back(read);
//Check whether reading these writes has made threads unable to
//resolve promises
//Check whether reading these writes has made threads unable to
//resolve promises
- for (unsigned int i = 0; i < threads_to_check.size(); i++)
- mo_check_promises(threads_to_check[i], write);
+ for (unsigned int i = 0; i < actions_to_check.size(); i++) {
+ ModelAction *read=actions_to_check[i];
+ mo_check_promises(read->get_tid(), write, read);
+ }
* write, or actually did the model action write.
*
* @param write The ModelAction representing the relevant write.
* write, or actually did the model action write.
*
* @param write The ModelAction representing the relevant write.
+ * @param read The ModelAction that reads a promised write, or NULL otherwise.
-void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
+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++) {
{
void *location = write->get_location();
for (unsigned int i = 0; i < promises->size(); i++) {
//same thread as the promise
if (act->get_tid() == tid) {
//same thread as the promise
if (act->get_tid() == tid) {
-
- //do we have a pwrite for the promise, if not, set it
- if (promise->get_write() == NULL) {
- promise->set_write(write);
- //The pwrite cannot happen before the promise
- if (write->happens_before(act) && (write != act)) {
+ //make sure that the reader of this write happens after the promise
+ if (( read == NULL ) || ( promise->get_action() -> happens_before(read))) {
+ //do we have a pwrite for the promise, if not, set it
+ if (promise->get_write() == NULL) {
+ promise->set_write(write);
+ //The pwrite cannot happen before the promise
+ if (write->happens_before(act) && (write != act)) {
+ priv->failed_promise = true;
+ return;
+ }
+ }
+
+ if (mo_graph->checkPromise(write, promise)) {
priv->failed_promise = true;
return;
}
}
priv->failed_promise = true;
return;
}
}
- if (mo_graph->checkPromise(write, promise)) {
- priv->failed_promise = true;
- return;
- }
}
//Don't do any lookups twice for the same thread
}
//Don't do any lookups twice for the same thread
ClockVector * get_cv(thread_id_t tid) const;
ModelAction * get_parent_action(thread_id_t tid) const;
void check_promises_thread_disabled();
ClockVector * get_cv(thread_id_t tid) const;
ModelAction * get_parent_action(thread_id_t tid) const;
void check_promises_thread_disabled();
- void mo_check_promises(thread_id_t tid, const ModelAction *write);
+ void mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction * read);
void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
bool isfeasibleprefix() const;
void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
bool isfeasibleprefix() const;