projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
a79c756
)
fix getNextThread func
author
Derek Yeh
<djyeh@plrg-1.ics.uci.edu>
Fri, 7 Aug 2020 00:14:25 +0000
(17:14 -0700)
committer
Derek Yeh
<djyeh@plrg-1.ics.uci.edu>
Fri, 7 Aug 2020 00:14:25 +0000
(17:14 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 170edc748b8e9fc72c815d73a4ef1c098713587c..ac394d9a49ec9f164051c04328fe35af04e22d85 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-366,13
+366,14
@@
void ModelChecker::continueExecution(Thread *old)
Thread* ModelChecker::getNextThread()
{
Thread* ModelChecker::getNextThread()
{
- Thread *
thr
= nullptr;
+ Thread *
nextThread
= nullptr;
for (unsigned int i = curr_thread_num; i < get_num_threads(); i++) {
thread_id_t tid = int_to_id(i);
for (unsigned int i = curr_thread_num; i < get_num_threads(); i++) {
thread_id_t tid = int_to_id(i);
- thr = get_thread(tid);
+
Thread *
thr = get_thread(tid);
if (!thr->is_complete() && !thr->get_pending()) {
curr_thread_num = i;
if (!thr->is_complete() && !thr->get_pending()) {
curr_thread_num = i;
+ nextThread = thr;
break;
}
ModelAction *act = thr->get_pending();
break;
}
ModelAction *act = thr->get_pending();
@@
-383,7
+384,7
@@
Thread* ModelChecker::getNextThread()
chooseThread(act, thr);
}
chooseThread(act, thr);
}
- return
thr
;
+ return
nextThread
;
}
void ModelChecker::finishExecution(Thread *old)
}
void ModelChecker::finishExecution(Thread *old)
@@
-537,7
+538,12
@@
void ModelChecker::run()
curr_thread_num = 1;
thread_id_t tid = int_to_id(1);
Thread *thr = get_thread(tid);
curr_thread_num = 1;
thread_id_t tid = int_to_id(1);
Thread *thr = get_thread(tid);
- switch_from_master(thr);
+ if (!thr->get_pending())
+ switch_from_master(thr);
+ else {
+ consumeAction();
+ switch_from_master(thr);
+ }
finish_execution((exec+1) < params.maxexecutions);
//restore random number generator state after rollback
setstate(random_state);
finish_execution((exec+1) < params.maxexecutions);
//restore random number generator state after rollback
setstate(random_state);