projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
f9772fc
)
fix two bugs in model.cc...mainly don't print bogus data race messages...
author
Brian Demsky
<bdemsky@uci.edu>
Sat, 3 Nov 2012 05:13:31 +0000
(22:13 -0700)
committer
Brian Demsky
<bdemsky@uci.edu>
Sat, 3 Nov 2012 05:13:31 +0000
(22:13 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 7808b104969f72fd9f9b62fe25a8574fffdac9b5..0fb315e24ce5b4a8e0c5db6d3c15516080f3e10e 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-218,7
+218,8
@@
void ModelChecker::execute_sleep_set() {
for(unsigned int i=0;i<get_num_threads();i++) {
thread_id_t tid=int_to_id(i);
Thread *thr=get_thread(tid);
for(unsigned int i=0;i<get_num_threads();i++) {
thread_id_t tid=int_to_id(i);
Thread *thr=get_thread(tid);
- if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
+ if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
+ thr->get_pending() == NULL ) {
thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
@@
-971,7
+972,7
@@
bool ModelChecker::promises_expired() {
/** @return whether the current partial trace must be a prefix of a
* feasible trace. */
bool ModelChecker::isfeasibleprefix() {
/** @return whether the current partial trace must be a prefix of a
* feasible trace. */
bool ModelChecker::isfeasibleprefix() {
- return promises->size() == 0 && pending_rel_seqs->size() == 0;
+ return promises->size() == 0 && pending_rel_seqs->size() == 0
&& isfeasible()
;
}
/** @return whether the current partial trace is feasible. */
}
/** @return whether the current partial trace is feasible. */