projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
annoying bug... Optimization was originally intended for the following insight:
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index 09e6b9da3150ddc88de4cc4b8ce363725cc493f3..da982d0db415395ed2be39e9dfcf3b34f74c1efe 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-272,8
+272,10
@@
bool ModelChecker::next_execution()
pending_rel_seqs->size());
pending_rel_seqs->size());
- if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
+ if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+ checkDataRaces();
print_summary();
print_summary();
+ }
if ((diverge = get_next_backtrack()) == NULL)
return false;
if ((diverge = get_next_backtrack()) == NULL)
return false;
@@
-1386,10
+1388,9
@@
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
unsigned int i;
{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
unsigned int i;
-
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
- ModelAction *write_after_read = NULL;
+
const
ModelAction *write_after_read = NULL;
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
@@
-1401,12
+1402,14
@@
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
break;
else if (act->is_write())
write_after_read = act;
break;
else if (act->is_write())
write_after_read = act;
+ else if (act->is_read()&&act->get_reads_from()!=NULL&&act!=reader) {
+ write_after_read = act->get_reads_from();
+ }
}
}
-
- if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+
+ if (write_after_read &&
write_after_read!=writer &&
mo_graph->checkReachable(write_after_read, writer))
return false;
}
return false;
}
-
return true;
}
return true;
}
@@
-1834,7
+1837,7
@@
void ModelChecker::compute_promises(ModelAction *curr)
!act->same_thread(curr) &&
act->get_location() == curr->get_location() &&
promise->get_value() == curr->get_value()) {
!act->same_thread(curr) &&
act->get_location() == curr->get_location() &&
promise->get_value() == curr->get_value()) {
- curr->get_node()->set_promise(i);
+ curr->get_node()->set_promise(i
, act->is_rmw()
);
}
}
}
}
}
}
@@
-1856,6
+1859,16
@@
void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
}
}
}
}
+void ModelChecker::check_promises_thread_disabled() {
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ if (promise->check_promise()) {
+ failed_promise = true;
+ return;
+ }
+ }
+}
+
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
@@
-1915,7
+1928,7
@@
void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
if (promise->has_sync_thread(tid))
continue;
if (promise->has_sync_thread(tid))
continue;
- if (mo_graph->checkReachable(promise->get_write(), write)) {
+ if (
promise->get_write()&&
mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
failed_promise = true;
return;
if (promise->increment_threads(tid)) {
failed_promise = true;
return;