seL4/include
Adrian Danis 8028066a65 ksSchedulerAction contains candidate thread instead of target thread
Instead of switching to the thread contained in `ksSchedulerAction` on a `schedule` we
instead decide between the 'candidate' contained in `ksSchedulerAction`, the current thread
or potentially neither if the candidate is deemed invalid and the current thread is blocked.

A consequence of this change is that it is no longer meaningful to have a distinction between
`switchIfRequiredTo` and `attemptSwitchTo`. Now both these cases simply identify a candidate,
which may or may not be picked in `schedule`. Part of the distinction of `switchIfRequiredTo`
was to not avoid switching if possible when performing notifications. This is now handled by
prefering the current thread over the candidate if the current thread has not blocked.

This change is largely semantic preserving overall, with the exception of non-blocking
synchronous sends now acting like notifications and also preferring to resume running the
current thread.

The motivation for this change was to make it much easier for verification to show
correspondence between the fastpath changes introduced in the previous commit and the
slowpath scheduler.
2017-11-28 10:18:35 +11:00
..
32/mode Add stdint MAX definitions 2017-11-17 14:49:27 +11:00
64/mode Add stdint MAX definitions 2017-11-17 14:49:27 +11:00
api seL4_DebugDumpScheduler: reformat output 2017-06-23 10:28:54 +10:00
arch aarch64: implement cycle counter, PMU 2017-11-28 10:14:12 +11:00
benchmark Move timestamp_t definition to types.h 2017-11-28 10:13:49 +11:00
fastpath x64: Rearrange cnode_cap structure to improve fastpath speed 2017-01-10 16:57:57 +11:00
kernel ksSchedulerAction contains candidate thread instead of target thread 2017-11-28 10:18:35 +11:00
machine Fix licenses (the rest) 2017-06-22 15:29:12 +10:00
model Correct L2 bitmap size calculation and put it in one place 2017-11-28 10:18:35 +11:00
object Declare and check IPC buffer size 2017-10-27 16:12:18 +11:00
plat x64: add MODIFIES statements for extern functions 2017-11-09 12:18:31 +11:00
smp ARM/SMP: Re-implement atomic exchange taking sel4 IPI into account 2017-11-23 14:35:54 +11:00
api.h
assert.h Add unverified_compile_assert 2017-05-04 11:13:31 +10:00
basic_types.h
bootinfo.h
compound_types.h
config.h SMP: Introduce ENABLE_SMP_SUPPORT 2017-06-29 16:23:39 +10:00
linker.h Share linker.h between architectures 2017-08-10 08:38:36 +10:00
machine.h
Makefile Add stdint MAX definitions 2017-11-17 14:49:27 +11:00
object.h
stdarg.h
stdint.h Add stdint MAX definitions 2017-11-17 14:49:27 +11:00
string.h
types.h
util.h Verification: popcount- Avoid conflict variable names/types 2017-06-29 13:35:30 +10:00