hardware.py: Create smaller UT at end of addresses

At the end of the physical address range, the last address isn't turned
into an UT object. The scripts generating the memory regions
unnecessarily round down to a small page size when they could instead
round down to the smallest UT size and this memory could be used for
smaller kernel objects.

Signed-off-by: Kent McLeod <kent@kry10.com>
This commit is contained in:
Kent McLeod 2021-09-21 18:54:23 +10:00 committed by Kent McLeod
parent 04c7ec0010
commit 18a3fb3bae
2 changed files with 6 additions and 1 deletions

View file

@ -27,6 +27,9 @@ class Config:
''' Get page size in bits for this arch '''
return 12 # 4096-byte pages
def get_smallest_kernel_object_alignment(self) -> int:
return 4 # seL4_MinUntypedBits is 4 for all configurations
def get_device_page_bits(self) -> int:
''' Get page size in bits for mapping devices for this arch '''
return self.get_page_bits()

View file

@ -97,7 +97,9 @@ def get_physical_memory(tree: FdtParser, config: Config) -> List[Region]:
def get_addrspace_exclude(regions: List[Region], config: Config):
''' Returns a list of regions that represents the inverse of the given region list. '''
ret = set()
as_max = utils.align_down(config.addrspace_max, config.get_page_bits())
# We can't create untypeds that exceed the addrspace_max, so we round down to the smallest
# untyped size alignment so that the kernel will be able to turn the entire range into untypeds.
as_max = utils.align_down(config.addrspace_max, config.get_smallest_kernel_object_alignment())
ret.add(Region(0, as_max, None))
for reg in regions: