seL4/include
Gerwin Klein 97588df016
mcs: simplify sc_sporadic, assert invariant
It is an invariant in the MCS kernel that scSporadic implies sc_active.
Make use of that invariant by avoiding an explicit check for sc_active,
but assert the invariant in debug mode so it fails quickly when new
code breaks the invariant.

Essentially reverts 56098195f2 now that the invariant is preserved,
but adjusts the assertion from 17109eb8c9 to actually express
the invariant.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-11-07 08:39:10 +11:00
..
32/mode replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
64/mode replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
api doc: improve comments 2023-08-14 15:41:57 +10:00
arch riscv: place traps and fastpath code adjacently 2023-11-02 09:36:28 +00:00
benchmark benchmark: config opt. name to enable log buffer 2022-03-31 08:56:06 +11:00
drivers generc_timer: enable only once for mcs/non-mcs 2023-05-25 20:42:02 +10:00
fastpath Implemented the vm fault fastpath on aarch64 2023-03-08 17:58:14 +11:00
kernel mcs: simplify sc_sporadic, assert invariant 2023-11-07 08:39:10 +11:00
machine debug: restructure kernel console handling 2021-05-14 13:13:36 +10:00
model use types time_t and tickts_t properly 2023-08-14 15:41:57 +10:00
object remove Arch_migrateTCB() 2023-06-21 08:58:28 +10:00
plat make physBase a static inline function 2023-03-07 14:29:14 +11:00
smp create helper function handle_SysDebugSendIPI() 2022-01-10 11:58:30 +11:00
api.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
assert.h trivial: fix typos 2022-02-27 13:10:34 +11:00
basic_types.h boot: document region types 2023-04-12 15:07:02 +10:00
bootinfo.h boot: Remove constant BI_FRAME_SIZE_BITS 2023-08-23 15:10:32 +02:00
compound_types.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
config.h libsel4: Fix name for AARCH64_VSPACE_S2_START_L1 2021-09-06 08:08:54 +10:00
hardware.h boot: simplify boot code recycling 2023-08-13 09:04:26 +10:00
linker.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
machine.h re-use existing functions to avoid redundancy 2022-09-15 11:25:04 +02:00
object.h trivial: remove duplicate headers 2022-02-05 15:30:25 +11:00
stdarg.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
stdint.h print 64-bit integers on 32-bits systems fully 2021-11-26 06:01:11 +01:00
string.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
types.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
util.h make macro ARRAY_SIZE() handle corner cases 2022-03-10 18:16:00 +11:00