projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
54fe8f7
)
fix bugs
author
Derek Yeh
<djyeh@plrg-1.ics.uci.edu>
Tue, 28 Jul 2020 05:52:49 +0000
(22:52 -0700)
committer
Derek Yeh
<djyeh@plrg-1.ics.uci.edu>
Tue, 28 Jul 2020 05:52:49 +0000
(22:52 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 2aacaa2de441e3d3ff391b8009a241431fa0f9d7..5decd2bea613c3058abcfd53dcc0d371fd3f5336 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-440,6
+440,9
@@
uint64_t ModelChecker::switch_thread(ModelAction *act)
exit(EXIT_FAILURE);
}
} else {
exit(EXIT_FAILURE);
}
} else {
+ if (old->is_waiting_on(old))
+ assert_bug("Deadlock detected (thread %u)", curr_thread_num);
+
if (execution->has_asserted())
finishExecution(old);
if (!chosen_thread)
if (execution->has_asserted())
finishExecution(old);
if (!chosen_thread)
@@
-450,7
+453,11
@@
uint64_t ModelChecker::switch_thread(ModelAction *act)
chosen_thread->set_wakeup_state(false);
chosen_thread->set_pending(NULL);
chosen_thread = NULL;
chosen_thread->set_wakeup_state(false);
chosen_thread->set_pending(NULL);
chosen_thread = NULL;
- continueExecution(old); // Allow this thread to stash the next pending action
+ // Allow this thread to stash the next pending action
+ if (should_terminate_execution())
+ finishExecution(old);
+ else
+ continueExecution(old);
} else {
/* Consume the next action for a Thread */
consumeAction();
} else {
/* Consume the next action for a Thread */
consumeAction();