threads: bugfix - do not call thread_current() from model-checker
authorBrian Norris <banorris@uci.edu>
Wed, 13 Feb 2013 00:54:38 +0000 (16:54 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 15 Feb 2013 22:55:02 +0000 (14:55 -0800)
commit3e520de48b5be0b0d4fa4a5f033e207b17c4496d
tree8437e3b2d4c61e2343b459110744ed1ff7a395cc
parente0d4c19ffcaf877eaac3a2b7324daae6c1fa7a25
threads: bugfix - do not call thread_current() from model-checker

thread_current() was designed for use in the user context. It is not
guaranteed to provide a reliable result in the model-checker context,
since we may perform context switches as needed, such that the "last
executed user thread" may not be the thread that we are checking at the
time.

This change is made to clear up future changes that will modify the
scheduling patterns.
model.cc
threads.cc