projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
c4f504b
)
edits
author
weiyu
<weiyuluo1232@gmail.com>
Mon, 10 Aug 2020 20:54:09 +0000
(13:54 -0700)
committer
weiyu
<weiyuluo1232@gmail.com>
Mon, 10 Aug 2020 20:54:09 +0000
(13:54 -0700)
model.cc
patch
|
blob
|
history
threads.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index a1204d0ab852352600edb95063476bd6f2976fa7..70ea4cd6534a9910ac176c1f497882e1ae6d3395 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-346,11
+346,13
@@
uint64_t ModelChecker::switch_to_master(ModelAction *act)
void ModelChecker::continueRunExecution(Thread *old)
{
void ModelChecker::continueRunExecution(Thread *old)
{
+/*
if (params.traceminsize != 0 &&
execution->get_curr_seq_num() > checkfree) {
checkfree += params.checkthreshold;
execution->collectActions();
}
if (params.traceminsize != 0 &&
execution->get_curr_seq_num() > checkfree) {
checkfree += params.checkthreshold;
execution->collectActions();
}
+*/
thread_chosen = false;
curr_thread_num = 1;
Thread *thr = getNextThread();
thread_chosen = false;
curr_thread_num = 1;
Thread *thr = getNextThread();
@@
-366,11
+368,13
@@
void ModelChecker::continueRunExecution(Thread *old)
void ModelChecker::startRunExecution(ucontext_t *old)
{
void ModelChecker::startRunExecution(ucontext_t *old)
{
+/*
if (params.traceminsize != 0 &&
execution->get_curr_seq_num() > checkfree) {
checkfree += params.checkthreshold;
execution->collectActions();
}
if (params.traceminsize != 0 &&
execution->get_curr_seq_num() > checkfree) {
checkfree += params.checkthreshold;
execution->collectActions();
}
+*/
thread_chosen = false;
curr_thread_num = 1;
Thread *thr = getNextThread();
thread_chosen = false;
curr_thread_num = 1;
Thread *thr = getNextThread();
@@
-402,7
+406,7
@@
Thread* ModelChecker::getNextThread()
scheduler->sleep(thr);
}
scheduler->sleep(thr);
}
-
chooseThread(act, thr);
+
//
chooseThread(act, thr);
}
return nextThread;
}
}
return nextThread;
}
@@
-478,7
+482,7
@@
uint64_t ModelChecker::switch_thread(ModelAction *act)
if (act2 && execution->is_enabled(old) && !execution->check_action_enabled(act2)) {
scheduler->sleep(old);
}
if (act2 && execution->is_enabled(old) && !execution->check_action_enabled(act2)) {
scheduler->sleep(old);
}
-
chooseThread(act2, old);
+
//
chooseThread(act2, old);
curr_thread_num++;
Thread* next = getNextThread();
curr_thread_num++;
Thread* next = getNextThread();
@@
-536,7
+540,7
@@
void ModelChecker::handleChosenThread(ucontext_t *old)
chosen_thread = get_next_thread();
if (!chosen_thread || chosen_thread->is_model_thread())
finishRunExecution(old);
chosen_thread = get_next_thread();
if (!chosen_thread || chosen_thread->is_model_thread())
finishRunExecution(old);
-
if (chosen_thread->just_woken_up()) {
+
/*
if (chosen_thread->just_woken_up()) {
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;
@@
-545,7
+549,9
@@
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();
@@
-587,10
+593,13
@@
void ModelChecker::run()
initstate(423121, random_state, sizeof(random_state));
checkfree = params.checkthreshold;
for(int exec = 0;exec < params.maxexecutions;exec++) {
initstate(423121, random_state, sizeof(random_state));
checkfree = params.checkthreshold;
for(int exec = 0;exec < params.maxexecutions;exec++) {
- chosen_thread = init_thread;
- thread_chosen = false;
- curr_thread_num = 1;
- startRunExecution(&system_context);
+ do {
+ chosen_thread = init_thread;
+ thread_chosen = false;
+ curr_thread_num = 1;
+ startRunExecution(&system_context);
+ } while (!should_terminate_execution());
+
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);
diff --git
a/threads.cc
b/threads.cc
index 3d6b0863234273684de989ce7dd199e9f1931a72..fc5c84a160296f12f7b3c39db3a84c898bafee9f 100644
(file)
--- a/
threads.cc
+++ b/
threads.cc
@@
-60,7
+60,7
@@
Thread * thread_current(void)
}
void modelexit() {
}
void modelexit() {
- model->switch_t
hread
(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
+ model->switch_t
o_master
(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
}
void initMainThread() {
}
void initMainThread() {