projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
f09f0fe
)
model: remove argument from mo_check_promises
author
Brian Norris
<banorris@uci.edu>
Sat, 9 Feb 2013 01:08:33 +0000
(17:08 -0800)
committer
Brian Norris
<banorris@uci.edu>
Sat, 9 Feb 2013 01:08:33 +0000
(17:08 -0800)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 3a5a4ba46aa788b83428657e7c593f877d50a734..7c6b90d7093e88d0452c14f2ceaa2bab633a58c1 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-729,7
+729,7
@@
bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
read_from(curr, reads_from);
mo_graph->commitChanges();
read_from(curr, reads_from);
mo_graph->commitChanges();
- mo_check_promises(curr
->get_tid(), reads_from, NULL
);
+ mo_check_promises(curr
, true
);
updated |= r_status;
} else if (!second_part_of_rmw) {
updated |= r_status;
} else if (!second_part_of_rmw) {
@@
-895,7
+895,7
@@
bool ModelChecker::process_write(ModelAction *curr)
}
mo_graph->commitChanges();
}
mo_graph->commitChanges();
- mo_check_promises(curr
->get_tid(), curr, NULL
);
+ mo_check_promises(curr
, false
);
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;
@@
-2312,7
+2312,7
@@
bool ModelChecker::resolve_promises(ModelAction *write)
for (unsigned int i = 0; i < actions_to_check.size(); i++) {
ModelAction *read = actions_to_check[i];
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
);
+ mo_check_promises(read
, true
);
}
return haveResolved;
}
return haveResolved;
@@
-2399,8
+2399,11
@@
void ModelChecker::check_promises_thread_disabled()
* @param write The ModelAction representing the relevant write.
* @param read The ModelAction that reads a promised write, or NULL otherwise.
*/
* @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, const ModelAction *read
)
+void ModelChecker::mo_check_promises(
const ModelAction *act, bool is_read_check
)
{
{
+ thread_id_t tid = act->get_tid();
+ const ModelAction *write = is_read_check ? act->get_reads_from() : act;
+
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
const ModelAction *pread = promise->get_action();
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
const ModelAction *pread = promise->get_action();
@@
-2412,7
+2415,7
@@
void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write,
// same thread as pread
if (pread->get_tid() == tid) {
// make sure that the reader of this write happens after the promise
// same thread as pread
if (pread->get_tid() == tid) {
// make sure that the reader of this write happens after the promise
- if (
(read == NULL) || (pread->happens_before(read
))) {
+ if (
!is_read_check || (pread->happens_before(act
))) {
// do we have a pwrite for the promise, if not, set it
if (promise->get_write() == NULL) {
promise->set_write(write);
// do we have a pwrite for the promise, if not, set it
if (promise->get_write() == NULL) {
promise->set_write(write);
diff --git
a/model.h
b/model.h
index f8c2bc867946dc255b0cf2946e9c8f85c422b4d2..99a93cdc9fd3e33dad9cbc5a4ef21954354c1191 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-121,7
+121,7
@@
public:
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, const ModelAction * read
);
+ void mo_check_promises(
const ModelAction *act, bool is_read_check
);
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;