I have created my own project on the PC99 architecture (x64) and have
been working through the tutorial source (copy & pasted into my project)
to learn and then prototype with seL4. I have done the mapping tutorial
(pc99) and utilized that code within my project and everything seems to
work just fine, but if I change out the seL4_X86_4K to
seL4_X86_LargePageObject I don't end up with 2MiB of mappable virtual space.
All the seL4 system calls through the client API return seL4_NoError.
The seL4_LargePageBits value is 21 (2^21 == 2MB, and intel documentation
for IA-32e shows that 2 MiB should be the large page size. However, if
I address memory outside of the first 256 KiB it halts.
The following works:
seL4_Word *x = (seL4_Word *) TEST_VADDR;
printf("Read x: %lu\n", *x);
And this works:
seL4_Word *x = (seL4_Word *) TEST_VADDR + 0x0003FFF0;
printf("Read x: %lu\n", *x);
But this halts when trying to dereference x to print it:
seL4_Word *x = (seL4_Word *) TEST_VADDR + 0x00040000;
printf("Read x: %lu\n", *x);
I am running seL4 12.1 using QEMU with the following command line:
qemu-system-x86_64 -cpu
Nehalem,-vme,+pdpe1gb,-fsgsbase,-invpcid,+syscall,+lm,enforce -nographic
-serial mon:stdio -m size=512M -s -S -kernel
../sel4-project/build/images/kernel-x86_64-pc99 -initrd build/cxxkit
Does anybody have any idea why I might be having this issue and what I
may do about it?
-Ben McCart
