Hi Alex,

This is coming about due to seL4 doing some extremely dumb memory allocation. I think I have worked out what is going on, so I will try to describe what is happening.

The kernels boot code needs to unpack the module, which is an elf file. It allocates the memory to unpack it into by picking the first page (physically) after the last module.

The check that is specifically failing for you here is where the kernel checks that this picked region is actually valid memory. Part of 'valid memory' for this purpose also means will fall inside the kernel window (which is approximately the first 512mb physically).

It looks to me like it was written this way because most bootloaders seem to place the modules in the first free physical memory after the kernel, and this algorithm then picks the next free physical address after that to load into.

There's absolutely no reason this couldn't do some more sensible memory allocation here, and it should definitely be fixed. Unfortunately I cannot say that we will get around to fixing this in a particularly timely manner.

Adrian

On Fri 22-Jul-2016 3:16 AM, Alexander Boettcher wrote:
Hi,

I want to boot seL4 (x86) 3.2.0 on a native machine (Lenovo X201) and I
get a message like:

End of loaded userland image lies outside of usable physical memory seL4
called fail at sel4/src/arch/x86/kernel/boot_sys.c: in function
boot_sys, saying "boot_sys failed for some reason :(

(Full log below attached)

It seems that our used bootloader put the image to high in physical
memory for seL4 (the other x86 kernels we use don't complain so far). Is
this right that only memory below PPTR_TOP (0x1fc00000 on x86 3.2.0) can
be used for the initial boot modules? Can this be changed or should we
not try to touch this define (it seems to be derived from various other
defines).

Is there maybe a description about the required physical memory layout
of the kernel and why it has to be as it is? Just in order to understand
better the constraints we probably have to apply to our bootloader ;-)

Thanks in advance,

Alex.





Parsing GRUB physical memory map
	Physical Memory Region from 0 size 89000 type 1
	Physical Memory Region from 89000 size 17000 type 2

	Physical Memory Region from d2000 size 2000 type 2

	Physical Memory Region from dc000 size 24000 type 2

	Physical Memory Region from 100000 size bb17c000 type 1
Adding physical memory region 0x100000-0x1fc00000
	Physical Memory Region from bb27c000 size 6000 type 2

	Physical Memory Region from bb282000 size dd000 type 1
	Physical Memory Region from bb35f000 size 12000 type 2

	Physical Memory Region from bb371000 size 81000 type 4
	Physical Memory Region from bb3f2000 size 1d000 type 2

	Physical Memory Region from bb40f000 size 60000 type 1
	Physical Memory Region from bb46f000 size 1f9000 type 2

	Physical Memory Region from bb668000 size 80000 type 4
	Physical Memory Region from bb6e8000 size 27000 type 2

	Physical Memory Region from bb70f000 size 8000 type 1
	Physical Memory Region from bb717000 size 8000 type 2

	Physical Memory Region from bb71f000 size 4c000 type 1
	Physical Memory Region from bb76b000 size c000 type 4
	Physical Memory Region from bb777000 size 3000 type 3
	Physical Memory Region from bb77a000 size 7000 type 4
	Physical Memory Region from bb781000 size 1000 type 3
	Physical Memory Region from bb782000 size 9000 type 4
	Physical Memory Region from bb78b000 size 1000 type 3
	Physical Memory Region from bb78c000 size 13000 type 4
	Physical Memory Region from bb79f000 size 60000 type 3
	Physical Memory Region from bb7ff000 size 1000 type 1
	Physical Memory Region from bb800000 size 800000 type 2

	Physical Memory Region from bc000000 size 4000000 type 2

	Physical Memory Region from e0000000 size 10000000 type 2

	Physical Memory Region from feaff000 size 1000 type 2

	Physical Memory Region from fec00000 size 10000 type 2

	Physical Memory Region from fed00000 size 0 type 2

	Physical Memory Region from fed1c000 size 4000 type 2

	Physical Memory Region from fed20000 size 70000 type 2

	Physical Memory Region from fee00000 size 1000 type 2

	Physical Memory Region from ff000000 size 1000000 type 2

	Physical Memory Region from 0 size 38000000 type 1



Kernel loaded to: start=0x100000 end=0x147000 size=0x47000 entry=0x10003e
ACPI: RSDP paddr=0xf68e0
ACPI: RSDP vaddr=0xdfcf68e0
ACPI: RSDT paddr=0xbb7f07a2
ACPI: RSDT vaddr=0xdfff07a2
ACPI: DMAR paddr=0xbb781000
ACPI: DMAR vaddr=0xdff81000
ACPI: IOMMU host address width: 36
	ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d
fun=0x0
	ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a
fun=0x0
	ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x2 fun=0x0
ACPI: 3 IOMMUs detected
ACPI: MADT paddr=0xbb7feb45
ACPI: MADT vaddr=0xdfffeb45
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_APIC apic_id=0x1
ACPI: MADT_APIC apic_id=0x4
ACPI: MADT_APIC apic_id=0x5
ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: 4 CPU(s) detected
Detected 4 CPUs. Only just 1
Detected 1 boot module(s):
  module #0: start=0x7fc7a000 end=0x7ffff338 size=0x385338 name='/image.elf'
ELF-loading userland images from boot modules:
size=0x385000 v_entry=0x2000000 v_start=0x2000000 v_end=0x2385000
p_start=0x80000000 p_end=0x80385000

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.