seL4_X86_Page_Map on seL4_X86_LargePageObject != 2MiB
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
Hi Ben,
I think you are accessing all 2MB of the page, it's just that TEST_VADDR is being cast to a seL4_Word *, and doing pointer arithmetic like TEST_VADDR + 1 increments the address by the size of the type being pointed to (see https://www.gnu.org/software/c-intro-and-ref/manual/html_node/Pointer-Arithm...), which for an seL4_Word on x86_64 is 8 bytes, not one. 8 * 0x00040000 is indeed 2MB so I suspect that if you cast the pointer to a uint8_t * or a char * instead, you'll find that your example works as expected.
- Alwin
________________________________
From: Ben McCart
Alwin, Exactly right - thank you! I am not a C guy and I don't use C-style casts in my code. I did not realize the operator presedence there was adding to the pointer instead of adding to the number before cast to pointer. Shame on me for not taking the time to investigate the pointer value in the debugger or even considering that the perceived range was 1/8 th of the target rage... exactly sizeof(seL4_Word). -Ben On 7/9/2024 7:46 PM, Alwin Joshy wrote:
Hi Ben,
I think you are accessing all 2MB of the page, it's just that TEST_VADDR is being cast to a seL4_Word *, and doing pointer arithmetic like TEST_VADDR + 1 increments the address by the size of the type being pointed to (see https://www.gnu.org/software/c-intro-and-ref/manual/html_node/Pointer-Arithm... https://www.gnu.org/software/c-intro-and-ref/manual/html_node/Pointer-Arithm...), which for an seL4_Word on x86_64 is 8 bytes, not one. 8 * 0x00040000 is indeed 2MB so I suspect that if you cast the pointer to a uint8_t * or a char * instead, you'll find that your example works as expected.
- Alwin ------------------------------------------------------------------------
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
participants (2)
-
Alwin Joshy -
Ben McCart