Hi Jeff,

What you are experiencing is a long standing set of limitations of seL4:
* Limited (currently 512mb on ia32) kernel window
* Static kernel window (i.e. memory cannot be swapped in and out)
* Simple offset translation of kernel virtual addresses to physical addresses

The result of these is that there is a 512mb¹ of physically contiguous memory (on x86 this starts at physical address 0) that becomes the kernel window and the RAM inside that region is all you get.

One of the goals of device untyped is to actually allow you to use the additional RAM that falls outside of the kernel window. Whilst you can only create frames out of it, and not arbitrary kernel objects, if you're needing lots of memory it is probably for frames anyway. Admittedly the kernel does not currently give the physical memory map to user level so know which 'devices' you can treat as memory currently requires a bit of hard coding and hoping that memory doesn't move between boots of a particular machine. Passing the memory map to the root task, as well as other things such as VBE info, is on the todo list, just not high priority yet.

x86-64 solves most of these problems by just having a giant kernel window :)

Adrian

[1] Technically 508mb as the last 4mb of the window is used to map kernel devices such as the APIC

On Wed 19-Oct-2016 8:15 AM, Jeff Waugh wrote:

Hi all,

Using x86 master on qemu with 2G memory, the kernel's map looks good:

Parsing GRUB physical memory map

Physical Memory Region from 0 size 9fc00 type 1

Physical Memory Region from 9fc00 size 400 type 2

Physical Memory Region from f0000 size 10000 type 2

Physical Memory Region from 100000 size 7fee0000 type 1

Adding physical memory region 0x100000-0x1fc00000

Physical Memory Region from 7ffe0000 size 20000 type 2

Physical Memory Region from fffc0000 size 40000 type 2

But the largest physical address of non-device untyped I get from bootinfo is 0x1faf9000. Same at 1G to 3G, though it does the right thing at 128M. On the other hand, x86_64 looks fine with 0x7ffc0000, and adapts to more.

btw, very exciting to see x86_64 code land! Working well so far.

Thanks,

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