Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-03-27 10:29:57 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix TCB size for SMP + benchmark config

Browse Source 
In the definition of tcb_t, there's extra fields if there's
SMP or BENCHMARK_TRACK_UTILISATION or ARM_HYPERIVSOR_SUPPORT.
It looks like the combination of all three (which Microkit uses)
is not enough for 11 bits.

Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This commit is contained in:
Ivan Velickovic
2025-11-21 21:12:22 +11:00
committed by Ivan Velickovic
parent 19b78543f9
commit 11c5d50527
1 changed files with 2 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
View File

@@ -170,7 +170,8 @@ typedef enum {
#define seL4_LargePageBits 21
#define seL4_HugePageBits 30
#define seL4_SlotBits 5
#if defined(CONFIG_HARDWARE_DEBUG_API) || defined(CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE)
#if defined(CONFIG_HARDWARE_DEBUG_API) || defined(CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE) || \
(defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ENABLE_SMP_SUPPORT) && defined(CONFIG_BENCHMARK_TRACK_UTILISATION))
#define seL4_TCBBits 12
#else
#define seL4_TCBBits 11