projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
c832cb5
)
fix bug...can't mo_check_promises until we're done resolving promises for a write...
author
Brian Demsky
<bdemsky@uci.edu>
Thu, 4 Oct 2012 08:32:45 +0000
(
01:32
-0700)
committer
Brian Demsky
<bdemsky@uci.edu>
Thu, 4 Oct 2012 08:32:45 +0000
(
01:32
-0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 824e1e430c7e29c983a380a92ae821ddc425c721..667c1d57d68ee50ec5790cd0f8f2cf9458eab0c8 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-1490,6
+1490,7
@@
ClockVector * ModelChecker::get_cv(thread_id_t tid)
bool ModelChecker::resolve_promises(ModelAction *write)
{
bool resolved = false;
bool ModelChecker::resolve_promises(ModelAction *write)
{
bool resolved = false;
+ std::vector<thread_id_t> threads_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];
@@
-1507,14
+1508,18
@@
bool ModelChecker::resolve_promises(ModelAction *write)
post_r_modification_order(read, write);
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
post_r_modification_order(read, write);
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
- mo_check_promises(read->get_tid(), write);
-
delete(promise);
delete(promise);
+
promises->erase(promises->begin() + promise_index);
promises->erase(promises->begin() + promise_index);
+ threads_to_check.push_back(read->get_tid());
+
resolved = true;
} else
promise_index++;
}
resolved = true;
} else
promise_index++;
}
+ for(unsigned int i=0;i<threads_to_check.size();i++)
+ mo_check_promises(threads_to_check[i], write);
+
return resolved;
}
return resolved;
}