projects
/
c11tester.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Bug fix for spsc-queue test
[c11tester.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index 078a1ce75849ebc48334958a7842b22dd6c958d1..ea8f268ff270fa8d59674570103699c1eb36eb03 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-423,6
+423,7
@@
void ModelChecker::finishRunExecution(Thread *old)
void ModelChecker::finishRunExecution(ucontext_t *old)
{
scheduler->set_current_thread(NULL);
void ModelChecker::finishRunExecution(ucontext_t *old)
{
scheduler->set_current_thread(NULL);
+ break_execution = true;
}
void ModelChecker::consumeAction()
}
void ModelChecker::consumeAction()
@@
-544,12
+545,16
@@
void ModelChecker::handleChosenThread(Thread *old)
void ModelChecker::handleChosenThread(ucontext_t *old)
{
void ModelChecker::handleChosenThread(ucontext_t *old)
{
- if (execution->has_asserted())
+ if (execution->has_asserted())
{
finishRunExecution(old);
finishRunExecution(old);
+ return;
+ }
if (!chosen_thread)
chosen_thread = get_next_thread();
if (!chosen_thread)
chosen_thread = get_next_thread();
- if (!chosen_thread || chosen_thread->is_model_thread())
+ if (!chosen_thread || chosen_thread->is_model_thread())
{
finishRunExecution(old);
finishRunExecution(old);
+ return;
+ }
if (chosen_thread->just_woken_up()) {
chosen_thread->set_wakeup_state(false);
chosen_thread->set_pending(NULL);
if (chosen_thread->just_woken_up()) {
chosen_thread->set_wakeup_state(false);
chosen_thread->set_pending(NULL);
@@
-559,9
+564,7
@@
void ModelChecker::handleChosenThread(ucontext_t *old)
finishRunExecution(old);
else
startRunExecution(old);
finishRunExecution(old);
else
startRunExecution(old);
- } else
-
- {
+ } else {
/* Consume the next action for a Thread */
consumeAction();
/* Consume the next action for a Thread */
consumeAction();
@@
-604,7
+607,11
@@
void ModelChecker::run()
checkfree = params.checkthreshold;
for(int exec = 0;exec < params.maxexecutions;exec++) {
chosen_thread = init_thread;
checkfree = params.checkthreshold;
for(int exec = 0;exec < params.maxexecutions;exec++) {
chosen_thread = init_thread;
+ break_execution = false;
do {
do {
+ if (break_execution)
+ break;
+
thread_chosen = false;
curr_thread_num = 1;
startRunExecution(&system_context);
thread_chosen = false;
curr_thread_num = 1;
startRunExecution(&system_context);