projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
[model-checker.git]
/
promise.cc
diff --git
a/promise.cc
b/promise.cc
index 259ba058ddba82bbd8eaeb0b8559a24144cd087e..cbd45c2ffcf96f5398c49b29c4fdc2ef169c9b61 100644
(file)
--- a/
promise.cc
+++ b/
promise.cc
@@
-4,17
+4,17
@@
bool Promise::increment_threads(thread_id_t tid) {
unsigned int id=id_to_int(tid);
bool Promise::increment_threads(thread_id_t tid) {
unsigned int id=id_to_int(tid);
- if (
id>=synced_thread.size()
) {
+ if (
id >= synced_thread.size()
) {
synced_thread.resize(id+1, false);
}
if (synced_thread[id])
return false;
synced_thread[id]=true;
synced_thread.resize(id+1, false);
}
if (synced_thread[id])
return false;
synced_thread[id]=true;
-
bool
* enabled=model->get_scheduler()->get_enabled();
-
+
enabled_type_t
* enabled=model->get_scheduler()->get_enabled();
+ unsigned int sync_size=synced_thread.size();
for(unsigned int i=0;i<model->get_num_threads();i++) {
for(unsigned int i=0;i<model->get_num_threads();i++) {
- if (
!synced_thread[id] && enabled[id]
)
+ if (
(i >= sync_size || !synced_thread[i]) && (enabled[i] != THREAD_DISABLED)
)
return false;
}
return true;
return false;
}
return true;