projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Bug fix for broken treatment of promises + coherence based pruning to regain pruning...
[model-checker.git]
/
promise.cc
diff --git
a/promise.cc
b/promise.cc
index 3a38384721cd3dfdc59b25f59440b432cf62c87b..a98403bbcf10569a91c2929bd17c420f4a3dc5f6 100644
(file)
--- a/
promise.cc
+++ b/
promise.cc
@@
-16,6
+16,7
@@
Promise::Promise(const ModelExecution *execution, ModelAction *read, struct future_value fv) :
execution(execution),
num_available_threads(0),
Promise::Promise(const ModelExecution *execution, ModelAction *read, struct future_value fv) :
execution(execution),
num_available_threads(0),
+ num_was_available_threads(0),
fv(fv),
readers(1, read),
write(NULL)
fv(fv),
readers(1, read),
write(NULL)
@@
-82,6
+83,12
@@
void Promise::add_thread(thread_id_t tid)
available_thread[id] = true;
num_available_threads++;
}
available_thread[id] = true;
num_available_threads++;
}
+ if (id >= was_available_thread.size())
+ was_available_thread.resize(id + 1, false);
+ if (!was_available_thread[id]) {
+ was_available_thread[id] = true;
+ num_was_available_threads++;
+ }
}
/**
}
/**
@@
-100,6
+107,14
@@
bool Promise::thread_is_available(thread_id_t tid) const
return available_thread[id];
}
return available_thread[id];
}
+bool Promise::thread_was_available(thread_id_t tid) const
+{
+ unsigned int id = id_to_int(tid);
+ if (id >= was_available_thread.size())
+ return false;
+ return was_available_thread[id];
+}
+
/**
* @brief Get an upper bound on the number of available threads
*
/**
* @brief Get an upper bound on the number of available threads
*