portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

mcs: Don't rollback time when not rescheduling

Browse source 
This allows ksCurTime to be monotonically increasing making proofs much
easier to construct.
This commit is contained in:
Curtis Millar 2019-08-23 12:11:10 +10:00
parent 8748d8ea5e
commit c25e5445fb
2 changed files with 0 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
include/kernel/thread.h
View file

@ -130,16 +130,6 @@ static inline void commitTime(void)
NODE_STATE(ksConsumed) = 0llu;
}
static inline void rollbackTime(void)
{
/* it is invalid to rollback time if we
* have already acted on the new time */
assert(!NODE_STATE(ksReprogram) || NODE_STATE(ksConsumed) == 0);
NODE_STATE(ksCurTime) -= NODE_STATE(ksConsumed);
NODE_STATE(ksConsumed) = 0llu;
}
static inline bool_t PURE isSchedulable(const tcb_t *thread)
{
return isRunnable(thread) &&

3
src/kernel/thread.c
View file

@ -345,9 +345,6 @@ static void switchSchedContext(void)
/* if we are reprogamming, we have acted on the new kernel time and cannot
* rollback -> charge the current thread */
commitTime();
} else {
/* otherwise, we don't need to do anything - avoid reprogramming the timer */
rollbackTime();
}
NODE_STATE(ksCurSC) = NODE_STATE(ksCurThread)->tcbSchedContext;