Skip to content

Fix TCB size for SMP + benchmark config#1563

Merged
Ivan-Velickovic merged 2 commits intoseL4:masterfrom
Ivan-Velickovic:tcb_size_fix
Nov 24, 2025
Merged

Fix TCB size for SMP + benchmark config#1563
Ivan-Velickovic merged 2 commits intoseL4:masterfrom
Ivan-Velickovic:tcb_size_fix

Conversation

@Ivan-Velickovic
Copy link
Copy Markdown
Contributor

@Ivan-Velickovic Ivan-Velickovic commented Nov 21, 2025

In the definition of tcb_t, there's extra fields if there's SMP or BENCHMARK_TRACK_UTILISATION, looks like having both on is not enough for 11 bits.

@Ivan-Velickovic
Copy link
Copy Markdown
Contributor Author

Ivan-Velickovic commented Nov 21, 2025

I only ran into this on AArch64, but I only was building this kind of configuration of the kernel in AArch64 and RISC-V 64-bit.

lsf37
lsf37 approved these changes Nov 22, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume you found this because the compile_assert for the TCB size failed?

@Ivan-Velickovic
Copy link
Copy Markdown
Contributor Author

Ivan-Velickovic commented Nov 22, 2025 •
edited
Loading

Yes, but I'm wondering if I need a CONFIG_KERNEL_MCS in the condition as well, since Microkit always uses MCS. I'll play around with sel4test to figure out what exact combination trips the assert.

@midnightveil midnightveil mentioned this pull request Nov 24, 2025
Merged
@midnightveil
Copy link
Copy Markdown
Contributor

midnightveil commented Nov 24, 2025 •
edited
Loading

I can reproduce this without MCS:

cmake -GNinja -DKernelArmHypervisorSupport=ON -DKernelBenchmarks=track_utilisation -DKernelDebugBuild=OFF -DKernelMaxNumNodes=4 -DKernelPlatform=qemu-arm-virt -DKernelSel4Arch=aarch64 -DKernelVerificationBuild=OFF -DQEMU_MEMORY=2048 -S /home/julia/ts/seL4 -B . -DCROSS_COMPILER_PREFIX=aarch64-none-elf-

@midnightveil
Copy link
Copy Markdown
Contributor

midnightveil commented Nov 24, 2025 •
edited
Loading

But actually, only when KernelVerificationBuild=OFF is specified: (well, duh, because without that it ignores the benchmarks being turned on). Hypervisor OFF also makes it go away, same as SMP.

cmake -GNinja -DKernelArmHypervisorSupport=ON -DKernelBenchmarks=track_utilisation -DKernelDebugBuild=OFF -DKernelMaxNumNodes=4 -DKernelPlatform=qemu-arm-virt -DKernelSel4Arch=aarch64 -DQEMU_MEMORY=2048 -S /home/julia/ts/seL4 -B . -DCROSS_COMPILER_PREFIX=aarch64-none-elf-

@Ivan-Velickovic Ivan-Velickovic added the hw-build do all sel4test hardware builds on this PR label Nov 24, 2025
@Ivan-Velickovic
Fix TCB size for SMP + benchmark config
68590d3 
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 <[email protected]>
@lsf37
Copy link
Copy Markdown
Member

lsf37 commented Nov 24, 2025

Thanks for checking. It sounds like we can merge this when the tests have passed.

@lsf37 lsf37 moved this from Todo to In progress in seL4 release 14.0.0 (+ Microkit and others) Nov 24, 2025
@Ivan-Velickovic
Copy link
Copy Markdown
Contributor Author

Ivan-Velickovic commented Nov 24, 2025

Thanks for checking. It sounds like we can merge this when the tests have passed.

Yep, it looks like hypervisor support being on as well is what triggers it. I think we've got the right combination of config options now.

@Ivan-Velickovic Ivan-Velickovic merged commit 11c5d50 into seL4:master Nov 24, 2025
51 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@lsf37 lsf37 lsf37 approved these changes

@Indanz Indanz Indanz approved these changes

Assignees

No one assigned

Labels

hw-build do all sel4test hardware builds on this PR

Projects

No open projects
seL4 release 14.0.0 (+ Microkit and others)
Status: Done

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Ivan-Velickovic @midnightveil @lsf37 @Indanz