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:
d57536b
)
schedule: do not allow model-checker thread to enter scheduler
author
Brian Norris
<banorris@uci.edu>
Sat, 6 Oct 2012 01:29:45 +0000
(18:29 -0700)
committer
Brian Norris
<banorris@uci.edu>
Mon, 8 Oct 2012 05:22:52 +0000
(22:22 -0700)
schedule.cc
patch
|
blob
|
history
diff --git
a/schedule.cc
b/schedule.cc
index cca60ebfba45795252c4e3de97d1223b934aa0f4..dd35237b22232df0744e22baadaaceb54ae6affd 100644
(file)
--- a/
schedule.cc
+++ b/
schedule.cc
@@
-48,6
+48,7
@@
bool Scheduler::is_enabled(Thread *t) const
void Scheduler::add_thread(Thread *t)
{
DEBUG("thread %d\n", id_to_int(t->get_id()));
void Scheduler::add_thread(Thread *t)
{
DEBUG("thread %d\n", id_to_int(t->get_id()));
+ ASSERT(!t->is_model_thread());
set_enabled(t, THREAD_ENABLED);
}
set_enabled(t, THREAD_ENABLED);
}
@@
-79,6
+80,7
@@
void Scheduler::sleep(Thread *t)
*/
void Scheduler::wake(Thread *t)
{
*/
void Scheduler::wake(Thread *t)
{
+ ASSERT(!t->is_model_thread());
set_enabled(t, THREAD_DISABLED);
t->set_state(THREAD_READY);
}
set_enabled(t, THREAD_DISABLED);
t->set_state(THREAD_READY);
}
@@
-106,6
+108,9
@@
Thread * Scheduler::next_thread(Thread *t)
return NULL;
}
}
return NULL;
}
}
+ } else if (t->is_model_thread()) {
+ /* model-checker threads never run */
+ t = NULL;
} else {
curr_thread_index = id_to_int(t->get_id());
}
} else {
curr_thread_index = id_to_int(t->get_id());
}
@@
-120,6
+125,7
@@
Thread * Scheduler::next_thread(Thread *t)
*/
Thread * Scheduler::get_current_thread() const
{
*/
Thread * Scheduler::get_current_thread() const
{
+ ASSERT(!current || !current->is_model_thread());
return current;
}
return current;
}