search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Fix value of seL4_MaxUntypedBits when emulating kernel boot #20

Closed Ivan-Velickovic closed 5 months ago

Ivan-Velickovic commented 1 year ago

I believe the variable max_bits corresponds to seL4_MaxUntypedBits. The value of this on AArch64 is 47 (see seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h.

I have not run into issues because this value is not correct yet, but I thought I would try to fix it before having to debug something going wrong.

bennoleslie commented 1 year ago

I need to spend a little more time on this one. (Very simple change!).

I'm not 100% sure that it is intended to match seL4_MaxUntypedBits (it probably is, but I just want to check, from memory there is a few different things going on there).

Ideally these constants come from a kernel build process artefact that would specify all of these in JSON or something.

Ivan-Velickovic commented 1 year ago

I think this code is trying to emulate the kernel function create_untypeds_for_region.

I agree that these constants should come from the kernel build output. This isn't currently done by the kernel, but I'll look into changing it to do so.