projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
43124ec
)
rename params
author
Derek Yeh
<djyeh@plrg-1.ics.uci.edu>
Sun, 2 Aug 2020 22:24:18 +0000
(15:24 -0700)
committer
Derek Yeh
<djyeh@plrg-1.ics.uci.edu>
Sun, 2 Aug 2020 22:24:18 +0000
(15:24 -0700)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index d3692c47c80c5731cc32e9bddc920aa5a7d8bdad..170edc748b8e9fc72c815d73a4ef1c098713587c 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-402,21
+402,21
@@
void ModelChecker::consumeAction()
chosen_thread = execution->take_step(curr);
}
chosen_thread = execution->take_step(curr);
}
-void ModelChecker::chooseThread(ModelAction *act, Thread *
old
)
+void ModelChecker::chooseThread(ModelAction *act, Thread *
thr
)
{
{
- if (!thread_chosen && act && execution->is_enabled(
old) && (old
->get_state() != THREAD_BLOCKED) ) {
+ if (!thread_chosen && act && execution->is_enabled(
thr) && (thr
->get_state() != THREAD_BLOCKED) ) {
if (act->is_write()) {
std::memory_order order = act->get_mo();
if (order == std::memory_order_relaxed || \
order == std::memory_order_release) {
if (act->is_write()) {
std::memory_order order = act->get_mo();
if (order == std::memory_order_relaxed || \
order == std::memory_order_release) {
- chosen_thread =
old
;
+ chosen_thread =
thr
;
thread_chosen = true;
}
} else if (act->get_type() == THREAD_CREATE || \
act->get_type() == PTHREAD_CREATE || \
act->get_type() == THREAD_START || \
act->get_type() == THREAD_FINISH) {
thread_chosen = true;
}
} else if (act->get_type() == THREAD_CREATE || \
act->get_type() == PTHREAD_CREATE || \
act->get_type() == THREAD_START || \
act->get_type() == THREAD_FINISH) {
- chosen_thread =
old
;
+ chosen_thread =
thr
;
thread_chosen = true;
}
}
thread_chosen = true;
}
}
@@
-443,6
+443,16
@@
uint64_t ModelChecker::switch_thread(ModelAction *act)
}
old->set_pending(act);
}
old->set_pending(act);
+
+ if (old->is_waiting_on(old))
+ assert_bug("Deadlock detected (thread %u)", curr_thread_num);
+
+ ModelAction *act2 = old->get_pending();
+
+ if (act2 && execution->is_enabled(old) && !execution->check_action_enabled(act2)) {
+ scheduler->sleep(old);
+ }
+ chooseThread(act2, old);
curr_thread_num++;
Thread* next = getNextThread();
curr_thread_num++;
Thread* next = getNextThread();
@@
-456,16
+466,6
@@
uint64_t ModelChecker::switch_thread(ModelAction *act)
void ModelChecker::handleNewValidThread(Thread *old, Thread *next)
{
void ModelChecker::handleNewValidThread(Thread *old, Thread *next)
{
- if (old->is_waiting_on(old))
- assert_bug("Deadlock detected (thread %u)", curr_thread_num-1);
-
- ModelAction *act = old->get_pending();
-
- if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) {
- scheduler->sleep(old);
- }
- chooseThread(act, old);
-
scheduler->set_current_thread(next);
if (Thread::swap(old, next) < 0) {
scheduler->set_current_thread(next);
if (Thread::swap(old, next) < 0) {
diff --git
a/model.h
b/model.h
index b81858c87f6a815c2ea4d58c5fc46f2562d72534..503b225d23569b4acc8a9b8564ab80c9537c621c 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-58,7
+58,7
@@
public:
void continueExecution(Thread *old);
void finishExecution(Thread *old);
void consumeAction();
void continueExecution(Thread *old);
void finishExecution(Thread *old);
void consumeAction();
- void chooseThread(ModelAction *act, Thread *
old
);
+ void chooseThread(ModelAction *act, Thread *
thr
);
Thread * getNextThread();
void handleChosenThread(Thread *old);
void handleNewValidThread(Thread *old, Thread *next);
Thread * getNextThread();
void handleChosenThread(Thread *old);
void handleNewValidThread(Thread *old, Thread *next);